To refine Alejandro's answer a bit: The OutsideIn(X) paper is really the one to read. It's long, but I think it would have to be! The later papers he mentions describe enhancements to the internal, typed language (called variously System FC or GHC Core -- they're more or less the same). With these enhancements came some changes to type inference, but not major ones. The "Promotion" paper describes a bit about polymorphic kind inference in datatype definitions, but the details aren't really there. The "Closed Type Families" paper does not really address type inference, as the closed type families feature (somewhat surprisingly) doesn't interact much with type inference at all. It would be great to see this work be adopted into another language. Good luck! Richard On Feb 25, 2014, at 8:46 AM, Alejandro Serrano Mena wrote:

The current version of GHC does type inference by (an advanced version of) the OutsideIn(X) algorithm. You can check the original paper at http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp... The initial algorithm was then enhanced with datatype promotion and closed type families, which you can learn about in "Giving Haskell a Promotion" and "Closed Type Families with Overlapping Equations".

2014-02-25 14:38 GMT+01:00 Di Xu : Hi, all

I'm new to haskell, I'm learning haskell for its type system, and I found haskell type inference is excellent, I'm interested in its type inference algorithm, could you give me some paper or material reference that describe the haskell type inference algorithm? I want to port it to typed clojure.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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 paperhttp://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