## 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
`Name`s 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 `Expr`ession 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
`infer`ring and `check`ing 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