rhi/blog
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity
blog/posts-wip/quox-type-system.md

514 lines
16 KiB
Markdown
Raw Normal View History

a bunch of stuff sorry
2023-12-27 19:00:25 -05:00
---
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 #⁠UIP⁠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
Reference in a new issue Copy permalink