Type inference algorithms for functional programing languages.

• Luis Damas, Robin Milner. (1982). Principal type-schemes for functional programs.
• My blog commentary (Japanese)

Type stack exec algorithmW to test some expressions

• Oukseh Lee, Kwangkeun Yi. (1998). Proofs about a Folklore Let-Polymorphic Type Inference Algorithm.
• My blog commentary (Japanese)

Type stack exec algorithmM to test some expressions

• Robin Milner. (1978). A Theory of Type Polymorphism in Programming.
• My blog commentary (Japanese)

Type stack exec algorithmJ to test some expressions

Algorithm M with side effects. I named this algorithm.

Type stack exec algorithmZ to test some expressions

• Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields. (2005). Practical type inference for arbitrary-rank types.

Type stack exec arbitrary-rank to test some expressions

Type inference of arbitrary rank types and System F translation

• Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields. (2005). Practical type inference for arbitrary-rank types. Type inference algorithm for arbitrary-rank types

Type stack exec systemF to enter the interactive shell. If you input an semi-typed expression, then it is translated to System F-like term. For example:

$ stack exec systemF
>> \f -> let x = () in f x
/\a. \f : () -> a. let x : () = () in f x
>> \f -> f () :: (∀a. a -> a) -> ()
\f : ∀a. a -> a. (f [()]) ()