complete type inference for `Expr`

[Memorytaco]

The following three articles should cover most problems to be solved except the omega part and predicate constraint part.

1. Botlan, Didier Le and Didier Rémy. “MLF: raising ML to the power of system F.” ACM SIGPLAN International Conference on Functional Programming (2003).
2. Rémy, Didier and Boris Yakobowski. “A graphical presentation of MLF types with a linear-time unification algorithm.” ACM SIGPLAN International Workshop on Types In Languages Design And Implementation (2007).
3. Rémy, Didier and Boris Yakobowski. “From ML to MLF: graphic type constraints with efficient type inference.” ACM SIGPLAN International Conference on Functional Programming (2008).

[Memorytaco]

And articles referenced here should provide us a good hint how MLFω should behave.

1. Herms, Paolo. “Partial Type Inference with Higher-Order Types.” (2009).
2. Scherer, Gabriel. “Internship report : Extending ML F with Higher-Order Types.” (2010).

[Memorytaco]

Haskell happens to have a great library named fgl, and one transformation from parsed type AST to its graph representation is done under module Inference.Graph and unification is on the way.

[Memorytaco]

For detailed technical introduction of graphic presentation of MLF, please refer to this great thesis (English version and French version) :

1. Boris Yakobowski. Graphical types and constraints - second-order polymorphism and inference. Software Engineering [cs.SE]. Université Paris-Diderot - Paris VII, 2008. English.
2. Yakobowski, Boris. “Graphical types and constraints - second-order polymorphism and inference. (Types et contraintes graphiques - polymorphisme de second ordre et inférence).” (2008).

[Memorytaco]

Since there is no special top level syntax for function, we need to handle the complex type inference of lambda. This is tricky when pattern match is involved, which means concepts like typed path polymorphism or pure pattern calculus are introduced.

1. Jay, C. Barry and Delia Kesner. “Pure Pattern Calculus.” European Symposium on Programming (2006).

Current solution or work around should be dropping the pattern match feature out, and deal with variables only. Let's see whether we will have methods to deal with this later. (maybe elaborate pattern calculus into simpler form?)

[Memorytaco]

Need more comments here. This could be most complex thing in this project.

Yet, i made some progress here.

1. MLF is a good candidate for core language and two variants need to be implemented in compiler.
2. Inference can be done using graph constraint, and we get a framework as a bonus to do constraint resolution, in which constraint as a feature can opt in. Inference or unification using graph in haskell is not tedious and seems a practical choice.
3. Unification is completed 90%, and i have encountered some problems to check correctness of unified result(for permission of each node to maintain a well formed type) . And also algorithms to transform graph type back to syntactic type are not determined.
4. It is, as author claimed, a framework for type inference and it could be a good candidate for constraint resolution which should do something with qualified type for MLF. However, i have little experience on dealing with constraint so i can't figure out a way to add constraint into this type system.
5. One thing is confirmed. A combination of MLF and SystemFC should be enough for a day to day use to make this language practical.

[Memorytaco]

A workflow has been done so we mark this as "Done", even with that there is no complete full type inference available.

see this commit.