# 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"]]
```