rhi/blog
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

some posts

Browse source
This commit is contained in:
rhiannon morris 2024-11-29 00:52:10 +01:00
parent e228947212
commit cf0624a983
55 changed files with 636 additions and 1086 deletions
Download patch file Download diff file Expand all files Collapse all files

315
posts-wip/2023-06-05-quox.md
View file

@ -1,315 +0,0 @@
---
title: intro to quox
date: 2023-06-05
tags: [computer, quox (language)]
show-toc: true
bibliography: quox.bib
link-citations: true
...
<figure class='shaped floating' style='shape-outside: url(/images/quox.png)'
aria-label=''>
<img src=/images/quox.png
alt='quox sprite from quest of ki'
title='quox sprite from quest of ki'>
<figcaption>(this is a quox)</figcaption>
</figure>
hello for _a while_ now i've been working on a language called quox. the
one-sentence, meaningless summary is "qtt and xtt mashed together".
:::aside
wow, q and x! what an amazing coincidence!
:::
but maybe i should say what those are. i'm going to _try_ to aim this at someone
who knows normal languages. i guess we'll see how successful that is. so first,
# dependent types {#dt}
maybe you already know this one. skip it if you want. (maybe you know all of
this but you came to say hi anyway. hi!)
all a <dfn>dependent type</dfn> is is a type that is allowed to talk about run
time values. like a dependent pair might be `(len : ℕ) × Array len String` for
a length paired with an array of strings with that length. a dependent function
with a type like `(len : ℕ) → (x : A) → Array len A` takes a length and element
`x` as arguments, and returns an array of that many copies of `x`.
even ~~parametric polymorphism~~ generics are a specific form of dependent type:
you take a type as a parameter, and get to use it in the types of the other
arguments.
:::aside
<details>
<summary>but i can do that in rust/c++/haskell too</summary>
yeah! well, partially. in rust you can have like
```rust
fn replicate<const N: usize, A: Clone>(val: A) -> [A; N] {
[(); N].map(|_| val.clone())
}
```
but it's a bit more restricted:
- `N` has to always be known at compile time. you can't, for example, have the
length come from a config file or command-line argument
- in rust [(at the time of writing)]{.note} and c++, only certain number-ish
types can be used in this way. in ghc-haskell you have more choice for what
data can be used in types, but you—or template haskell—have to rewrite
functions for the type and value level, and have "singleton" types to bridge
between compile time and run time
so yeah, you can get some of the way there, but not completely.
</details>
:::
dependent types let you classify values more precisely than before, so you can
do things like have ASTs that reflect their local variables in the type.
in quox, and most uses of this technique, it's enough to just keep the _number_
of variables in scope.
[(there are two counts in quox; see [below](#xtt) for why.)]{.note}
in a definition like
<!-- i need a default quantity so i can write this without any "what's that" -->
```quox
def backwards-plus : ω.ℕ → ω.ℕ → ℕ =
λ a b ⇒ plus b a
```
:::aside
<details>
<summary>what does all that mean</summary>
- the `ω` before each argument means you have no restrictions on how you can
use it. see [below](#qtt). i want to have a default so you could just write
`ℕ → ℕ → ℕ`, but i can't decide what the default should _be_
- functions are curried, which means they take their arguments one by one, like
in haskell or ocaml, rather than in a tuple. doing it this way makes writing
dependencies (and quantities) easier.
- a function is written as `λ var1 var2 ⇒ body`
- all those funky symbols have ascii alternatives, so you if you like it better
you can also write
```quox
def backwards-plus : #.Nat -> #.Nat -> Nat =
fun a b => plus b a
```
</details>
:::
the right hand side `λ a b ⇒ plus b a` is necessarily a `Term 0 0`, with
no local variables. the body of the function is a `Term 0 2`, because it has two
term variables in scope.
typing contexts also know how many variables they bind, so you can know for sure
you are keeping the context properly in sync with the term under consideration.
and if you forget, then the compiler, uh, "reminds" you. since it's notoriously
easy to make off-by-one errors and similar mistakes when dealing with variables,
so having the computer check your work helps a lot.
--------------------------------------------------------------------------------
you might not want to have every property you will ever care about be always
reflected in types. quox's expressions have their scope size in their type,
because dealing with variables is ubiquitous and fiddly, but they don't have
like, a flag for whether they're reducible. i _do_ care about that sometimes,
but it's easier to have it as a separate value:
```idris
-- in Data.So in the standard library
data Oh : Bool -> Type where
Oh : So True
-- in Data.DPair (simplified for now)
data Subset : (a : Type) -> (p : a -> Type) -> Type where
Element : (x : a) -> p x -> Subset a p
isRedex : Definitions -> Term d n -> Bool
whnf : (defs : Definitions) -> WhnfContext d n ->
Term d n -> Subset (Term d n) (\t => So (not (isRedex defs t)))
```
a term is a <dfn>redex</dfn> (reducible expression) if the top level AST node is
something that can be immediately reduced, like a function being applied to an
argument, or a definition that can be unfolded. <dfn>whnf</dfn> ([weak head
normal form][whnf]) reduces the top of the expression until there are no more
reductions to do, and then returns the result, along with a proof that there are
no more.
[whnf]: https://en.wikipedia.org/wiki/Lambda_calculus_definition#Weak_head_normal_form
datatype arguments can be of any type, but also, data constructors can restrict
the values of those arguments in their return types. (this is what makes them
useful in the first place.) in this case, `So` only has one constructor, only
usable when its argument is `True`, meaning that constructing a value of type
`So p` is only possible if the expression `p` reduces to `True`.
:::aside
<details>
<summary>`So` considered harmful, or whatever</summary>
in a lot of cases you need to write the property inductively, i.e., as a
datatype, like
```idris
data NotRedex : Definitions -> Term d n -> Type
-- DPair is similar to Subset
whnf : (defs : Definitions) -> WhnfContext d n ->
Term d n -> DPair (Term d n) (\t => NotRedex defs t)
```
the reason for this is that it is often easier to define other functions by
matching on the proof rather than the original term.
but in this case that is not necessary and writing a function into `Bool` is
easier.
</details>
:::
other parts of the compiler, like equality checking, can similarly require
a proof that their arguments are not redexes, so that they don't have to keep
calling `whnf` over and over, or risk wrongly failing if one argument isn't
reduced enough.
# qtt (quantitative type theory) {#qtt}
:::note
(idris (2) has this one too, so i can still use real examples for now)
:::
having this extra safety is nice, but it would be even nicer if it we could be
sure it wouldn't affect run time efficiency. for a long time, dependently typed
languages have tried to use heuristics to elide constructor fields that were
already determined by other fields, at least as far back as 2003 [@indices].
but these analyses are anti-modular, in that a constructor field can only be
erased if it is not matched against _anywhere_ in the whole program.
maybe we should try telling the computer what we actually want.
in qtt [@qtt; @nuttin], every local variable is annotated with
a <dfn>quantity</dfn>, telling us how many times we can use it at run time. in
quox [(and idris2)]{.note}, the possible choices are `0` (not at all;
<dfn>erased</dfn>), `1` (exactly once; <dfn>linear</dfn>), and `ω` (any number
of times; <dfn>unrestricted</dfn>, and the default in idris and not written). if
a variable is marked with `0`, then you can't do anything with it that would
affect run time behaviour. for example,
- you can only match on values if their type has one or zero cases. if you
"have" a variable of the empty type `v : {}`, you're already in an unreachable
branch, so it's fine to abort with
`case0 v return 〈whatever〉 of { }`.
if you have an erased pair, it's fine to split it up, but the two parts will
still be erased.
matching on something like `Bool` isn't possible, because the value is no
longer there to look at.
- type signatures only exist at compile time so you can do whatever you want
there.
- equality proofs don't have any computational behaviour (unlike in [some other
type theories][hott]), so [coercion](#xtt) works with an erased proof
[hott]: https://homotopytypetheory.org
as well as erasure, there is also linearity. a linear variable must be used
exactly once in a linear context (and any number of times in an erased context,
like in types or proofs talking about it). this is useful for things like file
handles and other kinds of resources that have strict usage requirements. it's
similar to passing a variable by value in rust, where after you do so, you can't
use it yourself any more.
:::aside
there's no equivalent to <dfn>borrowing</dfn> inside the type system, but
i think with a careful choice of builtins, it would be possible to do a similar
thing in an external library.
_[rust person voice]_ it would be less _ergonomic_ as library, but having
a borrow checker inside the language would immediately blow my _complexity
budget_. :crab:
:::
i don't have much to say about this, honestly, but ask any rust user about the
benefits of tracking resource ownership in types.
--------------------------------------------------------------------------------
so where do these quantities come from? from the types, of course. a function
type in quox, which looks like `ρ.(x : A) → B`, has a quantity ρ attached,
which describes how a function value of that type can use its argument.
an identity function `λ x ⇒ x` can have type `1.A → A` or `ω.A → A`, but not
`0.A → A`. and a "diagonal" function `λ x ⇒ (x, x)` can only be `ω.A → A × A`.
a whole definition can be erased (and if it's a definition of a type, it has to
be, since types don't exist at run time), like
```quox
def0 TwoOfThem : ★ = ℕ × ℕ
```
finally, you can mark a specific term with a quantity. say you want to write
a function that returns some number, plus an erased proof that it's even.
obviously you can't mark the whole definition as erased with `def0`, since
you want the number itself. and giving the return type as `(n : ℕ) × Even n`
makes the proof appear at run time, which might be unwanted if it's something
big. so you can erase the second half of the pair by writing
`(n : ℕ) × [0. Even n]`. a value of a "boxed" type `\[π. A]` is written `\[e]`
if `e : A`. for a slightly bigger example, you might want a decidable equality
that gives you _erased_ proofs, so you can use them in coercions, but they don't
show up at run time.
```quox
def0 Not : ω.★ → ★ = λ A ⇒ ω.A → {}
def0 Either : ω.★ → ω.★ → ★ = ⋯ -- constructors Left and Right
def0 Dec : ω.★ → ★ = λ A ⇒ Either [0. A] [0. Not A]
def Yes : 0.(A : ★) → 0.A → Dec A = λ A y ⇒ Left [0. A] [0. Not A] [y]
def No : 0.(A : ★) → 0.(Not A) → Dec A = λ A n ⇒ Right [0. A] [0. Not A] [n]
def0 DecEq : ω.★ → ★ = λ A ⇒ ω.(x y : A) → Dec (x ≡ y : A)
```
you can also use the same construction to have some unrestricted parts of an
otherwise linear structure.
:::aside
still missing from this story, in my opinion, is some form of compile-time
irrelevance. a lot of the time, you don't care about the content of a proof,
only that it is satisfied, so if division has a type like
`div : 1.ℚ → 1.(d : ℚ) → 0.(NonZero d) → ℚ`, you want some way to get
`div x y p₁` and `div x y p₂` to always be equal, without even having to look at
`p₁` and `p₂`. there's no way to do that yet, because it doesn't seem to fit
into qtt cleanly. maybe a single squash type..?
:::
# xtt ("extensional" type theory) {#xtt}
:::aside
but not _that_ extensional type theory
:::
[@xtt]
# other stuff {#misc}
- crude but effective [@crude; @mugen]
- bidirectional typechecking [@bidi]
- ...
# i still don't know how to actually write a program {.unnumbered}
i know. that's ok. i'm just trying to communicate why someone might,
hypothetically, care.
did it work?
# references {#ref}

112
posts-wip/2023-10-25-quox.md
View file

@ -1,112 +0,0 @@
---
title: quox. the language
date: 2023-10-25
tags: [quox, computer, types]
bibliography: quox.bib
link-citations: true
show-toc: true
...
<style>
header h1 { margin-left: 0; }
header h1::before, header h1::after {
content: url(../images/qt.svg);
display: inline-block;
height: 0.75em; width: 0.75em;
padding: 0 0.5em;
}
header h1::before {
transform: rotateY(0.5turn);
}
main > :is(h1, h2, h3, h4, h5, h6)::after {
content: url(../images/quox-tod.png);
image-rendering: crisp-edges;
image-rendering: pixelated;
margin-left: 0.5em;
}
.qtt-q { font-family: Muller; font-weight: 600; color: #60c; }
.xtt-x { font-family: Muller; font-weight: 600; color: #082; }
#panqt {
--width: 202px; --height: 200px;
}
#panqt div {
width: var(--width); height: var(--height);
position: relative;
}
#panqt img, #panqt div::before {
position: absolute;
top: 0; left: 0;
width: var(--width); height: var(--height);
}
#panqt div::before {
content:
image-set(url(../images/panqt.png) 1x,
url(../images/panqt2x.png) 2x);
mix-blend-mode: multiply;
}
#panqt figcaption {
width: var(--width);
}
</style>
:::{.aside .floating}
### [hot minute][wkt]&ensp;*n.* {.unnumbered}
1. A long period of time.
2. A short period of time.
3. An unspecified period of time.
[wkt]: https://en.wiktionary.org/wiki/hot_minute
:::
for the last _hot minute_ [@hotminute], i’ve been working on a little programming language. it’s finally starting to approach a state where it can compile some programs, so maybe i should talk about it a bit.
# what is a quox [(tl;dr for type system nerds)]{.note}
<figure class=floating>
<img src=../images/quox.png class='shadow pixel'
alt='a dragon from an old arcade game'
title='use my warps to skip some floors!'>
<figcaption>this is also a quox.</figcaption>
</figure>
0. it’s a *dependently typed functional language*, like your agdas and your idrises.
1. *[q]{.qtt-q}uantitative type theory* (qtt) [@nuttin; @qtt] is a nice combination of dependent types, resource tracking, and erasure of stuff like proofs.
2. it uses *[x]{.xtt-x}tt* [@xtt] for equality. i think it's neat
3. it has a *closed type universe*. you don’t define new datatypes, but the language gives you building blocks to put them together. this is because of xtt originally, but i just ran with it.
so now you can see where the name [q]{.qtt-q}uo[x]{.xtt-x} comes from. other than my favourite dragon. anyway it also has
4. *bidirectional type checking* [@bidi]
5. crude-but-effective stratification [@crude; @crude-blog] for dealing with universes
# dependent types
<figure class=floating>
<div><img src=../images/panqt.png srcset='../images/panqt.png 2x'
width=202 height=200
alt='one of my fursonas is a quox with three heads'
title='i hear putting pictures of your fursona on your blog is a good way to get hacker news types Big Mad'></div>
<figcaption>
sometimes i am also a quox. or three, depending on how you count.
</figcaption>
</figure>
there are lots of languages with dependent types already. if you are reading this, chances are probably _quite_ high you already know what they are and can skip to the next section.
`*but still something. probably*`
# qtt
sometimes, values can only be used in certain ways to make sense. this isn't controversial: it's the old use-after-free.
# xtt
# references {#refs}

513
posts-wip/quox-type-system.md
View file

@ -1,513 +0,0 @@
---
title: quox's type system
tags: [quox, programming]
date: 2021-07-26
...
main inspirations:
- [quantitative type theory](https://bentnib.org/quantitative-type-theory.pdf)
(2018\)
- mostly [conor's version](
https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.pdf),
even though it's older (2016)
- track how often things are used in terms. you get linearity if you want
it, but also, predictable erasure
- [graded modal dependent type theory](https://arxiv.org/pdf/2010.13163) (2021)
- a refinement of qtt. track occurrences in types too! your context becomes
two-dimensional but that's ok
- also the way quantities are tracked is a bit different
- [observational type theory](
https://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf) (2007)
- nice middle ground between intensional and extensional type theory. you
get stuff like funext in a decidable setting
- [xtt](https://arxiv.org/pdf/1904.08562.pdf)
("extensional" type theory, but not that one) (2019)
- a cubical reformulation of the ideas in ott. no univalence stuff tho,
don't worry i'm still #&#x2060;UIP&#x2060;Crew
<!-- those are WORD JOINERs btw, so that hopefully a screen reader will know to
say "hash u.i.p. crew" instead of whatever else -->
the basic idea is to mash all of these things together, obviously, but also to
embrace a closed type theory, so that stuff like the type-case in xtt can make
sense, and try to be a nice language anyway. what's a datatype?
the core then only needs to know about basic type formers like functions,
pairs, w-types (:cold_sweat:), cubes (:cold_sweat: :cold_sweat: :cold_sweat:),
etc, and their eliminators, instead of having to do the whole thing with
datatypes and functions. those would still exist in an eventual surface
language tho, since otherwise writing anything will be extremely painful, but
elaborated to this stuff.
# syntax
:::defs
$$
\newcommand\EQ{\mathrel\Coloneqq}
\newcommand\OR[1][]{\mkern17mu #1| \mkern10mu}
\newcommand\Or{\mathrel|}
\newcommand\KW\mathsf
\newcommand\L\mathbfsf
$$
$$
\newcommand\Type[1]{\KW{type}_{#1}}
\newcommand\Tup[1]{\langle #1 \rangle}
\newcommand\WTy{\mathbin\blacktriangleleft}
\newcommand\WTm{\mathbin\vartriangleleft}
\newcommand\BoxType{\mathop\blacksquare}
\newcommand\BoxTy[1]{\mathop{\blacksquare_{#1}}}
\newcommand\BoxTm{\mathop\square}
\newcommand\Case{\KW{case}\:}
\newcommand\Of{\:\KW{of}\:}
\newcommand\Return{\:\KW{return}\:}
\newcommand\Rec{\KW{rec}\:}
\newcommand\With{\:\KW{with}\:}
\newcommand\Arr{\mathrel\mapsto}
\newcommand\TCArr{\mkern-10mu \Arr}
\newcommand\Coe{\KW{coe}\:}
\newcommand\Comp{\KW{comp}\:}
\newcommand\Qty{\mathrel\diamond}
$$
:::
bidirectional syntax. i like it.
$$
\begin{align*}
x,y,z,X,Y,Z &\EQ \dotsb & \text{term variables} \\
\iota &\EQ \dotsb & \text{dimension variables} \\
\ell &\EQ n & \text{universe levels ($n \in \mathbb{N}$)} \\
\L{a},\L{b},\L{c}, \text{etc} &\EQ \dotsb & \text{symbols} \\[.75em]
%
\pi,\rho,\phi,\sigma &\EQ 0 \Or 1 \Or \omega
& \text{quantities} \\[.75em]
%
q,r &\EQ \varepsilon \Or \iota & \text{dimensions} \\
\varepsilon &\EQ 0 \Or 1 & \text{dimension endpoints} \\[.75em]
%
s,t,A,B &\EQ \Type\ell & \text{types \& terms: universe} \\
&\OR (x \Qty \pi,\rho : A) \to B \Or \lambda x. t
& \text{functions} \\
&\OR (x \Qty \rho : A) \times B \Or \Tup{s, t}
& \text{pairs} \\
&\OR (x \Qty \rho,\phi : A) \WTy B \Or s \WTm t
& \text{inductive data} \\
&\OR \{ \overline{\L{a}_i}^i \} \Or \L{a}
& \text{enumerations} \\
&\OR \BoxTy\pi A \Or \BoxTm s
& \text{quantity} \\
&\OR s =_{\iota.A} t \Or \lambda\iota.s
& \text{equalities} \\
&\OR \underline{e}
& \text{elimination in term} \\[.75em]
%
e, f &\EQ x & \text{eliminations: variable} \\
&\OR f \: s
& \text{application} \\
&\OR \Case e \Return z. A \Of \Tup{x, y} \Arr s
& \text{unpairing} \\
&\OR \Rec e \Return z. A \With s
& \text{recursion} \\
&\OR \Case e \Return z. A \Of
\{ \overline{\L{a}_i \Arr s_i}^i \}
& \text{enumeration} \\
&\OR \Case e \Return z. A \Of \BoxTm x \Arr s
& \text{quantity} \\
&\OR f \: q
& \text{equality application} \\
&\OR \Coe (\iota.A)^q_{q'} \: s
& \text{coercion} \\
&\OR[\left] \Comp A^q_{q'} \: s \:
\left\{
\begin{aligned}
(r=0) & \Arr \iota.t_0 \\
(r=1) & \Arr \iota.t_1
\end{aligned}
\right\} \right.
& \text{composition} \\
&\OR[\left] \Case e \Return A \Of
\left\{
\begin{array}{ll}
\Type{} & \TCArr t_0 \\
\Pi \: X \: Y & \TCArr t_1 \\
\Sigma \: X \: Y & \TCArr t_2 \\
\KW{W} \: X \: Y & \TCArr t_3 \\
\KW{Enum} & \TCArr t_4 \\
\BoxType X & \TCArr t_5 \\
\KW{Eq} \: X \: X' \: y \: z \: z' & \TCArr t_6 \\
\end{array}
\right\} \right.
& \text{type case} \\
&\OR s : A
& \text{annotation}
\end{align*}
$$
__TODO wtf does all this cube stuff even mean. especially composition__
i'm going to use abbreviations like $A \to_\pi B$ for $(x \Qty \pi,0 : A) \to
B$, just $A$ for $z. A$ or $\iota. A$ in elim return types, etc for
non-dependent stuff. $\emptyset$ means $\{\,\}$.
a function type has two quantities attached to it, since unlike in qtt classique
we care about what's going on in types too. in $(x \Qty \pi,\rho : A) \to B$,
$x$ is used $\pi$ times in the body of a function of this type, and it's used
$\rho$ times in $B$ itself.
pairs $(x \Qty \rho : A) \times B$ only have one since it's just two things, the
first doesn't occur in the second at all, but we still care about what's going
on in $B$
w-types $(x \Qty \rho,\phi : A) \WTy B$ also have two quantities, but in
a different way. the $\rho$ still says how $x$ is used in $B$, but this time
$\phi$ says how $x$ is used in $t$ in a term like $s \WTm \lambda x. t$.
## examples of encodings
also possible syntax. TODO universe & quantity polymorphism obviously
```
-- empty type
Void : type 0 := {};
absurd : (A @ 0,1 : type 0) -> Void @ 1 -> A :=
fun A v => case v return A of {};
-- unit type
Unit : type 0 := {'tt};
swallow : (A @ 0,2 : type 0) -> Unit @ 1 -> A -> A :=
fun t x => case t return A of {'tt => x};
-- boolean type
Bool : type 0 := {'false; 'true};
-- use 'case' for 'if'
not : Bool @ 1 -> Bool :=
fun b => case b return Bool of {'false => 'true; 'true => 'false};
-- natural numbers
NatTag : type 0 := {'zero; 'suc};
NatBody : NatTag @ 1 -> type 0 :=
fun n => case n return type 0 of {'zero => Void; 'suc => Unit};
Nat : type 0 := (tag : NatTag @ 1,1) <|| NatBody tag;
zero : Nat := 'zero <| absurd;
suc : Nat @ 1 -> Nat := fun n => 'suc <| fun t => swallow t n;
elimNat : (P @ inf,0 : Nat @ inf -> type 0) ->
(Z @ inf,0 : P zero) ->
(S @ inf,0 : (n @ 1,2 : Nat) -> P n -> P (suc n)) ->
(n @ inf,1 : Nat) -> P n :=
fun P Z S n =>
rec n return n₀. P n₀ with fun tag =>
case tag
return t. (f @ inf,2 : NatBody t @ 0 -> Nat) ->
(IH @ inf,0 : (b @ 1 : NatBody t) -> P (f b)) ->
P (t <| f)
of {'zero => fun _ _ => Z;
'suc => fun f IH => S (f 'tt) (IH 'tt)}
```
or something.&#x3000;:ghost: eliminators :ghost: w-types :ghost: \
it's a core language and it's possible to translate a good language to
these primitives, so try not to worry that it is impossible to write an
elimination for a w-type correctly first try.
btw, you can see in `elimNat` that the part after `with` is a partially applied
function. this seems to be the most common pattern for dependent eliminators,
which is why it's `rec n with s` instead of something like
`case n of (tag <| f, IH) => s[tag,f,IH]`.
getting rid of those `inf`s (and those in `elimNat`'s type) will need dependent
quantities arrrg
# type rules
:::defs
$$
\newcommand\Q{\mathrel|}
\newcommand\Z{\mathbf0}
\newcommand\Chk{\mathrel\Leftarrow}
\newcommand\Syn{\mathrel\Rightarrow}
\newcommand\Ty[3]{\frac{\begin{matrix}#2\end{matrix}}{#3}\;\mathbfsf{#1}}
\newcommand\AA{\textcolor{Purple}}
\newcommand\BB{\textcolor{OliveGreen}}
\newcommand\CC{\textcolor{RoyalBlue}}
\newcommand\DD{\textcolor{Bittersweet}}
\newcommand\EE{\textcolor{WildStrawberry}}
\newcommand\FF{\textcolor{PineGreen}}
\newcommand\GG{\textcolor{RedViolet}}
\newcommand\HH{\textcolor{RedOrange}}
$$
:::
:::rulebox
$$
\begin{gather}
\Psi \Q \Delta \Q \Gamma \vdash
\AA{s} \Chk \BB{A}
\dashv \AA{\delta_s}; \BB{\delta_A} \\[.1em]
\Psi \Q \Delta \Q \Gamma \vdash
\AA{e} \Syn \BB{A}
\dashv \AA{\delta_e}; \BB{\delta_A} \\
\end{gather}
$$
:::
ok. here we go. tybes. get ready for Density. to try and make things a little
easier to pick out, quantities will be colour coded with where they came from.
some of the colours are too similar. sorry.
$$
\begin{align*}
\Gamma &\EQ \cdot \Or \Gamma, x : A
& \text{type context} \\
\delta &\EQ \cdot \Or \delta, \pi x
& \text{quantity vector} \\
\Delta &\EQ \cdot \Or \Delta, \delta
& \text{quantity context} \\
\Psi &\EQ \cdot \Or \Psi, \iota \Or \Psi, q=r
& \text{cube}
\end{align*}
$$
a context $\Gamma$ is a list of types, as always.
a quantity context $\Delta$ is a triangle of how many times each type in
$\Gamma$ uses all the previous ones. $\delta$ is a single vector of quantities,
used for counting the quantities of everything in the subject and the subject's
type. $0\Gamma$ means a quantity vector with the variables of $\Gamma$, with
everything set to zero.
a :ice_cube: cube :ice_cube: collects the dimension variables in scope, and
constraints between them.
the grtt paper (which doesn't have cubes) has this example (but written slightly
differently):
$$
\left(\begin{smallmatrix}
\\
1 A \\
1 A & 0 x \\
\end{smallmatrix}\right) \Q
(A: \Type0, x: A, y: A) \vdash
\AA{x} \Syn \BB{A}
\dashv \AA{(0A,1x,0y)}; \BB{(1A,0x,0y)}
$$
in $\Delta$ (the big thing at the beginning):
- $A$ is the first element, so there is nothing it could mention, and it has
just an empty list $()$.
- $x: A$ contains $A$ once, which is the only option, so it has $(1A)$.
- $y: A$ also mentions $A$, but not $x$, so it's $(1A,0x)$.
after the type of the subject are two more quantity vectors. the first is how
the context elements are used in the subject itself, and the second how they're
used in its type.
by the way the reason i write the judgements this way with those two vectors at
the end is because they are outputs, so now everything before $\vdash$ is an
input, and everything after $\dashv$ is an output. whether the type is an input
or output varies: since the syntax is bidirectional, $s \Chk A$ means that
the term $s$ can only be checked against a known $A$ (so it's an input), and
$e \Syn A$ means that for an elimination $e$ the type $A$ can be inferred (so
it's an output).
## universes
$$
\Ty{type}{
\AA{\ell} < \BB{\ell'}
}{
\Psi \Q \Delta \Q \Gamma \vdash
\AA{\Type\ell} \Chk \BB{\Type{\ell'}}
\dashv 0\Gamma; 0\Gamma
}
$$
universes are cumulative. since we have a known universe to check against, why
not.
## functions
$$
\Ty{fun}{
\Psi \Q \Delta \Q \Gamma \vdash
\AA{A} \Chk \Type\ell
\dashv \AA{\delta_A}; 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\BB{B} \Chk \Type\ell
\dashv (\BB{\delta_B}, \EE\rho x); (0\Gamma, 0x) \\
}{
\Psi \Q \Delta \Q \Gamma \vdash
(x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B} \Chk \Type\ell
\dashv (\AA{\delta_A} + \BB{\delta_B}); 0\Gamma
}
$$
in formation rules like this, the type-level quantities being all zero doesn't
actually have to be checked, since everything is being checked against
$\Type\ell$ which never uses variables. if universe polymorphism starts existing
that will have to be tweaked in some way. maybe rules like __lam__ will have
$\AA{\delta_A}; \FF{\delta_\ell}$ in the output of the first premise, and
$\CC{\delta_t}; (\AA{\delta_A} + \BB{\delta_B} + \FF{\delta_\ell})$ in the
conclusion. something like that.
$$
\Ty{lam}{
\Psi \Q \Delta \Q \Gamma \vdash
\AA{A} \Chk \Type\ell
\dashv \AA{\delta_A}; 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\CC{t} \Chk \BB{B}
\dashv (\CC{\delta_t}; \DD\pi x); (\BB{\delta_B}; \EE\rho x) \\
}{
\Psi \Q \Delta \Q \Gamma \vdash
\lambda x. \CC{t} \Chk (x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B}
\dashv \CC{\delta_t}; (\AA{\delta_A} + \BB{\delta_B})
}
$$
$$
\Ty{app}{
\Psi \Q \Delta \Q \Gamma \vdash
\FF{f} \Syn (x \Qty \DD\pi,\EE\rho : \AA{A}) \to \BB{B}
\dashv \FF{\delta_f}; (\AA{\delta_A} + \BB{\delta_B}) \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\BB{B} \Chk \Type\ell
\dashv (\BB{\delta_B}, \EE\rho x); (0\Gamma, 0x) \\
\Psi \Q \Delta \Q \Gamma \vdash
\CC{s} \Chk \AA{A}
\dashv \CC{\delta_s}; \AA{\delta_A} \\
}{
\Psi \Q \Delta \Q \Gamma \vdash
\FF{f} \: \CC{s} \Syn \BB{B}[\CC{s}/x]
\dashv (\FF{\delta_f} + \DD\pi\CC{\delta_s});
(\BB{\delta_B} + \EE\rho\CC{\delta_s})
}
$$
the head of an application needs to inferrable, but a lambda isn't. so a
β redex is actually going to be something like
$\big((\lambda x. t) : (x \Qty \pi,\rho : A) \to B\big) \: t$
with an annotation on the head. probably from an inlined definition with a type
signature.
## pairs
$$
\Ty{pair}{
\Psi \Q \Delta \Q \Gamma \vdash
\AA{A} \Chk \Type\ell
\dashv \AA{\delta_A}; 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\BB{B} \Chk \Type\ell
\dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
}{
\Psi \Q \Delta \Q \Gamma \vdash
(x \Qty \EE\rho : \AA{A}) \times \BB{B} \Chk \Type\ell
\dashv (\AA{\delta_A} + \BB{\delta_B}); 0\Gamma
}
$$
$$
\Ty{comma}{
\Psi \Q \Delta \Q \Gamma \vdash
\CC{s} \Chk \AA{A}
\dashv \CC{\delta_s}; \AA{\delta_A} \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\BB{B} \Chk \Type\ell
\dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
\Psi \Q \Delta \Q \Gamma \vdash
\DD{t} \Chk \BB{B}[\CC{s}/x]
\dashv \DD{\delta_t}; (\BB{\delta_B} + \EE\rho\CC{\delta_s}) \\
}{
\Psi \Q \Delta \Q \Gamma \vdash
\Tup{\CC{s}, \DD{t}} \Chk (x \Qty \EE\rho : \AA{A}) \times \BB{B}
\dashv (\CC{\delta_s} + \DD{\delta_t}); (\AA{\delta_A} + \BB{\delta_B})
}
$$
$$
\Ty{casepair}{
\Psi \Q \Delta \Q \Gamma \vdash
\FF{e} \Syn (x \Qty \EE\rho : \AA{A}) \times \BB{B}
\dashv \FF{\delta_e}; (\AA{\delta_A} + \BB{\delta_B}) \\
\Psi \Q \Delta \Q \Gamma \vdash
\AA{A} \Chk \Type\ell
\dashv \AA{\delta_A}; 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A}) \Q (\Gamma, x : \AA{A}) \vdash
\BB{B} \Chk \Type\ell
\dashv (\BB{\delta_B}, \EE\rho x); 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A} + \BB{\delta_B})
\Q (\Gamma, z: (x \Qty \EE\rho : \AA{A}) \times \BB{B}) \vdash
\GG{C} \Chk \Type\ell
\dashv (\GG{\delta_C}, \HH\sigma z); 0\Gamma \\
\Psi \Q (\Delta, \AA{\delta_A}, (\BB{\delta_B}, \EE\rho))
\Q (\Gamma, x : \AA{A}, y : \BB{B}) \vdash
\CC{s} \Chk \GG{C}[\Tup{x, y}/z]
\dashv (\CC{\delta_s}, \DD\pi x, \DD\pi y);
(\GG{\delta_C}, \HH\sigma x, \HH\sigma y)
}{
\Psi \Q \Delta \Q \Gamma \vdash
(\Case \FF{e} \Return z. \GG{C} \Of \Tup{x, y} \Arr \CC{s})
\Syn \GG{C}[\FF{e}/z]
\dashv (\CC{\delta_s} + \DD\pi\FF{\delta_e});
(\GG{\delta_C} + \HH\sigma\FF{\delta_e})
}
$$
## inductive data
:^)
## enumerations
$$
\Ty{enum}{}{
\Psi \Q \Delta \Q \Gamma \vdash
\{ \overline{\L{a}_i}^i \} \Chk \Type\ell
\dashv 0\Gamma; 0\Gamma
}
$$
$$
\Ty{symbol}{
\L{a} \in \overline{\L{a}_i}^i
}{
\Psi \Q \Delta \Q \Gamma \vdash
\L{a} \Chk \{ \overline{\L{a}_i}^i \}
\dashv 0\Gamma; 0\Gamma
}
$$
$$
\Ty{caseenum}{
\Psi \Q \Delta \Q \Gamma \vdash
\FF{e} \Syn \{\L{a}_i\}
\dashv \FF{\delta_e}; 0\Gamma \qquad
\overline{
\Psi \Q \Delta \Q \Gamma \vdash
\CC{s_i} \Chk \AA{A}[\L{a}_i/z]
\dashv \CC{\delta_s}; \AA{\delta_A}
}^i
}{
\Psi \Q \Delta \Q \Gamma \vdash
\Case \FF{e} \Return z. \AA{A} \Of \{ \overline{\L{a}_i \Arr \CC{s_i}}^i \}
\dashv (\FF{\delta_e} + \CC{\delta_s}); \AA{\delta_A}
}
$$
__TODO__ the rest

274
posts-wip/rainbow-quox.md Normal file
View file

@ -0,0 +1,274 @@
---
title: rainbow quox
date: 2024-11-17
tags: [computer, website, fursona]
summary: q.t. colour scheme generator
...
so how about that regular posting, huh. ha ha ha
i haven't been up to much unusual. [drawing], mostly. i installed [nixos] on both my computers and it's going pretty well so far [(less than a week)]{.note}, but every computer toucher does that at some point, so, whatever.
[drawing]: https://gallery.niss.website
[nixos]: https://nixos.org
anyway, to the point.
:::banner
[go here if you just want to play with the thing][thing]
<!-- TODO add this link!!! -->
:::
# the point {.unnumbered}
the animal-inclined might know that [q.t.][qt] can change its colour any time it wants. if you click that link you can clearly see i have some tendencies, but it can in theory be anything. so something i have wanted for a while is a page where you can click a button and get a bespoke randomly-generated quox theme of your very own.
so i did that.
:::aside
you can also skip to [what i _actually_ ended up doing](#actual), if you don't care about the false starts.
:::
[qt]: https://gallery.niss.website/by-any/#qt
# doing that
![this is the image i'm starting from.](rainbow-quox/front.avif){.floating .expandable .nobg .shaped}
pretty much what i want to do, at least to begin with, is take the original colours of the image and move the hues around at random.
if you look at [mdn], you might see this interesting [`hue-rotate()`][hr] thing that might do what i want. let's have a look.
[mdn]: https://developer.mozilla.org/en-US/docs/Web/CSS
[hr]: https://developer.mozilla.org/en-US/docs/Web/CSS/filter-function/hue-rotate
> **Note:** `hue-rotate()` is specified as a matrix operation on the RGB color. It does not actually convert the color to the HSL model, which is a non-linear operation. Therefore, it may not preserve the saturation or lightness of the original color, especially for saturated colors.
well that doesn't sound very promising. but maybe it'll be fine, so let's try it. first, separate the pictures from [q.t.'s refsheet][ref] into bits. like this.
[ref]: https://gallery.niss.website/main/niss/2024-06-27-qt
![sock stripes, belly, main body, and masks/claws should change independently from each other. the other colours don't change.](rainbow-quox/pieces1.avif){.expandable .lightbg}
now let's layer them back on top of each other with some css.
```html
<!doctype html>
<style>
#container {
width: 100%; position: relative;
img { position: absolute; inset: 0; }
}
</style>
<div id=container>
<img src=outer.png> <img src=belly.png> <img src=eyes.png>
<img src=tongues.png> <img src=collars.png> <img src=masks.png>
<img src=socks.png> <img src=stripes.png> <img src=lines.png>
</div>
```
![took a hot shower for too long](rainbow-quox/red.avif){.floating .left .nobg .expandable .shaped}
ok, next, actually try to do the hue stuff. to check it works at all, i shoved everything to hue 0° (using krita's _hue HSL_ blend mode), and used `hue-rotate()` to change it back to the 'main' colour of each region---it won't look exact, but it'll be close.
```css
#container img { filter: hue-rotate(var(--hue)); }
#outer { --hue: 273deg; } #belly { --hue: 26deg; }
#eyes { --hue: 133deg; } #masks { --hue: 284deg; }
#stripes { --hue: 188deg; } #lines { --hue: 273deg; }
/* also add the id to each image */
```
right?
![oh](rainbow-quox/dark.avif){.expandable .nobg}
well that's no good at all. i guess that warning was serious.
# ok what about blend modes
![shoutout to the four different types of "soft light"](rainbow-quox/blends.avif){.floating .expandable}
all right, fine. what else. as a chronic over-user of `overlay`, i can certainly tell you that css has a few [blending modes][bm]. not as many as krita, which has approximately "too many", but enough for most purposes. one of them is `hue`. how about that.
[bm]: https://developer.mozilla.org/en-US/docs/Web/CSS/blend-mode
this takes a bit more messing, because i need to create a flood fill of one of the colours from that layer, and blend with that. so how about an SVG filter, i guess. or, six SVG filters---one for each filter, since you can't parametrise them.
time to copy and paste the same five lines six times. yaaaaaaaaay
![ugh](../images/bub_flop.png){.bigemoji .pixel} \
```svg
<svg style="position: absolute">
<filter id="fouter">
<feFlood result="hue" flood-color="#57267e" />
<feBlend in="hue" in2="SourceGraphic" mode="hue" result="res" />
<!-- ↓ without this the background will also be filled in -->
<feComposite in="res" in2="SourceGraphic" operator="in" />
</filter>
<!-- …and same for the others, with different flood-colors -->
</svg>
```
```css
#outer { filter: url(#fouter); }
/* …etc… */
```
and…
![also no](rainbow-quox/dark2.avif){.expandable .nobg}
i was expecting at least the same thing, but a different, also wrong, result is pretty cool.
# drastic measures {#actual}
ok, enough messing around, time to bite the bullet. separate every single colour into its own layer, and use those as _masks_ for colour fills.
now the pieces look like _this_:
![this image is probably incomprehensible now. it doesn't really matter---the main thing is that there are seventeen different layers.](rainbow-quox/pieces2.avif){.expandable .lightbg}
the colours in the images no longer matters, only the alpha channel. [(except for the eyes.)]{.note} each one is just a mask over a background fill of the right colour.
```css
@layer {
#container { position: relative; width: 90vw; aspect-ratio: 3439/2240; }
#container div { position: absolute; inset: 0; mask-size: contain; }
}
@layer {
#static { background: url(front/static.png) 0 0 / contain; }
#eye-shine {
background: url(front/eyes.png) 0 0 / contain;
mix-blend-mode: luminosity;
}
/* the others all look like this: */
#spines {
background: oklch(30.77% 0.1306 var(--hue)); --hue: 298.19;
mask-image: url(front/spines.png);
}
/* etc… */
}
```
```html
<div id=container>
<!-- divs not images now. the images are all in the background properties -->
<div class=part id=static></div>
<div class=part id=spines></div>
<div class=part id=stripes></div>
<!-- etc… -->
<div id=eye-shine></div>
</div>
```
since the hue is separated out into a variable, i can just do:
```js
for (const elem of document.getElementsByClassName('part')) {
elem.style.setProperty('--hue', Math.random() * 360);
}
```
and instantly i have _something_ working. i used `oklch` because it was more likely than `hsl` or whatever to keep the colours the same kind of distance from each other, since that is what it's designed for.
![some of these are kinda promising already??](rainbow-quox/quoxes1.avif){.expandable .hasborder}
# keeping the colours in sync
so as of last year, most browsers got a thing called [relative colours]. if you have an existing colour `--hi`, you can rotate its hue by half a turn by saying something like
[relative colours]: https://developer.mozilla.org/en-US/docs/Web/CSS/CSS_colors/Relative_colors
```css
:root {
--hi: #ea9aa1;
--wow: oklch(from var(--hi) l c calc(h + 180));
}
```
---
header-includes: |
<style>
#relcolor {
max-width: 20em; margin: auto;
display: grid; grid-template-columns: 1fr 1fr; gap: .5em;
font-weight: bold;
--hi: #ea9aa1; --wow: oklch(from var(--hi) l c calc(h + 180));
}
#relcolor div {
text-align: center; font-size: 125%;
padding: .4em; border-radius: .5em;
color: black;
background: var(--bg);
border: 4px solid oklch(from var(--bg) .25 75% h);
}
#hi { --bg: var(--hi); }
#wow { --bg: var(--wow); }
</style>
...
<div id=relcolor>
<div id=hi>\--hi</div>
<div id=wow>\--wow</div>
</div>
you're taking the value of `var(--hi)`, keeping the lightness and chroma channels the same, and adding 180° to the hue.
:::aside
that's not quite true. safari, as always, does it slightly wrong. according to the spec, all channels in a relative colour must be dimensionless, but in safari, the hue is an `<angle>`. other browsers, following the spec correctly, _don't allow_ that. so you _actually_ have to write
```css
:root {
--hi: #ea9aa1;
--wow: oklch(from var(--hi) l c calc(h + 180));
}
@supports (color: oklch(from red l c 10deg)) {
:root { --wow: oklch(from var(--hi) l c calc(h + 180deg)); }
}
```
thanks apple!
:::
so based on that, i can pick one initial colour and base all the others on it. like
```css
:root {
/* these aren't attempting to be the same colours, just guessing something
that MIGHT look nice */
--outer: #57267e;
--spines: oklch(from var(--outer) calc(l * .75) calc(c * 1.25) h);
--vitiligo1: oklch(from var(--outer) calc(1 - (1 - l)/4) calc(c / 2) h);
/* static l/c values because the socks are always some pale colour */
--stripes: oklch(from var(--outer) .9 12.5% calc(h + 120));
--cuffs: oklch(from var(--stripes) .8 25% h);
/* etc */
}
.outer { background: var(--outer); mask-image: url(front/outer.png); }
/* etc */
```
so after guessing a bunch of relative colours, i ended up with this:
![yeah that looks ok for a first try.](rainbow-quox/relative.avif){.expandable .nobg}
## notes for niss. if this goes online i fucked up
- palette types
- randomise distance between analogous colours
- light, dark, light-dark, dark-light (belly vs outer)
- reinstate chaos mode
- can you set the random seed in the browser
- no. anyway the algorithm might be different
- make yr own
- or <https://stackoverflow.com/a/47593315>. whatever
- if so: use that to make palette permalinks

BIN
posts-wip/rainbow-quox/blends.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 55 KiB

BIN
posts-wip/rainbow-quox/dark.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 67 KiB

BIN
posts-wip/rainbow-quox/dark2.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 63 KiB

BIN
posts-wip/rainbow-quox/front.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 153 KiB

BIN
posts-wip/rainbow-quox/pieces1.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 418 KiB

BIN
posts-wip/rainbow-quox/pieces2.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 536 KiB

BIN
posts-wip/rainbow-quox/quoxes1.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 652 KiB

BIN
posts-wip/rainbow-quox/red.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 152 KiB

BIN
posts-wip/rainbow-quox/relative.avif Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 210 KiB