Abbot is a tool for the automatic generation of implementations for abstract binding trees with the locally nameless representation. Abstract syntax trees are quite natural to express as Standard ML datatypes, but the abstract binding trees described in Harper's Practical Foundations of Programming Languages are tricker due to the necessity of alpha-equivalence and avoiding variable capture.
A reasonable implementation strategy for abstract binding trees keeps ABTs as an abstract type; whenever a bound variable is exposed, it is given a globally fresh name that ensures its uniqueness. Such an implementation avoids many potential errors that can happen because of shadowing. However, implementing this interface for each language that we might be interested in would be tedious and error-prone in the extreme.
One solution, which has been used successfully for large projects like Tom Murphy's ML5/pgh compiler, is to implement a library for ABTs, a functor parameterized by a set of operators. An ABT in the library implementation is either:
A variable
- view: ` x
- constructor: `` x
An abstract binding site
- view: \ (x,t)
- constructor: \\ (x,t)
An operator and a list of sub-abts
- view: oper $ [t1,...,tn]
- constructor: oper $$ [t1,...,tn]
Each operator has an arity, which determines both the number of subexpressions and the location of abstract binding sites. In the untyped lambda calculus, there is one operator Lam with one subexpression that binds one variable, and another Ap with two subexpressions that bind no variables. Small-step evaluation for the untyped lambda calculus looks like this:
fun trystep exp =
(case out exp of
` x => raise Malformed
| \ (x, exp) => raise Malformed
| Lam $ [exp'] => VAL
| Ap $ [exp1, exp2] =>
(case trystep exp1 of
STEPS exp1' => STEPS (Ap $$ [exp1', exp2])
| VAL =>
(case trystep exp2 of
STEPS exp2' => STEPS (Ap $$ [exp1, exp2'])
| VAL =>
(case out exp1 of
Lam $ [exp1'] =>
(case out exp1' of
\ (x, exp0) => subst exp2 x exp0
| _ => raise Malformed)
| _ => raise Malformed))))
Abbot takes a code generation approach to ABT specification. Instead of the operators and the corresponding information about their airities being passed to a functor, we can specify
abt exp = Lam (exp.exp) | Ap (exp, exp)
Abbot takes this specification and compiles it into Standard ML signature specific to that abstract binding tree spec:
signature EXP_VAR =
sig
type expVar
type t = expVar
val newvar: string -> expVar
val equal: (expVar * expVar) -> bool
val compare: (expVar * expVar) -> order
val toString: expVar -> string
val hash: expVar -> int
end
(* Implementation of normal sorts *)
signature EXP =
sig
type exp (* = Exp.t *)
type expVar (* = Exp.Var.t *)
type t = exp
structure Var: EXP_VAR where type expVar = expVar
datatype 'exp expView
= Var of Exp.Var.t
| Lam
| Ap of 'exp * 'exp
val Var' : expVar -> exp
val Lam': exp
val Ap': exp * exp -> exp
val into: exp expView -> exp
val out: exp -> exp expView
val aequiv: exp * exp -> bool
val toString: exp -> string
val subst: exp -> expVar -> exp -> exp
end
structure Exp: EXP
Code using Abbot-generated signatures looks about the same, but makes better use of Standard ML's type system to ensure correctness; instead of using operators and the infixed $ constructor, our views are normal-looking SML datatypes.
One significant difference from using Abbot is that binding sites are now automatically exposed along with the constructor they are attached to. This makes the reduction step in our example a little more concise.
fun trystep exp =
(case out exp of
Var _ => raise Malformed
| Lam (x, exp') => VAL
| Ap (exp1, exp2) =>
(case trystep exp1 of
STEPS exp1' => STEPS (Ap' (exp1', exp2))
| VAL =>
(case trystep exp2 of
STEPS exp2' => STEPS (Ap' (exp1, exp2'))
| VAL =>
(case out exp1 of
Lam (x, exp0) => subst exp2 x exp0
| _ => raise Malformed))))
The pretty concrete syntax for Abbot isn't connected to a frontend yet; the SML representation of a few datatypes is in analysis.sml, and the output of Abbot can be seen in the examples directory.