nat : type.
nat/z : nat.
nat/s : nat -> nat.
nat/plus : nat -> nat -> nat.
which are implemented as standard peano arithmetic. This we will take as our base for natural numbers. We are concerned with a language encoding expressions. In these expressions, variables might occur. In a direct-style semantics one would define expression trees like:
var : type.
mkVar : nat -> var.
exp : type.
exp/n : nat -> exp.
exp/v : var -> exp.
exp/plus : exp -> exp -> exp.
First, we introduce a type of variables. There is a single constructor making variables be indexed by natural numbers. Then we straightforwardly define our expression language. A simple syntax tree for this language might look like
which forces us to handle everything directly. We need to handle the variable as if we were writing a compiler. The way out of the misery is to kill variables and steal them from LF. An earlier post already hinted at this. We simply define our language as
exp : type.
exp/n : nat -> exp.
exp/plus : exp -> exp -> exp.
and then, whenever we want to represent an exp, we represent it as exp -> exp. In other words we introduce a lambda-expression with a hole for where the variable would be:
I hope the drawing is mostly clear: The circle is a place where a lambda-bound variable would be and the dotted line links this "hole" to the spot in the abstract syntax tree where it links. The drawing is more or less the one I had in my head when I first realized why HOAS is clever.
By wrapping more and more lambdas around a single expression, we would have a way to represent a complete expression with more than one variable. One will have to do a lot more to make the above toy-example actually work out: When executing the expression, we must have another expression to substitute for each variable. Of course, substitution is application from the lambda calculus followed by beta-reduction. In Twelf, the representation is
[x : exp] (exp/plus (exp/n 3) x).
and then it becomes clear that we use the LF-variable x to play the role of the variable x in the expression language we have formalized.
