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

a bunch of stuff sorry

Browse source
This commit is contained in:
rhiannon morris 2023-12-28 01:00:25 +01:00
parent 2910daf0c6
commit 32edbb1816
33 changed files with 4874 additions and 90 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -0,0 +1,315 @@
---
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}

1014
posts-wip/2023-06-12-algorithmic-xtt.md Normal file
View file

File diff suppressed because it is too large Load diff

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

@ -0,0 +1,112 @@
---
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}

177
posts-wip/2023-10-25-quox.md.old Normal file
View file

@ -0,0 +1,177 @@
---
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](https://en.wiktionary.org/wiki/hot_minute)&ensp;<i>n.</i> {.unnumbered}
1. A long period of time.
2. A short period of time.
3. An unspecified period of time.
:::
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. it has a *closed type universe*. you don’t define new datatypes, but the language gives you building blocks to put them together.
2. *[q]{.qtt-q}uantitative type theory* (qtt) [@nuttin; @qtt] is a nice combination of dependent types, resource tracking, and erasure of stuff like proofs.
3. *[x]{.xtt-x}tt* [@xtt], which `*i sure hope i remember to come back and add this!*`
- the closed type universe is a consequence of xtt (as well as its kinda-predecessor ott [@ott-now]), but i decided to just run with it.
- “xtt” stands for “extensional type theory”, but it’s not _that_ extensional type theory. i know. not my fault.
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
<figure class=floating id=panqt>
<div><img src=../images/panqt.nobg.png srcset='../images/panqt.nobg2x.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 if they find out about it'></div>
<figcaption>
sometimes i am also a quox. or three, depending on how you count.
</figcaption>
</figure>
4. *bidirectional type checking* [@bidi] `*this one too*`
5. crude-but-effective stratification [@crude; @crude-blog] for dealing with universes. `*does this need more detail too?*`
6. *written in idris2*. that doesn’t really have much impact on the language itself, other than the compilation process, but i’m enjoying using a dependently typed language for something substantial. even if it’s one you’re not currently supposed to be using for anything substantial. also currently it spits out scheme, like idris, because that was easy.
7. all the non-ascii syntax is [optional], but i like it.
[optional]: https://git.rhiannon.website/rhi/quox/wiki/ascii-syntax
as for what it _doesn’t_ have: any but the most basic of conveniences. sorry.
# dependent types
there are lots of languages with dependent types—well, quite a few—so i won’t spend too much time on this.
`*but still something*`
# closed type universe
instead of having datatypes like in normal languages, in quox you get the basic building blocks to make them. the main building blocks are functions, pairs, enumerations, equality types, strings, and natural numbers. some sort of syntactic sugar to expand a datatype declaration into this representation _is_ something i want to add, but it'd be in the pretty distant future.
:::aside
_at the moment_, natural numbers are the only recursion possible. so you can define types with the same recursive structure, like lists, but binary trees and stuff are not _currently_ possible, until i replace them with something more general. probably w-types [@nlab-wtype].
:::
but right now you can define a few types like this. see [qtt](#qtt) below for what all the `0`s and `ω`s mean. due to the lack of generic recursion, but the presence of _natural numbers_ specifically, a list is a length, followed by a nested tuple of that length (terminated by `'nil`).
```quox
def0 Vec : ℕ → ★ → ★ =
λ n A ⇒
case n return ★ of {
zero ⇒ {nil};
succ p, As ⇒ A × As
} -- ↖ As = Vec p A
def0 List : ★ → ★ = λ A ⇒ (n : ℕ) × Vec n A
def Nil : 0.(A : ★) → List A = λ A ⇒ (0, 'nil)
def Cons : 0.(A : ★) → A → List A → List A =
λ A x xs ⇒ case xs return List A of { (len, xs) ⇒ (succ len, x, xs) }
def NilS = Nil String
def ConsS = Cons String
def example = ConsS "im" (ConsS "gay" NilS)
def0 example-eq : example ≡ (2, "im", "gay", 'nil) : List String =
refl (List String) example
```
you might have noticed that i didn't write the eliminator. that is because they are kind of ugly. if you want to see it anyway you can find it in [the example folder][ex].
[ex]: https://git.rhiannon.website/rhi/quox/src/commit/246d80eea2/examples/list.quox#L12-L25
# qtt
sometimes, values of some type can only be used in certain ways to make sense. this is hardly controversial; if you do this with
a problem that dependent types used to have a lot is that the blurring of compile-time and run-time data can lead to more being retained than necessary.
`*is there an example that has superlinear junk data without resorting to peano naturals or some shit*`
consider this vector (length-indexed list) definition from a _hypothetical language_ with normal inductive types.
```agda
data Vect (A : ★) : ℕ → ★ where
[] : Vect A 0
_∷_ : (n : ℕ) → A → Vect A n → Vect A (succ n)
```
in a totally naive implementation, `cons` would store `n`, the length of its tail (and maybe even some kind of representation of `A` too). so a three element list would look something like
# xtt
`*mention about type-case and the closed universe*`
# bidirectional type checking
# references {#refs}

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

@ -0,0 +1,513 @@
---
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