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;