16 KiB
title: quox's type system tags: [quox, programming] date: 2021-07-26 ...
main inspirations:
- quantitative type theory
(2018)
- mostly conor's version, 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 (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 (2007)
- nice middle ground between intensional and extensional type theory. you get stuff like funext in a decidable setting
- xtt
("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 #UIPCrew
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 (😰), cubes (😰 😰 😰), 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. 👻 eliminators 👻 w-types 👻
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 infs (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 🧊 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):
Ais the first element, so there is nothing it could mention, and it has just an empty list().x: AcontainsAonce, which is the only option, so it has(1A).y: Aalso mentionsA, but notx, 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