Functional Programming: A PragPub Anthology

Type Inference and Type Checking

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