An abstract syntax tree is abstract because it is a mathematical object that has certain structure by its very nature. For instance, in first-order abstract syntax trees, as commonly used in compilers, the tree structure implies the subexpression relation, meaning that no parentheses are required to disambiguate programs. HOAS exposes additional structure: the relationship between variables and their binding sites. In FOAS representations, a variable is typically represented with an identifier, with the relation between binding site and use being indicated by using the same identifier. With HOAS, there is no name for the variable; each use of the variable refers directly to the binding site. There are a number of reasons why this technique is useful. First, it makes the binding structure of a program explicit: just as there is no need toexplainoperator precedence in a FOAS representation, there is no need to have the rules of binding and scope at hand to interpret a HOAS representation. Second, programs that are alpha-equivalent have identical representations in HOAS, which can make equivalence checking more efficient.
Implementation
One mathematical object that could be used to implement HOAS is a graph where variables are associated with their binding sites via edges. Another popular way to implement HOAS is with de Bruijn indices.
Use in logical frameworks
In the domain of logical frameworks, the term higher-order abstract syntax is usually used to refer to a specific representation that uses the binders of the meta-language to encode the binding structure of the object language. For instance, the logical frameworkLF has a λ-construct, which has arrow type. A first-order encoding of an object language constructlet would be : exp : type. var : type. v : var -> exp. let : exp -> var -> exp -> exp. Here, exp is the family of object language expressions. The family var is the representation of variables ; the constant v witnesses the fact that variables are expressions. The constant let is an expression that takes three arguments: an expression, a variable and another expression. The canonical HOAS representation of the same object language would be: exp : type. let : exp -> -> exp. In this representation, object level variables do not appear explicitly. The constant let takes an expression and a meta-level function exp → exp . This function is the higher-order part: an expression with a free variable is represented as an expression with holes that are filled in by the meta-level function when applied. As a concrete example, we would construct the object level expression let x = 1 + 2 in x + 3 using the HOAS signature above as let where e is Twelf's syntax for the function. This specific representation has advantages beyond the ones above: for one, by reusing the meta-level notion of binding, the encoding enjoys properties such as type-preserving substitution without the need to define/prove them. In this way using HOAS can drastically reduce the amount of boilerplate code having to do with binding in an encoding. Higher-order abstract syntax is generally only applicable when object language variables can be understood as variables in the mathematical sense. This is often, but not always, the case: for instance, there are no advantages to be gained from a HOAS encoding of dynamic scope as it appears in some dialects of Lisp because dynamically scoped variables do not act like mathematical variables.
