Lambda the Ultimate

So a few decades ago, people came up with the idea of "higher-order abstract syntax"

To get slightly historical, the basic idea behind HOAS is Church's work on representing quantifiers using lambda abstraction, which essentially is the origin of the lambda calculus. I'd say that van Dalen's work on Automath is the first HOAS work, in that it studies the general application of this intuition.

Great post, Neel. Thanks.

Thank you very much Neel, this is This is the kind of post that is going to be a great resource for newcomers, and non-theorists like myself for a long time coming.

So as I understand it this kind of theory is very important for people trying to implement languages using a formal approach. E.g. implementing the language using a small formal meta-language.

It seems like this is a very different approach then the one used by thousands of hackers like myself who just bolt together programming language implementations in some general purpose programming language. I can make a language implementation work, more or less, but I may never be able prove that there are no bugs.

By the way, I read your post three times and I got something new out of it each time. You have a talent at making a very rich and complex subject very accessible!

This sort of theory is potentially useful to anyone implementing languages related to the lambda calculus (at the very least). Presumably they have to do at least some manipulating of abstract syntax, and want correct implementations of alpha conversion, and possibly even beta reduction and such. Even the abstract machine language for the STG machine has variable names, for instance.

It's not impossible to just work with (string) variable names, and get everything correct. However, it's easy to make mistakes; especially so if you're doing some sort of code generation that needs to make up fresh names. For instance, in their paper I am not a Number, I am a Free Variable McBride and McKinna talk about generating inductive elimination principles in some type theory. One example they use is:

data Nat = Zero | Suc Nat

and want to generate the eliminator type:

∀(P : Nat → Prop). P Zero → (∀(k : Nat). P k → P (Suc k)) → ∀(n : Nat). P n

But, you have to be careful in doing so, not to accidentally do:

data P = Zero | Suc P

elim : ∀(P : P → Prop). P Zero → (∀(k : P). P k → P (Suc k)) → ∀(n : P). P n

So, your code generator needs to be robust enough not to pick names that are already in use.

There are several schemes for circumventing this sort of issue. For instance, De Bruijn indices/levels use natural numbers instead of names for bound variables, so for the above, you get something like:

∀(Nat → Prop). 0 Zero → (∀Nat. 1 0 → 1 (Suc 0)) → ∀Nat. 1 0

HOAS is another solution. The practical side of all this is that you don't have to implement the error-prone munging of variable names. Why write and check code for that when you can use some other technique that doesn't need it, and lends itself toward your writing the right code from the start? Of course, other techniques have their own trade-offs. But this isn't just a purely theoretical exercise.

HOAS also has connections to embedded DSLs in languages like Haskell. As an overly simplified example, presentations of delimited continuations sometimes present shift as a new sort of binder:

shift k in <k can be referred to here>

But one can obviously make shift higher-order instead:

shift (\k -> ...)

So, EDSLs (by necessity, I suppose, in the Haskell case) implement binders for the DSL as binders in the meta-language, just like HOAS.

You reminded me of another line of work, which goes back to work of Andrew Gordon. Cf. Gordon and Melham (1996), Five Axioms of Alpha-Conversion, LNCS 1125:173-190.

The basic approach is come up with an axiomatisation of what a theory needs to satisfy for its names to be free of substitution issues, and then prove that whatever concrete representation you want to use satisfies this property. The paper does this for the de Bruijn representation. I seem to recall that Andrew Pitts said that the technique wasn't completely straightforward in its application, but I don't recall what the problem was.

Another point is that the de Bruijn representation has a nontrivial parallel to the implementation of closures: lambda abstractions are like frames, and de Bruijn indices are a count of how many times you need to hop into the next-most enclosing frame to get to the one that binds the correct variable.

