Sooner or later, it’ll be important to write down what it is we think we’re doing and try to prove some theorems about it. I’ve been thinking a bit about how to present systems of rules which are algorithmic, in the sense that relational judgments have distinguished input and output positions, where the inputs determine the outputs if the judgment holds at all. My first attempts just involved defining an inductive relation
R : S → T → Set
then laboriously proving, by induction of one and inversion of the other
R s t ∧ R s t’ ⇒ t ≡ t’
I had the nasty sensation of working too hard. In the systems I’ve been working with, information flows clockwise around the rules, from the inputs of the conclusion to the inputs of the first premise, … to the outputs of the last premise, to the outputs of the conclusion. This discipline ensures that we can turn the rules into a monadic program. So, thought I, why not do it the other way around? Write the program and extract the rules! Giddy-up-a-ding-dong!
Before I go further, this is actual Agda code. If you want to see the colour version and muck about with it, you can get the general purpose gubbins and the typing rule development.
What’s in a typical rule system? A mutually inductive derivations system for a bunch of judgment forms. Each rule concludes with a judgment of one form, but may have multiple premises of any form and also side-conditions. Side-conditions should be somehow meaningful already. If we’re treating judgments as input-output systems, then think Hancock! We may specify the judgments forms as a pair
S : Set — of judgment forms with inputs
T : S → Set — of outputs appropriate
Let’s have an example, plucked out of the middle of the development. I’d better tell you what terms are, first:
Lev = Nat ; Inx = Nat — de Bruijn levels, indices
data Dir : Set where nm ne : Dir — normal or neutral
data Tm : Dir -> Set where — indexed by direction
_!_ : (c : Can)(ts : List (Tm nm)) -> Tm nm
— canonical constructors
lam : (t : Tm nm) -> Tm nm — λ-abstraction
[_] : (w : Tm ne) -> Tm nm — embed neutral into normal
var : (v : Inx) -> Tm ne — bound variables (indices)
par : (p : Lev) -> Tm ne — free variables (levels)
_%_ : (w : Tm ne)(e : Elim (Tm nm)) -> Tm ne
— irreducible elimination
Today’s canonical constructors and eliminators are:
data Can : Set where SET PI : Can — sets and functions
data Elim (X : Set) : Set where
_/ : (t : X) -> Elim X — application
As you can see, terms are guaranteed redex-free. But we still need to know how to compute with them, so we have a system of computation judgments, specified as follows.
data CompS : Set where
_!-_%%_ : Lev → Tm nm → Elim (Tm nm) → CompS
_!-[_:=_]_ : Lev → Lev → Tm nm → {p : Po} → Tm p → CompSCompT : CompS -> Set
CompT _ = Tm nm
The judgment forms in CompS are for elimination and instantiation, respectively. Both need a name supply: names are de Bruijn levels, here. They’ll be mutually defined, because instantiation (e.g. of a variable with a λ-abstraction) can create redexes to be eliminated. Elimination explains how to eliminate a normal form (e.g., applying a λ-abstraction), and instantiation explains how to instantiate a free variable with a normal form in any term. The definition of CompT says that both judgment forms emit normal forms.
Informally, you’d expect a rule like
x !-[ p := s ] w ⇒ t
x !-[ p := s ] e ⇒ e’
x !- t %% e’ ⇒ u
—————————————–
x !-[ p := s ] w % e ⇒ u
Glossing over how you lift instantiation to eliminators, you instantiate the components then see what you get when you compute the instantiated elimination (which might have come unstuck). It’s just like a monadic program. CompS and CompT specify a signature of operations permitted in the computation monad.
Side conditions may similarly be specified as a command-response system (A : Set, B : A → Set). For computation, I need to be able to say ‘it does not make sense to compute this’, so I take
data CompA : Set where
abort : CompACompB : CompA → Set
CompB abort = Zero
The ‘abort’ side-condition is always false! We can use it to give a rule for every judgment in CompS, just by aborting the ones we don’t want.
Now that we have an idea what our command-response systems are like, let’s build the corresponding monad of programs.
data Prog (A : Set)(B : A → Set)(S : Set)(T : S → Set)(X : Set) : Set where
ret : X → Prog A B S T X
_!!_ : (a : A)(k : B a → Prog A B S T X) → Prog A B S T X
_??_ : (s : S)(k : T s → Prog A B S T X) → Prog A B S T X
Given command-response systems (A,B) for side-conditions and (S,T) for judgments, a program can produce an X by returning immediately, or by invoking a side-condition with _!!_, or by invoking a judgment with _??_. In the latter two cases, you provide the command and explain how to continue given the response. (Yes, old hands, that is just the W-type, repurposed.) It’s not hard to see that this is monadic in the usual tree-grafting way.
If we have a relational characterisation, C of side-conditions and F of judgments (F because it will correspond to a function), then each program induces a predicate, describing the values it is willing to return.
[_!_]_=>_ : forall
{A B} (C : (a : A) → B a → Set)
{S T} (F : (s : S) → T s → Set)
{X} → Prog A B S T X → X → Set
[ C ! F ] ret y => x = y == x
[ C ! F ] a !! k => x = Σ _ \ b → C a b * [ C ! F ] k b => x
[ C ! F ] s ?? k => x = Σ _ \ t → F s t * [ C ! F ] k t => x
For each command, we just quantify existentially over possible responses and carry on until we reach a return, which must then agree with the value we’re thinking of.
Now to tie the knot. If we have a function f which explains how to interpret each judgment as a program, computing a T s given any s : S, we can calculate the relation F above, with a bit of help from this inductive definition.
data Go
{A : Set}{B : A -> Set}(C : (a : A) -> B a -> Set)
{S : Set}{T : S -> Set}(f : (s : S) -> Prog A B S T (T s))
(s : S)(t : T s) : Set where
<_> : [ C ! Go C f ] f s => t -> Go C f s t
We can go from s to t if the program given by (f s) delivers t, interpreting side-conditions by C and judgments by recursively invoking f. If we can implement a suitable f, we can extract a relational presentation, Go C f, of its judgment system. Let’s do that in a moment, for our example. First, though, let’s just observe that these things have a deterministic character.
Deterministic :
{A : Set}{B : A → Set}(C : (a : A) → B a → Set) → Set
Deterministic {A}{B} C
= (a : A)(b b’ : B a) → C a b → C a b’ → b == b’
A binary relation C is deterministic if two ‘runs’ from the same input to some output are sure to agree. An easy induction shows that
{A : Set}{B : A → Set}(C : (a : A) → B a → Set) → Deterministic C →
{S : Set}{T : S → Set}(f : (s : S) → Prog A B S T (T s)) →
Deterministic (Go C f)
Just grind through the program f generates for the given input: side-conditions are deterministic by assumption, premises are deterministic inductively.
For computation, side conditions are…who cares?
CompC : (a : CompA)(b : CompB a) → Set
CompC abort ()
DetCompC : Deterministic CompC
DetCompC abort ()
So before we even say what the computation rules are, we know they are deterministic by construction. Let’s take the COMP monad to be
COMP = Prog CompA CompB CompS CompT
To do the construction, we need a wee bit more variable-mangling kit. I won’t go into the boring details of vp and pv, but these helpers let us go in and out of binders.
_//_ : Tm nm → Lev → Tm nm — name a bound variable
t // x = vp ze x t_\\_ : Lev → Tm nm → Tm nm — bind a free variable
x \\ t = pv x ze t
As a result, we can always name the variables we work with, which is why the judgments take a name supply. We shall also need to lift instantiation to term-containing structures like List and Elim. This is no bother, because COMP is a monad and the containers are traversable. We need this kit (the type is the interesting part):
_!-[_:=_]^_^_??_ : forall {F X} →
Lev → Lev → Tm nm → {d : Dir} → Trav F → F (Tm d) →
(F (Tm nm) → COMP X) → COMP X
x !-[ p := s ]^ tr ^ ts ?? k
= bi{COMP} moProg (tr{COMP} apProg (\ t → x !-[ p := s ] t ?? ret) ts) k
which lifts the invocation of the judgment through any traversable structure.
Let’s do it!
compf : (s : CompS) → COMP (CompT s)
That’s the signature. Now we need to say what to do for each judgment, starting with elimination. We have the β-rule.
compf (x !- lam t %% s /) =
su x !-[ x := s ] t // x ?? \ u →
ret u
Tilt your head to the right to see the rule! A β-redex normalises to u if the corresponding instantiation does. Note that we name the bound variable with the next free name, x, then invoke instantiation with the new name supply, su x.
Stuck things just accumulate eliminators:
compf (x !- [ w ] %% e) =
ret [ w % e ]
Canonical types can’t be eliminated.
compf (x !- c ! _ %% e) = abort !! \ ()
Meanwhile, instantiation proceeds structurally through canonical things.
compf (x !-[ p := s ] c ! ts) =
x !-[ p := s ]^ travL ^ ts ?? \ us ->
ret (c ! us)
To instantiate under a binder, we first name, then instantiate, then abstract.
compf (x !-[ p := s ] lam t) =
su x !-[ p := s ] t // x ?? \ u ->
ret (lam (x \\ u))
When we see a stuck thing, we truck on inside:
compf (x !-[ p := s ] [ w ]) =
x !-[ p := s ] w ?? \ u ->
ret u
We should never see a bound variable!
compf (x !-[ p := s ] var v) = abort !! \ ()
And if we see a free variable, we test if it’s the one we seek (nq decides numeric equality, with inl for yes and inr for no):
compf (x !-[ p := s ] par q) with nq p q
… | inl _ = ret s
… | inr _ = ret [ par q ]
Finally, the example rule from earlier instantiates then recomputes eliminations (Elim is traversable):
compf (x !-[ p := s ] w % e) =
x !-[ p := s ] w ?? \ t ->
x !-[ p := s ]^ travE ^ e ?? \ e’ ->
x !- t %% e’ ?? \ u ->
ret u
I’d better stop here for the moment. What happens next? Well, up to a point, we can execute these rules. If we give a numerical bound (a gasoline suppply) on the depth of derivation we’re willing to tolerate, we can run this program until it aborts, gives us an output and a derivation, or runs out of gas. I’ll show you how that’s done. I’ll also build a type system (thence a gasoline-driven typechecker) for Set-in-Set along these lines, using these computation rules as the side-conditions: this is a trick which is easy to play twice!