Here’s the next episode in my story of algorithmic rules. I’m going to define a bidirectional type system and its definitional equality. Indeed, I’m going to define a bidirectional type system by its definitional equality. The judgments form a command-response system
data EqS : Set where
_&_!-_:>_≡_ : (x : Lev)(G : Cx x)(T t t’ : Tm nm) → EqS
_&_!-_≡_ : (x : Lev)(G : Cx x)(w w’ : Tm ne) → EqSEqT : EqS → Set
EqT (x & G !- T :> t ≡ t’) = One
EqT (x & G !- w ≡ w’) = Tm nm
Judgment
x & G !- T :> t ≡ t’
holds if in context G, type T admits that normal terms t and t’ are equal. The x is a name supply, allowing us to generate fresh names; G is a context assigning a type to every free variable (de Bruijn level less than x). The output from such a typechecking process is just an acknowledgement: EqT indicates that the One-element set is the relevant response type. Meanwhile, we don’t need a type to test if neutral terms are equal; we may ask
x & G !- w ≡ w’
and expect as response the normal form of the type that both w and w’ possess, should they indeed prove to be equal. Correspondingly EqT delivers Tm nm as the response type in that case.
Of course, this being a dependent type system, we shall need to do computation, and not all terms will be equal, so we shall need to abort. Correspondingly, the side-conditions we shall need are given and interpreted thus:
EqA : Set
EqA = CompA + CompS
EqB : EqA -> Set
EqB = CompB <?> CompT
EqC : (a : EqA)(b : EqB a) -> Set
EqC = CompC <?> Go CompC compf
where _<?>_ is the usual eliminator for sums: (f <?> g) (inl s) = f s, (f <?> g) (inr t) = g t. Recall that CompA allows us to abort (with no response) and CompS allows us to eliminate normal forms and instantiate free variables (and get a normal form back). We use the rules from the previous post, generated by the monadic program compf, to explain when these side-conditions hold. (Container fans will note that I’ve just formed the sum of (CompA <| CompB) with (CompS <| CompT). Command-response systems are delightfully compositional.)
With this setup, we can now say that
EQ = Prog EqA EqB EqS EqT
is the monad in which we’ll be checking equality.
Typechecking, here, is just the diagonal of equality. We say that T accepts t in context G just if
x & G !- T :> t ≡ t
holds, and we infer type T for some neutral w if
x & G !- w ≡ w
holds with response T.
We’re not quite ready to get cracking. I’d better just fill in how contexts work. It’s cheap, cheerful, and under review. Contexts are left-nested tuples of types (i.e. normal form terms), one for each free variable.
Cx : Lev → Set
Cx ze = One
Cx (su x) = Cx x * Tm nm
As befits de Bruijn levels, we count from global to local, even though the local end is the more accessible. In a Cx (su x), the most local free variable is x. Lookup (which may fail with a bounds error) thus tests numerical equality at each step (less efficient than subtracting just once and counting the other way, but to the point).
get : (x y : Lev) → Cx x → One + Tm nm
get ze y _ = inl _
get (su x) y (G , S) with nq x y
… | inl _ = inr S
… | inr _ = get x y G
One more thing. It’ll help to be able to match on responses inline, especially when taking apart a Π-type in the application rule. Let’s cook up the right gadget
mustPI : {X : Set} → (Tm nm → Tm nm → EQ X) →
Tm nm → EQ X
mustPI f (PI ! S , T , []) = f S T
mustPI _ _ = inl abort !! \ ()
So, let’s get on with it. The definition of
eqf : (s : EqS) -> EQ (EqT s)
gives the rules of the system as a monadic program which invokes premises and side-conditions, then aborts or responds.
Let’s start by checking equality of canonical sets. I’m being a Set-in-Set criminal, so
eqf (x & G !- SET ! [] :> SET ! [] ≡ SET ! []) =
ret _
Meanwhile, Π-types have domain set and a range family. Equality is structural. Once we’ve checked the domains agree, it makes sense to check that the ranges are equal families over the domain.
eqf (x & G !- SET ! [] :> PI ! S , T , [] ≡ PI ! S’ , T’ , []) =
x & G !- SET ! [] :> S ≡ S’ ?? \ _ →
x & G !- PI ! S , lam (SET ! []) , [] :> T ≡ T’ ?? \ _ →
ret _
Equality of functions is checked by η-expansion. We speculate a fresh variable of the domain type, then compare what the functions do with it, in the suitably specialised range type. To do the specialisation, we invoke elimination. If T, t or t’ is a lam-abstraction, this just replaces the bound variable by the free variable x. You can apply any normal form (even an ill-typed one) to a free variable without fear of setting off a nonterminating computation! So it’s ok to use this rule in typechecking, as well as in equality checking for the already well-typed.
eqf (x & G !- PI ! S , T , [] :> t ≡ t’) =
inr (su x !- T %% [ par x ] /) !! \ U →
inr (su x !- t %% [ par x ] /) !! \ u →
inr (su x !- t’ %% [ par x ] /) !! \ u’ →
su x & G , S !- U :> u ≡ u’ ?? \ _ →
ret _
To compare embedded neutral terms at a given type, change direction and compare them, synthesizing their shared type. Then check that the latter is the type you wanted!
eqf (x & G !- T :> [ w ] ≡ [ w' ]) =
x & G !- w ≡ w’ ?? \ S ->
x & G !- SET ! [] :> S ≡ T ?? \ _ ->
ret _
For type synthesizing equality, let’s start with free variables. We’d better have two copies of the same variable, and it had better be in the context. The context tells us its type.
eqf (x & G !- par p ≡ par p’) with nq p p’
eqf (x & G !- par p ≡ par .p) | inl refl with get x p G
eqf (x & G !- par p ≡ par .p) | inl refl | inl _ = inl abort !! \ ()
eqf (x & G !- par p ≡ par .p) | inl refl | inr S =
ret S
eqf (x & G !- par p ≡ par p’) | inr _ = inl abort !! \ ()
To check applications for equality, first compare the functions, synthesizing their type. It had better be a Π type. The arguments had better agree in the domain, and we can then apply the range to synthesize the type of the whole thing.
eqf (x & G !- w % s / ≡ w’ % s’ /) =
x & G !- w ≡ w’ ?? mustPI \ S T ->
x & G !- S :> s ≡ s’ ?? \ _ ->
inr (x !- T %% s /) !! \ U ->
ret U
No other equality judgments hold.
eqf _ = inl abort !! \ ()
And that’s it. The eqf function explains how equality-checking (and thus typechecking) problems decompose in a syntax-directed way. The relation Go EqC eqf gives us both directions of equality, and hence both directions of typechecking.
But that’s not quite it. We can actually run this typechecker if we give it something to recurse on. There’s a ‘gasoline-driven’ implemention for any relation defined with Go, where
Gas = Nat
Much like the step-indexing folk do, the idea is to burn one unit of gas every time you run out of structurally smaller things to do recursion on. Of course, you risk an out-of-gas exception!
I think I’d better show you how I’m managing monads here: it’s just dumb dictionary-passing.
record Monad (F : Set → Set) : Set1 where
constructor monad
field
re : {X : Set} → X → F X
bi : {S T : Set} → F S → (S → F T) → F T
open Monad public
Now I can run a gas-driven judgment-checker in any monad for which (a) I know how to splutter out of gas and fail, and (b) I have a gas-driven checker for the side-conditions.
mutual
gasGo : {M : Set → Set} → Monad M →
(splut : {X : Set} → M X) →
forall {A B S T}{C : (a : A) → B a → Set} →
(side : Gas → (a : A) -> M (Σ (B a) (C a))) →
(f : (s : S) → Prog A B S T (T s)) →
Gas → (s : S) → M (Σ (T s) \ t → Go C f s t)
gasGo {M} m splut {C = C} side f n s =
bi m (help (f s) n) (un \ t g → re m (t , < g >))
where
Note that I’m not just computing the responses, but also the derivations, in a dependent pair. Correspondingly, I need the same of side, the parameter which runs side-conditions. I make use of uncurry (or un, for short) to unpack these pairs inline. Of course, the work is done by a helper function which interprets the monadic computation, f s.
help : {X : Set}(p : Prog _ _ _ _ X) →
Gas → M (Σ X \ x → [ C ! Go C f ] p => x)
If we’re out of gas, we splut.
help p ze = splut
If we’ve still got some gas, we compute recursively through the program structure, invoking side for side conditions, help for continuations, and gasGo with one gallon less for recursive checks. If we ever reach ret, hurrah!
help (ret x) (su n) = re m (x , refl)
help (a !! k) (su n) =
bi m (side (su n) a) (un \ b c →
bi m (help (k b) (su n)) (un \ t h →
re m (t , (b , c , h))))
help (s ?? k) (su n) =
bi m (gasGo m splut side f n s) (un \ t h →
bi m (help (k t) (su n)) (un \ u j →
re m (u , (t , h , j))))
Let’s roll ourselves a monad:
data Run (X : Set) : Set where
abort noGas : Run X
ret : X → Run XmoRun : Monad Run
…
Now we can do computations
compN : Gas → (s : CompS) → Run (Σ (CompT s) (Go CompC compf s))
compN = gasGo moRun noGas (\ _ _ → abort) compf
I had to check this
bad = compN big
(ze !- (lam [ var ze % [ var ze ] / ]) %%
(lam [ var ze % [ var ze ] / ] /))
and yes, we run out of gas.
Given that we can compute, we can test equality. Apologies for brutal point-free plumbing (infix – is the S combinator): Agda’s implicit syntax does take some persuading sometimes (and no, you can’t replace the remaining \ _ → with k).
eqN : Gas -> (s : EqS) → Run (Σ (EqT s) (Go EqC eqf s))
eqN = gasGo moRun noGas (k _<?>_ – k (\ _ → abort) – compN) eqf
The point, though, is that just as we used the computation judgment for equality side-conditions, we use the gas-driven computer to run those computational side-conditions. Typechecking is a special case:
tyN : Gas -> (T t : Tm nm) →
Run (Σ One (Go EqC eqf (ze & _ !- T :> t ≡ t)))
tyN n T t = eqN n (ze & _ !- T :> t ≡ t)
I ran some tests. Everything’s AOK.
IDTY : Tm nm
IDTY = PI ! (SET ! []) , lam
(PI ! [ var ze ] , lam [ var (su ze) ] , []) , []
idtm : Tm nm
idtm = lam (lam [ var ze ])TEST = tyN big (SET ! []) IDTY
test = tyN big IDTY idtm
So, what have we got here? A method for defining algorithmic (syntax-directed, or type-directed) type systems as monadic programs. We can generate the relational presentation, deterministic by construction, in the hope of reasoning by induction over derivations. We can also just run the damn thing, with gasoline-fuelled partial recursion. My plan is to try to prove key results (e.g. computation preserves type) for this small system, and then start chucking in more features. We should end up with a formal definition of the Epigram kernel, and a reference implementation to boot!