[Edit: upon rereading the paper, I can that this comment, really misses the mark. Contexts are not as simple as that. I'm going to leave it for the sake of amusement. :-)]

I think I understand box gamma exp. A context is essentially a dictionary, right? Mapping names to values. So what I am understanding here is the suggestion that a term with free variables (e.g. a closure) can be implemented (at the meta-level) by using a dictionary meta-type. Right?

This seems kind of common sense doesn't it? This is exactly how I implemented closures in my language (and I am guessing many other people do as well).

I guess the magic here, is being able to do it in a provably correct way in a meta-language. That seems like quite a feat.

An open term isn't quite the same thing as a closure. The difference is that a closure has a value associated with each variable, whereas an open term doesn't. The free variables are really just typed placeholders, with nothing bound to them (yet).

A better way to think of the context is as a list of variables names. If gamma lists the variables x and y, then (suc x), (suc y) and (x + y) all have type [gamma]nat, but (suc z) doesn't.

In addition to listing the variable names, a context also lists the types of those variables. So if gamma is {x:nat, y:list nat}, then (suc x) has type [gamma]nat, but (suc y) doesn't.

You give this data type in OCaml for a 'HOAS' representation of the syntax of the lambda calculus:

  type exp = App of exp * exp | Lam of (exp -> exp)

This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term, e.g.:

  let not_a_term = Lam (fun e -> match e with
                                   | App (_,_) -> e
                                   | Lam _     -> App (e,e))

This value in the type exp "represents" a lambda abstraction that has a different body depending on whether the closure representing the body is passed an application or a lambda. Such values in this type are called "exotic" terms.

It is possible to attempt to get around this by restricting when the programmer is able to pattern match on members of types one wishes to use for representing data with binders. This is the approach taken by Fergaras and Sheard in Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space).

A better solution, first proposed, to my knowledge, by Coquand and Huet in Constructions: A higher order proof system for mechanizing mathematics back in 1985 and later independently promoted by Washburn and Weirich in Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, is to use parametric polymorphism. They use the type:

  exp = forall a. ((a -> a) -> a) -> (a -> a -> a) -> a

An example term is represented like so (explicitly writing the type abstraction):

  omega = /\a. \lam app. app (lam (\x -> app x x)) (lam (\x -> app x x))

The idea is that because the type a is kept abstract, it is not possible to analyse it and create exotic terms.

This is similar to the Church encodings of inductive data types (e.g. forall a. a -> (a -> a) -> a for the natural numbers): there is a universally quantified type variable for the carrier and a collection of "constructors" (abstraction and application for the exp type and zero and successor for the natural number type). The exp differs because there is a negative occurrence of a in the abstraction constructor, which is normally disallowed.

