3.5 Binders

The   typical case of binder comes from the simple -calculus (or ML-like languages). If we use a first-order abstract syntax we can simply define the expression as:

lambda : Id # Exp -> Exp;

If   we choose a second-order abstract syntax, as the syntactical type of is Exp -> Exp we declare:

lambda : (Id:Exp -> Exp) -> Exp;

This definition express both the fact that a lambda has a functional type and that the binder is concretely represented by an identifier.

Note that the first-order abstract syntax generated by this two declarations are identical.

The abstract syntax for a binder may seems distant from the concrete syntax. For example, in the typed -calculus expression , T is not in the scope of x, and so the correct abstract syntax (even in the first-order case) for this expression is:

lambda : Type # Binder -> Exp;
binder : (Id:Exp -> Exp) -> Binder;

AS does not allow a general higher-order abstract syntax, as for example -prolog. Only a second-order abstract syntax is permitted, and an operator must be declared for each higher-order type. This means that declarations like op : (X -> X) -> (X -> X) -> X in -Prolog are not possible in AS. One will have to give more operators as in the following example.

op : Binder # Binder -> X;
binder : (Id:X -> X) -> Binder;

Second-order operators