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 ...