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 ...
Get Functional Programming: A PragPub Anthology now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.