Using dependent types, it is possible to specify contracts for Agda programs at a very fundamental level. Today we’ll see how to transform an extremely simple tree-based calculator language to a stack-based one; and use Agda to assert the correctness of our transformation. The complete source code for this post is at 1.

The tree-based language is defined by the following data-type, with the obvious semantics:

``````data Exp : Set → Set₁ where
↑_ : {A : Set} → A → Exp A
_plus_ : Exp ℕ → Exp ℕ → Exp ℕ
_minus_ : Exp ℕ → Exp ℕ → Exp ℕ
_eq_ : Exp ℕ → Exp ℕ → Exp Bool
_lt_ : Exp ℕ → Exp ℕ → Exp Bool
cond_then_else_ : {A : Set} → Exp Bool → Exp A → Exp A → Exp A``````

Note how dependent types are helpful already – without them we would not be able to elegantly assert 2, for instance, that `lt` takes two `Exp ℕ`s and maps them to an `Exp Bool`. The semantics are defined by a function with the stereotypical name `eval` of type `Exp A → A`.

``````eval : {A : Set} → Exp A → A
eval (↑ value) = value
eval (a plus b) = eval a + eval b
eval (a minus b) = eval a ∸ eval b
eval (a eq b) with Data.Nat._≟_ (eval a) (eval b)
... | yes _ = true
... | no _ = false
eval (a lt b) with Data.Nat._≤?_ (eval a) (eval b)
... | yes _ = true
... | no _ = false
eval (cond c then t else f) = if eval c then eval t else eval f``````

Nothing unusual here, expect perhaps the implementation of ```eval (a eq b)``` and `eval (a lt b)`. Boolean values aren’t especially useful in dependently-typed programming languages since they don’t carry a proof of why a proposition is true. Operations like `≟` and `≤` therefore evaluate to a `Decidable` instance; which, apart from the result of the comparision (the `yes` and `no` we’re pattern matching on here), also contain a proof term of why the proposition is true or false. Since we don’t need the proofs for this rather simple use-case, we merrily ignore the same by underscores.

The stack-machine we’ll compile to is a bit more interesting – here too we use dependent types to guarantee consistency as much as possible. First of all, we use a stack that tracks the types of all its elements separately:

``````data TypedStack : List Set → Set₁ where
nil : TypedStack []
push : {A : Set} {S : List Set} → A → TypedStack S → TypedStack (A ∷ S)``````

This signature ensures that, for instance, the first three elements of a stack of type `TypedStack (ℕ ∷ ℕ ∷Bool ∷ S)` (for some `S`) will have types `ℕ`, `ℕ` and `Bool`.

The stack machine has six bytecodes, `bcAdd`, `bcSub`, `bcEq`, `bcLt`, `bcCond` and `push` (one of the constructors for `TypedStack`).

``````bcAdd : {S : List Set} → TypedStack (ℕ ∷ ℕ ∷ S) → TypedStack (ℕ ∷ S)
bcAdd (push a (push b rest)) = push (a + b) rest

bcEq : {S : List Set} → TypedStack (ℕ ∷ ℕ ∷ S) → TypedStack (Bool ∷ S)
bcEq (push a (push b rest)) with Data.Nat._≟_ a b
... | yes _ = push true rest
... | no _ = push false rest

bcCond : {S : List Set} {A : Set} → TypedStack (Bool ∷ A ∷ A ∷ S) →
TypedStack (A ∷ S)
bcCond (push c (push x (push y rest))) = push (if c then x else y) rest``````

The bytecode types specify how the bytecodes will transform the stack. A program in this context is essentially a composition of some of the above bytecodes

``````StackProgram : Set → Set₁
StackProgram a = {S : List Set} → TypedStack S → TypedStack (a ∷ S)``````

and a term of type `StackProgram X` is a program that leaves behind a value of type `X` when it’s done executing. So, for instance

``````leaveBehindEleven : StackProgram ℕ
leaveBehindEleven = bcAdd ∘ push 5 ∘ push 6``````

is well typed but

``````popsEmptyStack : StackProgram ℕ
popsEmptyStack = bcAdd ∘ push 5``````

isn’t.

Now we come to the compiler that transforms programs in the tree form to equivalent programs in the stack-machine form. The compiler itself is simple (some cases have been left out):

``````compile : {A : Set} → Exp A → StackProgram A
compile (↑ y) = push y
compile (a plus b) = bcAdd ∘ compile a ∘ compile b
compile (a eq b) = bcEq ∘ compile a ∘ compile b
compile (cond c then x else y) = bcCond ∘ compile c ∘ compile x ∘ compile y
-- ...``````

As a proof that the compiler actually preserves program semantics, we look for a term, `verifyCompiler` of the type ```{A : Set} → (exp : Exp A) → IsCorrectFor exp``` where ```IsCorrectFor exp = (S : List Set) → (compile exp {S} ≡ push{_}{S} (eval exp))```. In plain English, an expression exp is correctly compiled, denoted as `IsCorrectFor exp`, only if compiling and executing the stack-machine version is the same as evaluating the tree version and pushing the evaluated value onto the stack. The compiler is correct only if it correctly compiles all expressions. If you’ve been following along, give writing verifyCompiler yourself a shot!

Agda finds the simplest case for verifyCompiler obvious

``verifyCompiler (↑ y) S = refl``

To prove that we correctly compile `a minus b`, we need to show that `compile (a minus b)` is the same function (`compile` returns a stack program, which is essentially a function from `TypedStack` to `TypedStack`) as `push (eval (a minus b))`. To do this, we first show that since `compile b` is the same as `push (eval b)`, ```compile (a minus b)``` is `bcSub ∘ compile a ∘ compile b` is ```bcSub ∘ compile a ∘ (push (eval b))```. This is shown in `sub-prf₀`. Similarly, in `sub-prf₁` we show that since `compile a` is the same as ```push (eval a)```, `bcSub ∘ compile a ∘ (push (eval b))` is the same as ```bcSub ∘ (push (eval a)) ∘ (push (eval b))```. These two combined, by transitivity, gives us our proof – Agda is clever enough to see that `bcSub ∘ (push (eval a)) ∘ (push (eval b))` reduces to ```push ((eval a) ∸ (eval b))```.

``````verifyCompiler (a minus b) S =
let inductionA = verifyCompiler a
inductionB = verifyCompiler b
sub-prf₀ = subst (λ term → compile (a minus b)
≡ bcSub ∘ compile a ∘ term)
(inductionB S) refl
sub-prf₁ = subst (λ term → bcSub ∘ compile a ∘ (push (eval b))
≡ bcSub ∘ term ∘ (push (eval b)))
(inductionA (ℕ ∷ S)) refl
in trans sub-prf₀ sub-prf₁``````

We slightly deviate from this approach when proving correctness when compiling for `a lt b` and `a eq b` – I had to case on the two possibilities when comparing `a` and `b`.

Certified compilation is a rather 3 interesting 4 topic – something I’d like to explore further. A compiler for something a little more substantial than basic arithmetic should be a nice sequel.