Skip to content

Chapter 3

What is what

A Haskell program can be written with no types at all. The compiler finds them anyway. This chapter shows how the compiler guesses the type of everything, and how its guesses are always right.

Everything has a type

True is a Bool. 'a' is a Char. (True, 'a') is a pair of the two. A function that takes a Bool and gives a Char has the type Bool -> Char.

In Haskell, you can write the type of a thing above its definition. Most programmers do, because a type is a good comment that cannot go stale. But you do not have to. When you leave the type out, the compiler works it out from the code. A programmer calls this type inference. In aihc, the component aihc-tc does it.

Watch the compiler infer

The playground below runs the type checker of aihc on your code. On the right, it shows the same code with the types it inferred, as signatures above each definition.

x = ()

double n = n + n

twice f a = f (f a)

pair = (True, "hello")

The signature of double says (Num a) => a -> a. Read it as: for any type a that is a number, double takes an a and gives an a. The compiler does not know whether you will use double on an Int or on a Double. So it does not decide. It gives the most general type that works.

The signature of twice has no Num in it. twice never adds anything. It only calls f two times, so f must give back the same type that it takes. That is all the compiler knows about f, and that is exactly what the signature says.

Try this

  • Write swap (a, b) = (b, a). The compiler finds the two types and swaps them.
  • Write apply f = f 1. The argument of f must be a number, so Num appears.
  • Write oops = True + 1. True is not a number. The compiler says what it could not match.

How the guessing works

The compiler does not really guess. It plays a small game of constraints.

Take twice f a = f (f a). At first, the compiler knows nothing. It gives f an unknown type, and a another unknown type. Then it reads the body. f a means that f is a function, and that its argument has the type of a. f (f a) means that the result of f is also something f can take. So the argument type and the result type of f are the same.

Each fact is a small equation. The compiler solves the equations, and the unknowns get filled in. A programmer calls this unification. When every equation has a solution, the program is well typed. When one does not, the compiler stops and tells you which two types it could not match.

The road ahead

Three chapters in, the compiler has read the text, found every name, and worked out every type. It has not changed the program at all. That changes in the next chapter. The compiler rewrites the program into a smaller, stricter language, where nothing is left implicit.

Next chapterThe honest language. Not written yet.