A language by itself isn’t much use—we need some reasoning rules and algorithms to make it useful. That’s what we’ll cover here. The core inference rule is actually quite simple: if you have a function f that expects some value of type A, and you have a value x of type C such that A and C match in some way, then f(x) is firstly OK and also it has type B.

| f : A -> B x : C |

| -------------------- if A = C |

| f(x) : B |

Notice that this rule doesn’t “do” anything—it just says how we can relate bits of information. So next we can think about the two key algorithms: type inference and type checking.

Inference takes a piece of code and works out what the type could be, and most versions walk through a syntax tree ...

Start Free Trial

No credit card required