[Haskell-cafe] Q: haskell type inference algorithm paper

[Di Xu]

Thanks a lot for these paper reference and detailed explanation. I have a
lot to read now ;)


> Here's a reasonable plan:
>
> 1) Start with so-called "Unification" [1]. Try manually inferring the
> types of some Haskell fragments to get a sense of how it applies. The
> connection should emerge as clear as day.
>
> 2) Next, study Damas-Hindley-Milner. Gain a sense of what motivates
> 'principal types', why they're useful, as opposed to a situation where they
> are impossible to infer.
>
> 3) Finally, there's type classes. I don't know if typed clojure has them
> or not, but this is really what separates Haskell from, say, Lazy ML (LML).
> Be warned, this is where it gets gnarly.
>
> [1] http://en.wikipedia.org/wiki/Unification_%28computer_science%29
>

Wow, thanks for this such a detailed plan, I'm also new to type system, it
seems that all the later type inference algorithm is base on
Damas-Hindley-Milner, I must start from here.

The feature that typed clojure misses is some ability to do fully automatic
type inference, here are some example:

map is a polymorphic function with type `(a -> b) -> [a] -> [b]`, and so
does identity function of type `a -> a`, here are invocation: `map identity
[1,2,3]`, haskell could successfully inference its type, but typed clojure
is unable to do this fully automatically, we had to instantiate either map
or identity manually.

The author of typed clojure given me this
paper<http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7265>,
and to quote from paper:

When a polymorphic function is given an anonymous function as argument, we
have a situation where either one of these techniques can be used to infer
some type annotations, but not both at the same time. For example, in the
term map (fun x -> x) [1,2,3], we cannot infer both the type arguments to
map and the annotation on the function parameter x for the following
reason. We take the simple approach that all the the arguments' types must
be determined before calculation of any missing type arguments. This means
that the type of the anonymous function must be synthesized with the
concrete type of its parameter not available from the context. This
synthesis immediately fails, since the parameter is not annotated with its
type.


So, I'd like to know how haskell solved this problem?

Thanks
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140225/a41cecbd/attachment.html>