Several times i’ve tried poking into what exactly type inferencing is and how it works; even working through several chapters of the math in the brick book. It was still entirely unclear what type inferencing was.
After poking around some more i finally picked up enough hints to get it. It’s incredibly simple if you explain how it works before you go nuts with the math behind it: unification. Yes, that’s the same unification as seen in languages like prolog.
It’s obvious. It makes perfect sense.
Playing around with the Real World Haskell book i got an extra confirmation:
/tmp$ cat > occ.hs occ xs = occ (head xs) /tmp$ ghci GHCi, version 6.8.2: http://www.haskell.org/ghc/ :? for help Loading package base ... linking ... done. Prelude> :l occ [1 of 1] Compiling Main ( occ.hs, interpreted ) occ.hs:1:9: Occurs check: cannot construct the infinite type: a = [a] Expected type: a -> t Inferred type: [a] -> t In the expression: occ (head xs) In the definition of `occ': occ xs = occ (head xs) Failed, modules loaded: none.
Yep, you can get the occurs check from the type system.
Hindley and Milner are probably great chaps, but it would save a lot of confusion if we just called it type unification already.