Introduction to Twelf

I always spend some time during my summer holidays learning a new programming language. First was Python a couple of years ago, then Ruby and finally Haskell last summer. This summer I have decided to learn Twelf. The only reason that I have heard of Twelf is because of my friend, Jesper Louis, who keeps talking about it, due to his use of it for our Ex-SML project and this really annoyed me because I did not know what he was talking about.

Twelf is very different from any other programming language that I have ever played with. Twelf is an implementation of the logical framework – called LF – and it is used for logical programming and to formalise programming language theory.

From Twelf’s website:

Twelf is a language used to specify, implement, and prove properties of deductive systems such as programming languages and logics. Large research projects using Twelf include the TALT typed assembly language, a foundational proof-carrying-code system, and a type safety proof for Standard ML.

Twelf’s website is very useful and is, honestly, the only website available on the internet with a plethora of information about the language. You can find some decent tutorials if you look at some of the university websites out there (CMU especially has some very interesting slides about Twelf on their website).

I am going to give a short example on how to implement the factorial function in Twelf and hopefully this will enable you to understand Twelf a bit better than before you read this post.

Example

There are tons of small examples on Twelf’s website, but here is another one. We are going to implement the factorial function in Twelf. The factorial function is, for functional programming languages, what “Hello World” is for imperative programming languages – the first function you will see when you open a book about the language.

The factorial function can be defined recursively as this:

$$ n! = \begin{cases} 1 & \text{if } n = 0 \cr n (n - 1)! & \text{if } n > 0 \end{cases} \qquad \forall n \in \mathbb{N} $$

That is easy to implement in most programming languages. In a functional programming language, like Haskell, it can be implemented with pattern-matching so:

factorial :: Int -> Int
factorial 0 = 1
factorial n | n > 0 = n * factorial (n - 1)

In particular, notice how much the pattern-matching method looks like the formula listed above.

It is nowhere near as easy to implement this in Twelf. The first issues we will encounter are:

• Twelf has no knowledge of numbers. We really take that for granted in any modern programming language (for a very good reason: adding numbers to a language every time you have to write anything feels a bit like reinventing the wheel over and over again);

• Twelf has no arithmetic operators at all. We need to define all of those and the numbers via the type-system of Twelf.

The Natural Numbers

The first thing we need to define is the natural numbers ($\mathbb{N} = {0,1,2,\ldots}$). We are going to do that with Peano axioms which map well into the Twelf type-system. First we need to define a type for the natural numbers, and then two relations for it.

In Twelf we write:

nat : type.
nat/zero : nat.
nat/succ : nat -> nat.

This says: nat is a type, nat/zero is of the type nat and is going to be the type that represents the natural number zero, nat/succ is the successor of the former natural number. This way we have zero as nat/zero, one as nat/succ nat/zero, two as nat/succ (nat/succ nat/zero) and so on. It is already beginning to get a bit disturbing, right?

We also need to be able to perform some basic arithmetic on the Peano numbers. We have to implement both addition and multiplication (since the latter requires the former) to be able to finally implement factorial in Twelf.

Addition on Peano numbers is defined recursively as:

$$ \eqalign{ a + 0 &= a \cr a + Succ(b) &= Succ(a + b) } $$

We need to convert this from the infix-notation above to something that fits into Twelf (Twelf is able to do infix-operators via the %infix-statement). Putting it together in Twelf will result in this:

plus : nat -> nat -> nat -> type.
plus/zero : plus nat/zero B B.
plus/succ : plus (nat/succ A) B (nat/succ C) <- plus A B C.

Multiplication is defined using addition and this is also done recursively, like so:

$$ \eqalign{ a \cdot 0 &= 0 \cr a \cdot Succ(b) &= a + (a \cdot b) } $$

And in Twelf:

mult : nat -> nat -> nat -> type.
mult/zero : mult nat/zero B nat/zero.
mult/succ : mult (nat/succ A) B C' <- plus B C C' <- mult A B C.

The only operation that we are missing is to be able to do $a - 1$, which can easily be defined with:

pred : nat -> nat -> type.
pred/s : pred (nat/succ A) A.

This works for what we are going to use, but it won’t work for someone who decides to do a $0 - 1$, since our system does not have any knowledge of negative numbers. However, we are never going to reach this in our factorial function (since we have a case for $n = 0$) and we are simply going to ignore this issue for now.

The Factorial Relation

The final relation that we have to define in Twelf is our factorial-relation, which can be defined in the form of the previous defined relations thusly:

factorial : nat -> nat -> type.
factorial/z : factorial nat/zero (nat/succ nat/zero).
factorial/s : factorial N R <- pred N N' <- factorial N' R' <- mult N R' R.

Testing

Twelf has a very nice declaration called %query where we can query (Prolog-style) a relation for a value. In most programming languages, we are used to functions being one-way. For instance, a function takes an argument and returns a value. With Twelf you can do it the other way around and ask for the input value for a given output value.

To query Twelf for the value of X in the equation $2 + 1 = X$, we write:

%query 1 1 plus (nat/succ (nat/succ nat/zero)) (nat/succ nat/zero) X.

And Twelf will reply with the answer:

---------- Solution 1 ----------
X = nat/succ (nat/succ (nat/succ nat/zero)).

One thing I discovered pretty quickly after I started playing around with Twelf, is that it becomes really tedious to work with Peano axioms like this. To make it a bit less annoying you can do the following:

0 : nat = nat/zero.
1 : nat = nat/succ 0.
2 : nat = nat/succ 1.
3 : nat = nat/succ 2.

And so on. This makes it possible to use “normal” numbers in your queries, but the answer will still be in the annoying format.

Getting the result of the factorial relation can be done in the same manner. With factorial we have two interesting cases. One where the input is zero and one where the input is larger than zero.

The output from Twelf with $n = 0$ and $n = 3$:

%query 1 1 factorial 0 X.
---------- Solution 1 ----------
X = nat/succ nat/zero.

%query 1 1 factorial 3 X.
---------- Solution 1 ----------
X = nat/succ (nat/succ (nat/succ (nat/succ (nat/succ (nat/succ nat/zero))))).

Both results are correct, but you will soon begin to really dislike the output-format – especially if you start trying with an $n$ value larger than $4$.

Conclusion

Twelf is fun to play with, but I do not have much use for it other than to be able to read the code. It is worth playing with if you want to try “a completely different programming language”.

We are going to use it in the Ex-SML project (a Moscow ML fork using LLVM as backend) to prove that the internal Lambda language is actually type-safe. Currently Moscow ML converts SML into the (currently) untyped Lambda language before it is turned into bytecode that runs on a virtual machine named Zinc. Our problem is that LLVM’s assembly language is typed, so we actually need to keep the type-information during every phase of the compilation.