This year at the London Computation Club, we’ve been reading Types and Programming Languages (TAPL). We covered about half the book, completing three of the book’s six sections: Untyped Systems, Simple Types, and Subtyping. It’s probably the most challenging text we’ve tackled in the club, and certainly one of the most challenging books I’ve read, especially as I have no formal computer science training.
Despite its difficulty, as we got into it I began to find it surprisingly accessible. It is entirely possible to read the book and get a lot out of it even if you approach it informally and skip over all the mathematical proofs. However, to get much out of it you will need to become familiar with one core concept: formal definitions of logical rules for the evaluation and typing of programs. Exploring these rules with code meant that as well as learning the material in the book, I accidentally learned the basics of logic programming, a radically different way of thinking about code if you’re used to imperative systems.
The first formal system we encounter in the book is a very simple language
consisting only of the boolean values true and false, and the conditional
expression if x then y else z. We learn how to formally describe a process for
evaluating expressions in this language, via the following rules.
First, an if-expression whose condition is the literal value true, reduces to
the then-expression. We say that (if true then $t2 else $t3) evaluates to
$t2 in one step, and we use the symbol -> to mean “evaluates in one step
to”. TAPL calls this rule E-IfTrue, and we write it as:
rule E-IfTrue {
(if true then $t2 else $t3) -> $t2
}
Second, an if-expression whose condition is false, reduces to the
else-expression:
rule E-IfFalse {
(if false then $t2 else $t3) -> $t3
}
Finally, if the condition does not yet have a specific value, but can be
reduced, then we reduce the whole if-expression by reducing the condition. This
is written as the following rule, which says that if $t1 evaluates to $t1',
then (if $t1 then $t2 else $t3) evaluates to (if $t1' then $t2 else $t3),
i.e. if the condition is not yet one of the exact values true or false,
then reduce it one step.
rule E-If {
$t1 -> $t1'
---------------------------------------------------------
(if $t1 then $t2 else $t3) -> (if $t1' then $t2 else $t3)
}
The text above the line is the premise of the rule, and the text below the
line is its conclusion. Rules without this line, like E-IfTrue, should be
read as just a conclusion, with no premises: they state things that are true
without depending on any other conditions.
We can use these rules to evaluate nested conditional expressions:
(if (if true then false else true) then false else true) -> ?
Neither E-IfTrue nor E-IfFalse match this statement; the condition of the
outer if-expression does not have the literal value true or false, it is
itself another if-expression. So we need to use E-If to reduce the inner
expression, (if true then false else true).
This inner expression matches E-IfTrue and so we can reduce it directly to
false. We write a proof of this result as:
——————————————————————————————————————— E-IfTrue
(if true then false else true) -> false
The line above the result tells us which rule was used to prove it. We can use this result to evaluate our original if-expression, since we know its condition can be reduced.
——————————————————————————————————————— E-IfTrue
(if true then false else true) -> false
——————————————————————————————————————————————————————————————————————————————————————————— E-If
(if (if true then false else true) then false else true) -> (if false then false else true)
This proof says: because we know from E-IfTrue that (if true then false else
true) evaluates to false, we therefore know by E-If that the outer
expression evaluates to (if false then false else true). We could evaluate
this one more time by applying E-IfFalse:
——————————————————————————————————————— E-IfFalse
(if false then false else true) -> true
From this chain of reasoning, we know that our original expression ultimately
evaluates to true. There are no rules whose conclusion has the form true ->
$t, so this cannot be evaluated further.
This language might not seem especially useful, but this process of defining semantics as a set of formal rules is what lets us prove things about programs, and all the type systems in the book are defined as sets of rules like this.
For example, we can write rules that say both true and false have type
Bool; the symbol : means “has the type”:
rule T-True {
true : Bool
}
rule T-False {
false : Bool
}
Then we can write a more complicated rule for the type of if-expressions. An
if-expression evaluates to either its then-clause or its else-clause, and the
type of an if-expression should match the type of what it evaluates to – in
type systems, this property of the type remaining the same after evaluation is
called preservation. This means that the then- and else-clause should have the
same type. We write this rule to say: if the condition has type Bool, and the
two clauses both have some type $T, then the whole expression has type $T.
(This rule has three premises and they are divided by a / symbol.)
rule T-If {
$t1 : Bool / $t2 : $T / $t3 : $T
--------------------------------
(if $t1 then $t2 else $t3) : $T
}
We can glue these rules together to prove the type of compound expressions, for example:
———————————— T-False ——————————— T-True ———————————— T-False
false : Bool true : Bool false : Bool
———————————————————————————————————————————————————————— T-If
(if false then true else false) : Bool
In this language where booleans are the only type this is not particularly
interesting, but as more forms are added to the language, we write typing rules
for them. For example, we say the value 0 has type Nat, short for “natural
number”.
rule T-Zero {
0 : Nat
}
We also add a function called iszero; iszero 0 evaluates to true and all
other inputs return false. Its typing rule says that if its input has type
Nat, then its result has type Bool.
rule T-IsZero {
$t : Nat
------------------
(iszero $t) : Bool
}
Now we can show that if-expressions can have other types, if their clauses are things other than booleans:
——————————— T-True ——————— T-Zero ——————— T-Zero
true : Bool 0 : Nat 0 : Nat
————————————————————————————————————————————— T-If
(if true then 0 else 0) : Nat
And we can also decide some programs won’t compile, because the types don’t
match. For example, if 0 then true else false cannot be typed, because the
first premise in T-If becomes 0 : Bool, which cannot be matched to any rule.
if true then 0 else false cannot be typed, because 0 and false have
different types and the repeated variable $T in T-If means the types must
match.
We can build arbitrarily nested trees of these proofs as our expressions become more complex:
——————— T-Zero
0 : Nat
————————————————— T-IsZero ——————————— T-True ———————————— T-False
(iszero 0) : Bool true : Bool false : Bool
—————————————————————————————————————————————————————————————— T-If
(if (iszero 0) then true else false) : Bool
TAPL progresses by inventing increasingly sophisticated typing rules that let us put useful constraints on programs and reject those that would crash at runtime. All these typing rules are essentially of the same kind we’ve seen above: a (possibly empty) set of premises followed by a conclusion, containing variables that can be filled in with arbitrary expressions.
The rules as I’ve written them above are very close to how they’re presented in the book, with minor modifications for writing them as ASCII text. In fact, the rules written out like this can be directly interpreted by a library I wrote to implement the ideas in the book: Infer. It’s based on an initial version of the idea, Tom Stuart’s inference-rules, and all it does is attempt to match input statements to the rules, and print a proof if a match can be found. For example, here’s the code for the last example:
rules = Infer.lang('./rules.txt')
expr = Infer.expr('(if (iszero 0) then true else false) : $?')
state = rules.derive(expr).first
Infer.print_derivation(state.build_derivation)
Infer figures out what the value of that variable $? should be, and generates
a proof for the result it found. The process it goes through to do this is
fairly simple. We start with the statement we’re trying to prove:
(if (iszero 0) then true else false) : $?
Infer has almost no built-in syntax; the only rules are that things beginning
with $ are variables, and parentheses group things. Everything else is an
arbitrary meaningless symbol from Infer’s point of view, and all it’s trying to
do is find rules whose conclusions can be made to match this statement.
What do we mean by matching in this context? It means that two sequences of
symbols can be made equal to each other by replacing variables. For example, the
sequences 1 $X 3 and 1 2 $Y can be made equal by setting $X = 2 and $Y
= 3. Occurrences of the same variable must be equal, so for example $X $X
can be made to match 2 2 but not 3 4.
If we look through the rules above, the only one whose conclusion has the right
form to match our target statement is T-If, whose conclusion is
(if $t1 then $t2 else $t3) : $T
We match this against our target statement:
(if (iszero 0) then true else false) : $?
This match gives us:
$t1=(iszero 0)$t2=true$t3=false$T=$?
Then we look at the premises of T-If. First, we require $t1 : Bool, that is
(iszero 0) : Bool. There is a rule whose conclusion matches this: T-IsZero
with (iszero $t) : Bool. This gives us $t = 0, and this rule has premise
$t : Nat, which is satisfied by using T-Zero to show 0 : Nat. That takes
care of the first premise in T-If.
The next premise says that $t2 : $T, and at this point we know $t2 is
true. Is there a rule to match true : $T? Yes: T-True says true : Bool,
so that means $T must be Bool.
Now the final premise: $t3 : $T. We now know both $t3 and $T, so we want
to show that false : Bool, and indeed we can do that using T-False. If we
had previously decided $T was Nat, then we’d be trying to match false :
Nat, and there is no rule that will generate this, so the expression cannot be
typed.
Having proved all the premises, we can apply T-If to conclude the type of the
entire expression, and since we have matched the $? variable to $T, we can
conclude that $? is Bool.
This example demonstrates the basic mechanics of answering questions like “what
type does this expression have”. We phrase the question as a statement like “the
expression has type ?”, and then we match the statement against the rules to
try to find out what ? is. When a rule has premises, we recursively try to
match each of those in the same way, storing the values of variables as we go.
The trace of rules invoked as we match parts of the statement forms a proof of
the statement.
This method might not look very powerful, but it can actually be used to perform
arbitrary computation, and it is the basis of logic programming. Rather
than executing a sequence of statements, as imperative programs do, logic
programs are declarative sets of rules that input queries are matched against.
A query is just any statement we’d like to prove, and it may have variables in
it: (if true then false else true) : $? is a query where we’d like to know the
value of $? if one exists.
Logic programming is radically different to imperative programming, and has some powerful properties. We can view the above rules as defining a function that computes the type of an expression, if it can be typed. Each expression should have a single well-defined type, and so this function should return a single value, as we are used to in imperative languages. However, logic functions don’t have to behave that way: they can generate any number of results, and they can be run “backwards”.
For example, rather than ask for the type of an expression, we could ask for all
the expressions that have type Bool. We’d express this as the query $? :
Bool, and we can evaluate it just as we did before:
expr = Infer.expr('$? : Bool')
rules.derive(expr).each do |state|
Infer.print_derivation(state.build_derivation)
end
This will print a few obvious things that we can reach in one step:
——————————— T-True
true : Bool
It will also print things that require a little more work:
——————— T-Zero
0 : Nat
————————————————— T-IsZero
(iszero 0) : Bool
It will generate complex nested expressions:
——————— T-Zero
0 : Nat
————————————————— T-IsZero ——————— T-Zero ——————— T-Zero
(iszero 0) : Bool 0 : Nat 0 : Nat
————————————————————————————————————————————————————— T-If
(if (iszero 0) then 0 else 0) : Nat
————————————————————————————————————————————— T-IsZero
(iszero (if (iszero 0) then 0 else 0)) : Bool
And it just keeps going, generating an infinite series of all the expressions that have the desired type:
——————— T-Zero
0 : Nat
————————————————— T-IsZero ——————— T-Zero ——————— T-Zero
(iszero 0) : Bool 0 : Nat 0 : Nat
——————————— T-True ——————— T-Zero ————————————————————————————————————————————————————— T-If
true : Bool 0 : Nat (if (iszero 0) then 0 else 0) : Nat
—————————————————————————————————————————————————————————————————————————————————— T-If
(if true then 0 else (if (iszero 0) then 0 else 0)) : Nat
——————————————————————————————————————————————————————————————————— T-IsZero
(iszero (if true then 0 else (if (iszero 0) then 0 else 0))) : Bool
This ability to explore all the possible true statements from a declarative set of rules is core to logic programming, and it makes it particularly good at search and constraint-solving problems.
Generating all possible results like this certainly felt like a neat trick when I first encountered it. (Incidentally, my first encounter with this technique was via a language called microKanren in Tom’s talk Hello, declarative world.) But how does one do real programming? How do we handle state and use data structures? The answer involves a little bit of retraining your brain, so let’s take another example from TAPL.
When we introduce user-defined functions, they look like this: λx: T. t. This
is, the symbol λ (lambda), followed by a parameter x, then the parameter’s
type T, and finally the function’s body, which is a single term t. Here’s an
example function:
λn: Nat. (if (iszero n) then false else true)
When we type-check a program, we recursively go into every sub-expression in the
program and work out its type. To computer the type of (iszero n) above, we
need to know the type of n – we need to remember that the function definition
says that n has type Nat, which would means (iszero n) is a well-typed
expression. We do this with something called a typing context, which is just a
data structure that remembers the types of any parameters that are currently in
scope.
In Ruby, we’d just use a hash for that: { 'x' => Nat }. Each time we enter a
lambda-expression, we add its parameter and type to this hash, and then carry
the hash down into the function’s body as we check its type. But the language
we’ve seen above doesn’t have any apparent data structures, or ways of updating
them, so we need to invent one.
In TAPL, typing contexts are referred to by the letter Γ (gamma). A context is
a list of pairs of parameters and their types. The structure of these lists is
defined recursively; a context is either:
- the empty context,
∅ - a context with a parameter-type pair
x : Tappended
So, these are all valid contexts:
∅
(∅ , x : Bool)
((∅ , x : Bool) , y : Nat)
We can then write a pair of rules for getting the type of a variable in a given
context; the statement Γ ⊢ x : T means “in context Γ, the term x has type
T”. First, we use pattern-matching on the structure of the context: if the
context ends with the pair $x : $T, then the type of $x in the context is
$T.
rule T-Var-1 {
($Γ, $x : $T) ⊢ $x : $T
}
Then we write a case for when the parameter doesn’t match the last pair in the
context. By writing ($Γ, $y : $S), we destructure the context into its final
pair $y : $S and everything before it, $Γ. The premise says that if $x has
type $T in this reduced context, then it has the same type in the reduced
context with one pair added.
rule T-Var-2 {
$Γ ⊢ $x : $T
-----------------------
($Γ, $y : $S) ⊢ $x : $T
}
These rules define a recursive method for looking up the type of a parameter in a list of key-value pairs. Here are a couple of proofs that show the recursion working, first for the base case:
————————————————————————— T-Var-1
(∅ , x : Bool) ⊢ x : Bool
And then for the recursive case:
——————————————————————— T-Var-1
(∅ , y : Nat) ⊢ y : Nat
———————————————————————————————————— T-Var-2
((∅ , y : Nat) , x : Bool) ⊢ y : Nat
(These were derived by entering a query like (∅ , x : Bool) ⊢ x : $?.)
We can now use this typing-context abstraction to write a rule for computing the
type of a function. This rule says that in context Γ a function λx: T. t has
type T → S if, in the extended context (Γ, x: T), the body t has type S.
rule T-Abs {
($Γ, $x : $T) ⊢ $t : $S
---------------------------------
$Γ ⊢ (λ $x : $T . $t) : ($T → $S)
}
At this point all the other rules must be extended with rules to pass the
context around; all we need to do is add $Γ ⊢ to the start of each premise and
conclusion, for example:
rule T-Zero {
$Γ ⊢ 0 : Nat
}
rule T-IsZero {
$Γ ⊢ $t : Nat
-----------------------
$Γ ⊢ (iszero $t) : Bool
}
Now we can run a query to see if we can figure out the type of an expression inside a function:
query: ∅ ⊢ (λn: Nat. (iszero n)) : $?
——————————————————————— T-Var-1
(∅ , n : Nat) ⊢ n : Nat
————————————————————————————————— T-IsZero
(∅ , n : Nat) ⊢ (iszero n) : Bool
——————————————————————————————————————————— T-Abs
∅ ⊢ (λ n : Nat . (iszero n)) : (Nat → Bool)
Indeed we can. Let’s try something more complex to make sure the context is passed down into sub-expressions:
query: ∅ ⊢ (λn: Nat. (if (iszero n) then false else true)) : $?
——————————————————————— T-Var-1
(∅ , n : Nat) ⊢ n : Nat
————————————————————————————————— T-IsZero ———————————————————————————— T-False ——————————————————————————— T-True
(∅ , n : Nat) ⊢ (iszero n) : Bool (∅ , n : Nat) ⊢ false : Bool (∅ , n : Nat) ⊢ true : Bool
——————————————————————————————————————————————————————————————————————————————————————————————————————————————— T-If
(∅ , n : Nat) ⊢ (if (iszero n) then false else true) : Bool
————————————————————————————————————————————————————————————————————— T-Abs
∅ ⊢ (λ n : Nat . (if (iszero n) then false else true)) : (Nat → Bool)
Implementing the various language extensions and subtyping rules in TAPL is excellent practice in expressing rules as executable logic programs, and you’ll soon discover you can get a very long way by using pairs of rules to recursively pattern-match over nested structures. A good example of this is the rules for records, a key-value pair structure that’s used repeatedly in the text. Some more advanced patterns can be found in my implementation of joins and meets, the rules for finding common supertypes and subtypes which are used in the subtyping relation.
So finally, what does this all have to do with Prolog? Well Prolog is probably the best-known logic programming language. One of our group, Simon Coffey, was using it in his implementation, and he gave me a lot of help in learning it and figuring out my own logic rules. Through his explanations, I realised that this language that had always looked bizarre and impenetrable to me was actually the thing I’d just spent months learning and implementing! The language I’d cooked up for doing TAPL was just a small subset of Prolog with different syntax.
Here’s the same rules written in Prolog. Instead of premises followed by a line
then a conclusion, Prolog rules put the conclusion first, then the symbol :-,
then the premises. Expressions in Prolog are not quite as free-form as in Infer;
they must take the form a(b, c, ...). Variables begin with uppercase letters,
and everything else is an arbitrary symbol. Prolog also has lists, written [a,
b, c, ...], or [a | b] where a is the first element and b is the rest of
the list. See if you can match these rules to how they’re written above.
% types.pl
% T-True
has_type(_, true, bool).
% T-False
has_type(_, false, bool).
% T-If
has_type(Ctx, if(Cond, Then, Else), T) :-
has_type(Ctx, Cond, bool),
has_type(Ctx, Then, T),
has_type(Ctx, Else, T).
% T-Zero
has_type(_, 0, nat).
% T-IsZero
has_type(Ctx, iszero(T), bool) :- has_type(Ctx, T, nat).
% T-Var-1
has_type([[X, T] | _], X, T).
% T-Var-2
has_type([_ | Ctx], X, T) :- has_type(Ctx, X, T).
% T-Abs
has_type(Ctx, λ(X, T, Body), fn(T, S)) :-
has_type([[X, T] | Ctx], Body, S).
You can download a Prolog implementation like SWI Prolog, load this file into it and run queries:
$ swipl types.pl
?- has_type([], λ(n, nat, if(iszero(n), false, true)), T).
T = fn(nat, bool).
Because I had most of the machinery necessary to run logic programs, I decided to stick a different parser on the front and bootstrap a Prolog implementation of my own. Because Infer has a module for printing the proof tree of any result, I could then use this to show traces of my Prolog code, which was really useful while learning. Here’s a Ruby snippet for proving the above statement:
types = Infer::Prolog.program(File.read('types.pl'))
expr = 'has_type([], λ(n, nat, if(iszero(n), false, true)), T).'
Infer::Prolog.execute_and_print(types, expr)
And the result:
————————————————————————————
has_type([[n, nat]], n, nat)
————————————————————————————————————— ————————————————————————————————— ————————————————————————————————
has_type([[n, nat]], iszero(n), bool) has_type([[n, nat]], false, bool) has_type([[n, nat]], true, bool)
——————————————————————————————————————————————————————————————————————————————————————————————————————————————————
has_type([[n, nat]], if(iszero(n), false, true), bool)
——————————————————————————————————————————————————————————————————
has_type([], λ(n, nat, if(iszero(n), false, true)), fn(nat, bool))
T = fn(nat, bool)
I’ve barely scratched the surface of Prolog and logic programming here, but hopefully this gives you a flavour of how different it is, and how to solve simple problems with it. It’s a lot like pure functional programming as found in languages like Haskell, but without any distinction between function inputs and outputs. It’s a really good discipline to learn as it forces you to formalise your understanding of a problem and prove things about it. And, it goes to show how trying to study one topic can lead you to learn all sorts of other things by accident, just by seeing them in an unexpected context.
