514 lines
16 KiB
Markdown
514 lines
16 KiB
Markdown
|
---
|
|||
|
|
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.　: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
|