Implementing the simply-typed lambda calculus

The lambda calculus is a formal system invented by Alonzo Church in 1920s wherein all computation is reduced to the basic operations of function definition and application. It can simultaneously be viewed as a simple programming language.

As “PL people” we’re often in search of minimalism, and so we should ask if there is a simpler way to get “real” computation. One potential answer, which comes to us from Alonzo Church in the 1920s, via John McCarthy in the 1950s and Peter Landin in the 1960s, is the lambda calculus. As the name suggests, it’s a core calculus for computation. It’s dead simple—just three syntactic forms and three small-step rules or two big-step rules. And yet despite this simplicity, the lambda calculus is Turing complete!
— James Bornholt

Let’s consider the untyped, or pure, lambda calculus first. A term t in the lambda calculus is one of three forms:

t := x      --> variable
   | λx. t  --> lambda abstraction
   | t t    --> application

Since variables and abstractions are values in the lambda calculus, only the application case can step - $\beta$-reduction. As noted above, a language consisting of just these constructs is Turing complete. One can informally justify this by mentioning that number can be represented by Church numerals, recursion can be implemented using fixed-point combinators and booleans can be encoded using lambdas. This is all out of scope for this article, but I would provide resources to get a better understanding of these concepts.

To make it easier to work with lambda calculus, we introduce a few extensions - namely, booleans and conditional expressions:

t := x
   | λx. t
   | t t
   | true
   | false
   | if t then t else t

@TODO: Define step rules

Let’s consider the untyped, or pure, lambda calculus and start with an interpreter for it instead. We need to define the “tokens”, i.e our internal representation of lanuage.

(define-type Simple
  [var (v identifier?)]
  [bool (b boolean?)]
  [sif (pred Simple?) (conseq Simple?) (altern Simple?)]  ;; if is a Racket keyword
  [fun (argType Type?) (i identifier?) (body Simple?)]
  [app (ratr Simple?) (rand Simple?)])

Implementing a parser is straightforward using Racket’s match functionality. We will implement an environment-passing interpreter. Notice that we do not have named functions, hence the only identifiers we need to keep track of are the arguments.