type unification

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:


[1]/tmp$ cat > occ.hs   
occ xs = occ (head xs)                                                           
[0]/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.

Advertisements

~ by pulotka on 2009/02/22.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

 
%d bloggers like this: