Embedding Lambda Calculus

Posted on by Chris Warburton

Functional programming makes heavy use of embedded domain-specific languages (EDSLs). These make our programming language (the host language) behave like another language (the embedded language). This is similar to the way Object-Oriented libraries often choose class, property and method names which ‘chain together’ nicely, eg. Mailer.send(Order.invoiceFor(Session.user)); except functional languages aren’t limited to arg1.method(arg2, arg3, ...) syntax. We can use function arg1 arg2 arg3 ..., and use functions as arguments (higher-order functions).

Due to this interest in embedding, the desire to use purely-functional languages, and the desire for minimalism/simplicity, we functional programmers spend an unhealthy amount of time trying to embed various forms of lambda calculus inside our functional languages (which themselves are usually some form of lambda calculus).

There are a few ways we can do this:

First-Order Representations

A first-order representation uses data to represent lambda calculus programs. An example would be:

data FirstOrderTerm = Var String
                    | Lam String FirstOrderTerm
                    | App FirstOrderTerm FirstOrderTerm

This represents the three syntactic forms of lambda calculus terms directly:

This is fine for human use, but it’s no good for a machine; the space of Strings is too large and complicated for software to understand. It’s very unlikely that two arbitrary strings will match, so therefore unlikely that an auto-generated variable will match the argument of an auto-generated binder. We’re much better off numbering our arguments, which limits our options and increases the chances of a match. If we use de Bruijn indices, which I’ve blogged about before, the numbers have a consistent meaning in the meta-language (although they’re often avoided by humans because they have inconsistent, or rather context-dependent, meanings in the object language):

data Nat = Z | S Nat

data DeBruijnTerm = Var Nat
                  | Lam DeBruijnTerm
                  | App DeBruijnTerm DeBruijnTerm

Higher-Order Representations

A higher-order representation uses functions to represent part of a lambda term. A classic implementation of Higher Order Abstract Syntax looks like this:

data HigherOrderTerm = Lam (HigherOrderTerm -> HigherOrderTerm)
                     | App HigherOrderTerm HigherOrderTerm

There are two clear differences to note: firstly, Lam now takes a function rather than a term. We can understand this by thinking of the Lam as a ‘term containing holes’; to “filled in” those holes, we must pass in a term, hence the use of a function type.

So what are those ‘holes’? They’re the variables! Notice that we don’t need a separate Var constructor, because:

  1. Variables only make sense inside Lam terms (think back to de Bruijn indices!)
  2. Each Lam term now contains a Haskell function
  3. Haskell functions let us use Haskell’s implementation of variables

Haskell variables are the “holes” in our terms!

This is a very neat trick, but it has a few problems:

Hybrid

There are hybrid solutions, like the use of “circular programming” to define first-order representations from a higher-order interface. For example, this will generate terms with non-conflicting variable names, in a more “natural” way than de Bruijn’s “inside-out” numbering:

data CircularTerm = Var Nat
                  | Lam Nat CircularTerm
                  | App CircularTerm CircularTerm

max :: Nat -> Nat -> Nat
max  Z       y  = y
max  x       Z  = x
max (S x) (S y) = S (max x y)

maxBoundVar :: CircularTerm -> Nat
maxBoundVar (Var _)   = Z
maxBoundVar (Lam n _) = n
maxBoundVar (App f x) = max (maxBoundVar f) (maxBoundVar x)

lam :: (CircularTerm -> CircularTerm) -> CircularTerm
lam f = let n    = S (maxBoundVar body)
            body = f (Var n)
         in Lam n body

Unfortunately this doesn’t translate easily to total languages like Coq. The n and body variables in lam are mutually-recursive, and exploit the laziness of maxBoundVar. What’s worse, this recursion will only terminate if f produces ‘well-formed’ terms, ie. it only uses the App and lam interfaces, rather than constructing its own Lam or Var terms directly. This causes problems since we tend to reason about values using universal quantifiers: ie. forall f, SomeProperty (App (lam f) x), which requires us to litter our code with witnesses to demonstrate that, indeed, our functions are safe.

Encoding/decoding

I’ve written about Morgensen-Scott encoding before. We can use their scheme to encode any ‘polynomial’ datatype as a lambda calculus function. As long as we use a first-order representation, this allows us to reason “under the lambda”, but it does have associated dangers.

Whenever we translate from a typed to an untyped (or unityped) representation, we lose information. We cannot, in general, convert back to a typed representation. We’re forced to either wrap our decoders’ return types in a maybe, or else provide it with a witness to demonstrate that the term is well-typed.

We can ‘compose over’ these requirements easily enough, eg. using functors, applicatives and monads to compose across maybes, and perhaps some kind of state monad to carry the witnesses. However, since both of these are conservative approaches (‘guilty until proven innocent’), every decoding we perform will limit the space of possible programs we allow: the number of values which survive the maybe, or which have accessible proofs, is monotonically-decreasing as we add more decoding steps.

Hence it’s a bad idea to convert back and forth “in the small”, regardless of whether we have monads to make it convenient: if we’re going to perform any conversion at all, we should convert the entire remainder of our program (or the continuation, if you prefer).

That may sound like madness: we’d be throwing away the safety of our typed language, surely? That’s where powerful type systems really shine: we can type-check the encoding process, to guarantee that only well-typed encodings are produced, even though the encoding language is untyped. We actually do this all the time: it’s exactly what a compiler does! Encoding our continuation is like staged compilation. Since types (not to be confused with tags or classes) only exist at compile time, we always end up running an untyped (/unityped) language in the end, since that’s the only kind of language which can “run”!