Simply Typed Lambda Calculus in Agda, Without Shortcuts

1 May 2013 (programming agda correctness language)

There are many ways to introduce dependent type systems, depending on which side of the Curry-Howard lens you look through. But if your interest is more in programming languages than proof assistants, then length-indexed vectors is your Hello, World!, and an interpreter for the simply-typed lambda calculus is your FizzBuzz. I think the usual presentation of the latter is a bit of a cheat, for reasons which I will explain below. I'll also show a "non-cheating" version.

First of all, for reference, let's look at the usual presentation. We define a datatype for well-typed lambda terms:

Note how these are correct by construction: we use de Bruijn indices to ensure variable occurances always point to variables in scope, and we encode the type system in the types of var, lam and _·_. With so many guarantees in place, the actual evaluation is a breeze:

Aaand we're done.

But I think this is cheating, since we're heavily exploiting the fact that the type system and the scoping rules of the language we're implementing readily fits into the host type system of Agda. But what if it didn't? For example, what if you were embedding a language with a linear type system? So let's write the same simply-typed lambda interpreter without taking "the Agda shortcut".

Scope checking

If we're serious about supporting something that might actually come from a human, the raw input should contain proper variable Names instead of all this de Bruijn nonsense:

But from the point of view of the poor soul who has to do any downstream processing, de Bruijn actually looks like a splendid idea, so we would prefer that. We also give a declarative account of what it means for an Expression to be well-scoped with respect to a variable Binder.

(note how var-suc implements shadowing by requiring the inner name to not match before considering the outer one)

We can then go from Syntax to Bound via a scope checker, which is basically a decision procedure for well-scopedness. I omit the implementation here, but you can look at it by clicking on the file name in the lower-right corner:

To implement actual scoping, we just extract the representation containing bound variables from the witness returned by check:

Typechecking

Typechecking goes along the exact same way: we define our type system (parametrised by some user-supplied universe U of leaf types) as derivation rules:

Nothing left to do but to apply some elbow grease and implement type inference / type checking. Again, I'm omitting the full source file here; the following two functions for inferring and checking types are defined in a mutually recursive manner.

Embedding

We could now write an interpreter by traversing the type derivation, but just for fun, let's feed this snake its tail by converting a well-typed, Bound expression into the "cheating" representation from earlier.

Putting it all together: semantics of STLC

With all these pieces ready, defining the semantics of our user-friendly representation of STLC couldn't be any simpler:

Full source code with nice syntax highlighting & full hyperlinking