PFPL Chapter 4: Type Judgements

Chapter 4 plunges us straight into type judgements, and they take a bit of explaining if you haven't seen them before.

The goal of this chapter is to find out how a programming language knows what type a value has. It's obvious to us that "fearful" ^ "symmetry" is a string, and 3 * (4 + 5) is a number, but how can a computer figure that out?

Let's start with the second case. The abstract syntax tree for 3 * (4 + 5) looks like this:

tree ["*", "3", ["+", "4", "5"]]  

We can start by noticing that each number is of type num - that's rule 4.1c in the text.

AST:  
tree ["times", "3", ["plus", "4", "5"]]  
Types:  
tree ["???", "num", ["???", "num", "num"]]  

Also, rule 4.1d tells us that if e1 and e2 both have type num, then so does e1+e2:

AST:  
tree ["times", "3", ["plus", "4", "5"]]  
Types:  
tree ["???", "num", ["num", "num", "num"]]  

And rule 4.1e tells us that num * num has type num:

AST:  
tree ["times", "3", ["plus", "4", "5"]]  
Types:  
tree ["num", "num", ["num", "num", "num"]]  

We can use rules 4.1b and 4.1f to do the same for "fearful" ^ "symmetry".

Variables and let bindings

Now let's throw a variable into the mix:

  let x be "Tyger"
   in len(x) - 1

This let...in syntax may be unfamiliar, but it's just setting up a local variable x, and then evaluating an expression using it. Functional languages do this to make it completely clear what the scope of the variable is going to be. The whole let block is the result of len(x) - 1.

The AST looks like this:

tree ["let", "\"Tyger\"", "x", ["+", ["len", ["x"]], "1"]]  

Rule 4.1g lets us deduce that if x is a string, then len(x) is a number, and as before we can then deduce that len(x)-1 is a number:

AST:  
tree ["let", "\"Tyger\"", "x", ["+", ["len", ["x"]], "1"]]  
Types:  
tree ["???", "str", "str", ["num", ["num", ["str"]], "num"]]  

And finally, we can use the most complicated rule of them all, 4.1h, which says that the type of a let block is the type of the expression after the in keyword, to deduce the type of the whole expression as num.

AST:  
tree ["let", "\"Tyger\"", "x", ["+", ["len", ["x"]], "1"]]  
Types:  
tree ["num", "str", "str", ["num", ["num", ["str"]], "num"]]