Neither Coquand and Huet nor Washburn and Weirich presented a proof that the exp type actually does represent only the untyped lambda calculus terms. I proved this in a TLCA paper published this year: Syntax For Free: Representing Syntax with Binding using Parametricity, in the setting of System F. One needs to use parametricity over Kripke logical relations to prove the result; the Kripke indexing is required to keep track of the number of binders that have been passed under. The paper also shows that weak HOAS (AKA Chlipala's "Parameterised HOAS") is isomorphic to normal HOAS, and that computational and syntax-with-binding can be intermixed easily (c.f. A universe of binding and computation by Licata and Harper). It also gives an interesting perspective on the Haskell ST monad (by thinking of dynamic allocation as name binding).

The construction at the core of the proof gives a way of going from the HOAS type exp to a more normal de Bruijn representation and back again. With Sam Lindley and Jeremy Yallop, we wrote a paper Unembedding Domain-Specific Languages that does this in Haskell and shows how one can use HOAS as an input language for EDSLs, but still retain the capability of converting to a de Bruijn representation which may be easier to work with. We also show how to do object languages with pattern matching and also how to represent open terms with arbitrary numbers of free variables, captured in the type system.

This technique extends smoothly to typed languages, using Haskell's types to represent types in the embedded language. This turns out to be very similar to Carette et al's "Finally Tagless" approach Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. We note in the "Unmebedding..." paper that to get an adequate representation of actual typed terms, one needs to restrict to a fixed subset of Haskell types rather than use all types as in the "Finally Tagless" approach, lest one allow "exotically typed" terms. Manuel Charavarty noted the same thing in his conversion from "not HOAS" to de Bruijn terms.

As a side note, I think that the "Finally" is pretty much meaningless here: the message of my "Syntax for free" paper is that the parametric polymorphic HOAS representation is actually a way of representing initial algebras in pre-sheaves (c.f. the Fiore, Plotkin, Turi approach to a mathematical representation of syntax with binding) just using parametric polymorphism, which is pretty cool.

I have recently been working on how to write computations over the parametric polymorphic HOAS (and weak HOAS) representations that gets some of the advantages of the new programming languages like the one presented in the paper at the top of this thread. I have been able to cover all the examples in this paper, plus some nice examples of NBE for various languages. I'll try and put them on-line sometime.

This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term, e.g. ...

Yes, you are entirely correct.

I was deliberately trying to avoid talking about adequacy of representations, but I suppose that avoiding at the price of technical error is too high a price to pay!

Neel said:

I was deliberately trying to avoid talking about adequacy of representations, but I suppose that avoiding at the price of technical error is too high a price to pay!

Though as a community member I'd like to thank both Bob and Neel for their contributions to this thread, I'd like to take a contrary view to this quoted section as it relates to LtU discussions.

Sometimes when trying to help out with an issue of basic understanding about some topic, it is necessary to glide over some of the "gory details". Once the other person "gets it", then the gory details can come back in.

Professors do this all the time in intro courses, and this relates to the use of the discussion of pseudo-code in algorithms textbooks.

I think Neel's presentation was just right for the spirit of the thread, and if the other choices were to make the example too complicated to follow for the original poster, or to not post at all to avoid an inaccuracy of detail, I think the best option for LtU is exactly the one he chose, i.e. an informative approximation.

Adequacy is a very modest name for a vitally important question: does the data representation actually faithfully represent what we intend? So when we write down an abstract syntax, and represent it with a fancy data structure, we really need for there to be a one-to-one correspondence between the intended syntax and the elements of the representation.

The existence of "exotic terms" shows that the datatype I gave is NOT adequate -- there's weird stuff in the type that doesn't correspond to any syntactic object. This isn't an entirely theoretical concern, either -- you can make some Lisp compilers go into infinite loops by asking them to compile programs represented as circular lists. This can be viewed as the result of a failure of adequacy: the compiler is written expecting the type of s-expressions to be well-founded, but the data type actually includes infinite terms that the compiler writer didn't expect.

If there were no way to ensure adequacy with HOAS, the whole approach would be a non-starter, because we'd be throwing away what we wanted and using some random datatype instead. So Bob's objection is wholly justified; the fact that adequate representations are possible is a critical feature of the methodology of HOAS.

The LF type theory used in Twelf (and Beluga, the system of this post) is very carefully engineered to restrict the function type so that exotic terms do not occur, and to make adequacy proofs very easy. You can view the work of Fiore et al. as a way of giving a denotational semantics to (many?) LF types.

But though presheaf models are a sturdy workhorse of semantics, they do have the downside that translating them into type theory is a bit awkward (you move "up a level" when you model presheaves straightforwardly in type theory). So I think Bob undersells his own work somewhat when he calls his proof of the equivalence of parametric representations with presheaf models "pretty cool" -- it's actually really, really cool, because now you've got a program you can actually run to translate between representations. I highly endorse reading both of his (and his coauthors') papers he linked to. :)

This is a great conversation. I know its lame to say so, but I had to say it. I am able to start getting a hint of how things like exotic terms tie into implementation problems in a compiler. Its weird how a compiler implementor can run into these kinds of problems, without knowing a thing about how deep the theory is behind it.

Its weird how a compiler implementor can run into these kinds of problems, without knowing a thing about how deep the theory is behind it.

Actually, this is just what you would expect in a healthy subject domain: the theoreticians and the practitioners talking about the same things, just one in the abstract and general case, the other in the concrete and particular.

If practitioners never stumbled across issues of theoretical import in their practice, you would have to wonder about the health of the field. ;-)

The existence of "exotic terms" shows that the datatype I gave is NOT adequate -- <snip> This isn't an entirely theoretical concern

I understand the problem, and acknowledge that if the point of your post was to give a detailed recipe on how to implement HOAS, that flaw would be fatal.

If on the other hand, your goal was to answer the OP's question, and further the poster's understanding of the issue itself, the "flaw" is an incidental casualty of the explanatory process.

I think it is great that people like Bob make those of us who already have the background to understand the issues aware of their valuable work.

But for those who don't yet get the gist of the problem, it is helpful to understand the idea before we get bogged down in the tough spots.

My purpose in pointing this out is to use this as a "teachable moment". I've lost count of the number of times I've been in threads where what started as an attempt to give the yin-and-yang of a problem to a poster, or to clarify a misunderstood foundational issue, turns into a master-class quibble-fest.

It is a disincentive to those who want to help beginners in a particular subject from posting if every time someone does it, they get publicly spanked by the experts. ;-) Especially when it's not that they have made a mistake but rather that they have made a strategic simplification.

I think it is great that we have both advanced-level and beginner-level discussions here. I think we just need to be a little more discerning of which is which.

I don't mind the master-class quibblefest effect so long as it's clear where the transition lies and people aren't treated disrespectfully for giving beginner-level answers. Done that way, the thread ends up managing to teach a wider range of people.

Of course, spanking generally isn't respectful :-)

This is not HOAS. It does not represent terms with binding; it is the solution of a particular recursive domain equation that contains pairs and functions. This data type contains many things that do not represent any lambda term

