Twelf - Introduction

Introduction

At its simplest, a Twelf program (called a "signature") is a collection of declarations of type families and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, with z standing for zero and s the successor operator.

nat : type. z : nat. s : nat -> nat.

Here nat is a type, and z and s are constant terms. As a dependently-typed system, types can be indexed by terms, which allows the definition of more interesting type families (relations). Here is a definition of addition:

plus : nat -> nat -> nat -> type. plus_zero : {M:nat} plus M z M. plus_succ : {M:nat} {N:nat} {P:nat} plus M (s N) (s P) <- plus M N P.

The type family plus is read as a relation between three natural numbers M, N and P, such that M + N = P. We then give the constants that define the relation: plus_zero indicates that any natural number M plus zero is still M. The quantifier {M:nat} can be read as "for all M of type nat".

The constant plus_succ defines the case for when the second argument is the successor of some other number N (see pattern matching). The result is the successor of P, where P is the sum of M and N. This recursive call is made via the subgoal plus M N P, introduced with <-. The arrow can be understood operationally as Prolog's :-, or as logical implication ("if M + N = P, then M + (s N) = (s P)"), or most faithfully to the type theory, as the type of the constant plus_succ ("when given a term of type plus M N P, return a term of type plus M (s N) (s P)").

Twelf features type reconstruction and supports implicit parameters, so in practice one usually does not need to explicitly write {M:nat} (etc.) above.

These simple examples do not display LF's higher-order features, nor any of its theorem checking capabilities. See the Twelf distribution for its included examples.