Our lambda calculus needs a type system. Some people may argue that this makes the lambda calculus worse, but I will take the stance that a type system adds information to our programs such that we may be able to prove certain properties. The first thing is to define the system. We introduce a new kind of types:

ty : type.

nat : ty.

arrow : ty -> ty -> ty.

We inform Twelf that natural numbers are types. We inform twelf that functions can be formed via the arrow type. (arrow A B) means a function from domain A to codomain B. Naturally, we would like a typing judgement, relating an expression to a type. To do this, we introduce a type family, called ``of'' for exactly this:

of : exp -> ty -> type.

Now, We will tell Twelf about specific relations. We directly have:

of/z : of z nat.
of/s : of (s S) nat
    <- of S nat.

Zero is a natural number. And successors are natural numbers provided that the ``innards'' are. For applications, we need a bit more structure:

of/app : of (app E1 E2) T2
    <- of E1 (arrow T1 T2)
    <- of E2 T1.

An application has a type T2, if the first part of the application has function type (arrow T1 T2) and the value we wish to pass to the function has type T1. Finally, there is the lambda-case. Higher-order abstract types shine here:

of/lam : of (lam [x] E x) (arrow T1 T2)
    <- ({x : exp} of x T1 -> of (E x) T2).

To break it up: The conclusion of the rule (the first line) says that a lambda-expression has arrow type (arrow T1 T2). The premise (second line) says: ``Suppose the variable x is an exp and suppose that x has type T1. Then we must show that (E x) has type T2''. Assumptions like these are all over the place in Twelf proof developments. We now have most of the toolset to construct theorems. But it has to wait for a later post.

This post will, hopefully, explain what Higher order abstract syntax in Twelf is. Suppose we have some natural numbers

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.

My editing speed in acme is now increased tremendously compared to earlier. I am slowly beginning to get a feel of what it is like to edit code. One thing is that you cut and paste a lot of text. Much more than what I did in emacs or vi. One reason is that it is the only way and another is that it is fast. Also, my mousing skills are slowly improving. That is, I am getting a lot faster with the mouse. Having seen some of the administrative support girls at my former job wield the mouse, I am lacking quite much in speed yet. I could also take a look at my brothers who game a lot. They happen to be much faster than I am. I am slowly beginning to learn the sam command set now. There is not that much to learn, so it should be pretty fast.

I have a hypothesis: People like to be in control of their software. That is, people like to have the full empowerment to change anything inside their system. The basic reason for this is simple: If you find a piece of the system that is bad, you want the right to redo that part of the system because you can see it will hamper your work later on. Looking back at a particular project made me realize that I weren't in control of it. We simply were too many hackers with a stake in different aspects of the system. Furthermore, since the system was put into production, there was also the army of marketdroids who wanted their stakes in the system. In effect, depending on how much power you had, parts of the system was carved down in stone. The result was utter disaster: Our data model sucked dead moose through bent straws. Yet nobody had the empowerment to change the data model. Hence, you really had no control of your code. About 70% of the code you wrote for any task was workaround code on the bad data model. This meant complexity skyrocketed to the point where no project could complete. At one point, I suddenly realized that I was not in control of the system that made the most problems. Then I realized that no programmer was in control. All the choice was on the marketdroids, and boy, did they make bad decisions. Rather than focusing on building a better system with a vision for how the components should fit together, they just threw in more stuff on top of the garbage pile. In sports psychology, it is all about focusing on the knobs that you are able to turn, and defocussing on the knobs which are turned for you by luck and coincidence. It is interesting how that knowledge applies to the above. In fact, the only knob you control is your sanity. Then, I realized it was time to move on.