Morally speaking, you are right: HOAS is about appropriate representations of possible terms of some language with binders. As a criterion describing what the literature accepts and rejects as being HOAS, this is not right. Using function spaces that overgenerate in the way you describe is not rare.

I think the reason people are willing to tolerate overgeneration is something along the lines of: each term-with-binders has an obvious, canonical representation in HOAS, so the image of our alpha-challenged term calculus in HOAS provides us with the syntactic theory we need, and who cares about the monsters lurking in the dark?

The problem with monsters lurking in the dark is that cannot safely retrieve anything from the dark. We push things in, and we are happy that they fit, but once they are in, we have lost them.

More concretely, the type that Neel gave:

  type exp = App of exp * exp | Lam of (exp -> exp)

has the serious bug that practically no useful functions can be written that take exp as input. For instance, maybe we want to write a function that computes the size of a term. So we try:

  let rec size t = match t with
   | App (t1, t2) -> 1 + size t1 + size t2
   | Lam t        -> 1 + size (t ???)

What do we put for ???? We need to pass in an exp, so we are limited to either App (...,...) or Lam ..., but either of these will lead to non-termination.

Fegaras and Sheard (see my other post above) solved this problem by adding a new constructor to represent whatever it was that was being computed, and parameterised everything by a type:

  type 'a exp = App of 'a exp * 'a exp | Lam of ('a exp -> 'a exp) | Hole of 'a

Now we can write the size function, but we still have the problem that exotic terms are representable (Fegaras and Sheard fix this by an ad-hoc extension to the type system to prevent case analysis of certain types). But we are nearly there! All we have to do is drop the negative occurrence of exp and wrap everything in a type abstraction:

  type 'a exp' = App of 'a exp' * 'a exp' | Lam of ('a -> 'a exp') | Var of 'a
  type exp = { x : 'a. 'a exp' }

This is Chlipala's parameterised HOAS, previously known as weak-HOAS, and it represents all and only the untyped lambda terms, see my "Syntax for Free..." paper (modulo problems with non-termination (which I think gives you possibly infinite terms) and the non-parametric features of OCaml). We can now write the size function easily by instantiating the 'a to be int.

This is from the #haskell channel (thanks Saizan)

Inspired (copied) from the "Parametric Higher-Order Abstract Syntax for Mechanized Semantics" paper

untyped HOAS:

data Exp' a =
Lam (a -> Exp' a)
| App (Exp' a) (Exp' a)
| Var a

type Exp = forall a. Exp' a

typed HOAS (using GADTs):

data TExp' a b where
Lam :: (a b -> TExp' a c) -> TExp a (b -> c)
App :: TExp' a (b -> c) -> TExp' a b -> TExp' a c
Var :: a b -> TExp' a b

type TExp = forall a. TExp' a

This is a great mini-glossary Charles, thank you. It really helps to get a sense of what is being discussed and help orient me in the massive world of language theory. The fact that the problem with binders is in the context of "structural induction" is a really key point for me. If I never do structural induction, I probably will never want to know the theory at the level of detail used in the paper. It is also an interesting revelation that that I would have to understand structural induction if I ever want to reason about the language implementations I work on. The Pitts paper seems to be very thorough in its treatment of the subject of variable binding and alpha-equivalence, thank you.

Yes, reasoning about your language implementation will be another area where the "bound name problem" comes in. This motivates efforts like Nominal Isabelle, which aims to provide support for working with alpha-equivalence classes in Isabelle/HOL. See Christian Urban's poster, "How to prove false using the variable convention" for a demonstration of how insidious naive reasoning with binders and alpha-equivalence classes can be.

As Charles mentioned, there's a whole mini-industry trying to solve the name binding (and related) problems, with (markedly) different methods. HOAS, and its variants, are one approach, embedding object-languages inside the simply-typed lambda-calculus. Gabbay and Pitts' Nominal sets are another, and were the inspiration for FreshML, alpha-Prolog, Nominal Isabelle, etc. de Bruijn indices "solve" the problem by making alpha-equivalence checks coincide with textual equality, at the expense of readability for human users (if that's a concern). Locally nameless approaches are another approach, along with many others.

I hope the maintainers of LtU won't mind a bit of a plug, but I recently started a blog, in a similar vein to LtU, for discussing these matters related to name binding. Rather strangely, I posted this same paper on the blog a few days ago!

A LtU-wiki is high on our todo list. It will appear at some point, I promise.

It can be used, at least in principle. However, it is not ready for general use. IIRC:

1. We have not really figured out the editorial policy yet. So anything you put there might not stay;
2. The wiki software is not yet unified with the main site, so there is no uniform login.