Hindley-Milner Type Inference
Jon Harrop
I'd like to implement the HM type system with type inference in my language
front-end. I once lashed together something that seemed to work but, given
the theoretical foundation behind this, I'd like to follow some more
rigorous guidance this time.
I found an interesting draft paper "Algorithm W Step by Step":
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf
that runs through a basic implementation in Haskell. Although this is
academically interesting, the implementation sucks because it is written in
Haskell (half of the code is just working around lack of mutation!) and it
doesn't implement the interesting bit: the value restriction.
Is there a similar tutorial providing a walkthrough of the construction of a
type inferer for an impure language? For example, what is the inferred type
of the empty array and can that even be represented using the code from
that paper? Also, does anyone have a minimal implementation written in ML?
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
Greg Fitzgerald
On Feb 24, 2010, Jon Harrop wrote:
> Is there a similar tutorial providing a walkthrough of the construction of a
> type inferer for an impure language? For example, what is the inferred type
> of the empty array and can that even be represented using the code from
> that paper? Also, does anyone have a minimal implementation written in ML?
There's an ML implementation of System F in Chapter 25 of Benjamin
Pierce's "Types and Programming Languages."
http://www.cis.upenn.edu/~bcpierce/tapl/index.html
-Greg
Jon Harrop
Isn't System F also purely functional?
Ganesh Sittampalam
> I'd like to implement the HM type system with type inference in my language
> front-end. I once lashed together something that seemed to work but, given
> the theoretical foundation behind this, I'd like to follow some more
> rigorous guidance this time.
>
> I found an interesting draft paper "Algorithm W Step by Step":
>
Another link here since citeseer can be unreliable:
http://www.grabmueller.de/martin/www/pub/AlgorithmW.en.html
> that runs through a basic implementation in Haskell. Although this is
> academically interesting, the implementation sucks because it is written in
> Haskell (half of the code is just working around lack of mutation!)
The only bits I see that could reasonably be considered "working
around lack of mutation" are the definitions of the monadic
infrastructure, which amount to three import lines and about 15-20
lines at the bottom of page 3/top of page 4, some of which would be
needed anyway to initialise/manipulate mutable state directly. That's
not "half the code".
Ganesh
Torben �gidius Mogensen
> Is there a similar tutorial providing a walkthrough of the construction of a
> type inferer for an impure language? For example, what is the inferred type
> of the empty array and can that even be represented using the code from
> that paper? Also, does anyone have a minimal implementation written in ML?
Most ML compilers are written in ML, so you could look at the source
code of these. There are no tutorials to go with them, though. My
guess is that tutorials would skip the complicated parts such as
references, arrays extensible records anyway.
The Moscow ML compiler is fairly straight-forward, so you could start
there.
Torben
Jon Harrop
> Jon Harrop <j...@ffconsultancy.com> writes:
>> Is there a similar tutorial providing a walkthrough of the construction
>> of a type inferer for an impure language? For example, what is the
>> inferred type of the empty array and can that even be represented using
>> the code from that paper? Also, does anyone have a minimal implementation
>> written in ML?
>
> Most ML compilers are written in ML, so you could look at the source
> code of these. There are no tutorials to go with them, though. My
> guess is that tutorials would skip the complicated parts such as
> references, arrays extensible records anyway.
Yes, that's exactly what I'm finding. The tutorials don't cover mutation or
even touch upon value restrictions.
> The Moscow ML compiler is fairly straight-forward, so you could start
> there.
Thanks.