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?

[Greg Fitzgerald]

Hi Jon,

Post by Jon Harrop
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]

Post by Greg Fitzgerald
Hi Jon,

Post by Jon Harrop
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

Isn't System F also purely functional?

[Ganesh Sittampalam]

Post by 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.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=...

Another link here since citeseer can be unreliable:
http://www.grabmueller.de/martin/www/pub/AlgorithmW.en.html

Post by Jon Harrop
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]

Post by Jon Harrop
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]

Post by Torben Ægidius Mogensen

Post by Jon Harrop
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.

Post by Torben Ægidius Mogensen
The Moscow ML compiler is fairly straight-forward, so you could start
there.

Thanks.