Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Name Binding

Foundational Aspects of Syntax

• rating: 1

The first two pages are an excellent description of the problem.

In a nutshell, the solution is to add lambda-abstractions to the AST:

In this way, the category variable is no longer necessary (being subsumed by the corresponding notion in the λ-calculus)

The weakness, IMO, with this solution is that it just "kicks the can to the meta-level". Yes, you have removed the need to worry about binding in your object language. But you still need to reason about binding in your meta-language (here, the lambda calculus.)

From some older notes I made a while back:

"Determining the structure of λ-trees" starts to get a little murky: when you try to match the pattern

(∀ (λu. ⊃ (P u) (Q u)))

against the term

(∀ (λx. ⊃ (p x x) (q a a)))

we get a match "by instantiating P with λx.p x x and Q with λx.q a a and then using α and β-conversion."

P = λx.p x x
Q = λx.q a a

What actually is happening here?

The short answer, I think, is "higher-order unification".

In the 2nd example, middle of page 3, the object language is the lambda calculus, so it almost seems absurd: it's unclear what the solution is actually aiming to provide to simplify the problem here.

The next section makes it clearer that the solution is to grapple with the lambda abstractions at the meta-level. Use higher-order unification to work with them. Use a weaker form of beta-reduction in it, to simplify this problem. It's still unclear why, if you are prepared to do this anyway, you want to move the name-binding abstraction to the meta-level. In most cases I imagine you could do the very same thing with binding abstractions in the object language. Perhaps lifting them to the meta-level makes the transformations tidier in some way. (The conclusion of "Abstract Syntax for Variable Binders" seems to be addressing this concern: apparently this view is "impatient" and these issues are foundational enough that they need to be addressed in a principled fashion, like this.)

How to recurse into these lambda abstractions? Define some inference rules at the meta-level, then

The hypothetical judgment (the meta-level implication) implicitly handles the typing context, and the generic judgment (the universal quantifier) implicitly handles the bound variable names by via the use of meta-level eigenvariables.

So if you like to have, or already have, the right mechanisms in your meta-language for handling these things, you can lean on it and re-use it for your object language. If you don't, this doesn't help you.

Abstract Syntax for Variable Binders

• rating: 1

(These are older notes, and if I read the paper again today, I might write them differently.)

Sometimes we want to write programs that manipulate other programs. Other programs have variables in them that have scopes and stuff. It would behoove us to have a representation of these other programs that would allow us to reason about them modulo those variables. e.g. compare two functions without regard to the names used for their formal parameters.

Programs have concrete syntax and abstract syntax. But what we're talking about here is even more abstract than abstract syntax is usually considered. It abstracts away name bindings.

The second section starts talking about Church's STT (as a logical system). Then starts talking about "equality modulo alpha, beta, eta equivalence". This is higher-order abstract syntax (HOAS).

Miller proposes HOAS to be an equational theory at the meta level that does not distinguish between object level forms if they are alpha, beta, eta convertible. This is different from how HOAS is conceived in Haskell, which is "merely" using the meta-level (Haskell-level) lambda to implement object-level lambda, but this is mainly because Haskell is "merely" a programming language.

Pfenning and Elliott have already coined the term "HOAS" and have proposed using a lambda calculus with product type and polymorphism. But Miller says

In practice, higher-order abstract syntax has generally come to refer to the encoding and manipulating of syntax using either simply or dependently typed λ-calculus modulo α, β, and η-conversion.

Then he starts talking about big-L-sub-lambda, and unification therein, which is basically unification of lambda terms in Lambda Prolog (which is where Miller has applied HOAS.)

big-L-sub-lambda uses a weaker version of beta-conversion that is called "beta-0 conversion".

Finally Miller gets to lambda-tree syntax:

In contrast to concrete syntax and parse tree syntax, a third level of syntax representation, named λ-tree syntax was introduced in [Foundational Aspects of Syntax]

Note that Harper's abstract binding trees are also described (by Harper) as a third level of syntax, more abstract than abstract syntax.

Miller prefers the term "lambda-tree syntax" over "higher-order abstract syntax" because:

• it has only beta-0 reduction (not full beta reduction -- Pfenning is quoted as saying "higher-order abstract syntax supports substitution through λ-reduction in the meta-language")
• it doesn't rely on types (he regards "higher order" as referring to types.)

(I would agree that "higher-order" is not greatly stable nomenclature, and often refers to things in ways that I don't expect it to refer to them in!)

A Simple Take on Typed Abstract Syntax in Haskell-like Languages

• rating: 1

A good simple example of untyped lambda calculus implementation.

The fact that we can represent untyped λ-terms is not a shortcoming of the meta language. One might want to represent programs in an untyped object language like Scheme or even structures for which no notion of type exists.

A good simple example of Haskell-style HOAS. (i.e. using Haskell's lambda to implement an object language's lambda.)

Shows that it can be polymorphically typed to reflect the object language's types, without getting into GADTs or anything.

Discusses partial evaluation a little bit (type directed) ("long beta-eta normal form" -- in one of my experiments, what I was trying to do with "simplification" of lambda terms, was fairly close to this.)

A simple and clear presentation of Church numerals:

zero :: (a -> a) -> a -> a
zero = \s -> \z -> z
suc n = \s -> \z -> s (n s z)
add m n = \s -> \z -> m s (n s z)

Demonstrates using Haskell's type inferencer as a theorem prover.

A Metalanguage for Programming with Bound Names Modulo Renaming

• rating: 0

.

I am not a Number, I am a Free Variable

• rating: 1

So, if we try to ignore the sheer amount of too-clever-by-half in this one; the basic idea is "locally nameless", which goes back much further, but this presents a rather souped-up version of it, where the named free variables are namespaced (to "Agencies"), and the de Bruijn indexed bound variables are abstracted away with the help of combinators for "navigating under binders". This more robust version was not developed as a general tool, more of a means to deal with using zippers to manipulate inductive type definitions; and this context strongly shows in how it is presented in the paper; yet it is claimed to be useful as a general tool nonetheless. The idea to have combinators that allow "navigating under binders" is indeed not a bad one; but the thing that makes it a good idea is that it abstracts away the binding mechanism, meaning that it is not actually important (to the user, or to the implementation) that the bound variables are represented by de Bruijn indices. I would've liked to have seen more emphasis on that angle than on "how we built something so that we could avoid headaches while we were implementing our proof assistant".

A Type and Scope Safe Universe of Syntaxes with Binding

• rating: TODO

.

Five Axioms of Alpha-Conversion

• rating: 1

.

Don’t Substitute Into Abstractions (Functional Pearl)

• rating: TODO

.

Abstract Binding Trees, Dynamics and Statics

• rating: 1

This is an assignment for the course 15-312: Principles of Programming Languages, at CMU, but it describes the ML library used for Abstract Binding Trees used at CMU, and has some interesting information about it. The function out transform a value of type t to a value of type t view, and into does the reverse. In their words,

The idea behind a view is that it is a type whose values represent a one-step unfolding of a value of the abstract type t.

In particular, out on a binder instantiates the bound variable in the binder with a fresh free variable.

Viewing λ-terms through Maps

• rating: TODO

.

How do real-world proof assistants bind variables and check equality?

• rating: 1

.

mathink/mslambda: Map, Skeleton, Lambda term.

• rating: 1

See also the paper this is based on: [Viewing λ-terms through Maps][].

bacam/sato-maps-agda

• rating: 1

See also the paper this is based on: [Viewing λ-terms through Maps][].

jsiek/abstract-binding-trees: Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

• rating: 1

Mostly for the write-up, which, although written in Agda and thus cast in type theory, makes a few points about ABTs.