type system list

I has investigate the relation between varias type system for a long time, and finally find the lambda cube is a good way to explain all these mess.

1. untyped lamda calculus
2. simply typed typed calculus: extend untyped one with type, to avoid the paradox that a set refer to itself
   

according to lambda cube, there is a cube with simply typed typed calculus as the origin, and can be extended on three axim.

• Terms depending on types, or polymorphism (as in System F),
• Types depending on types, or type operators, and
• Types depending on terms, or dependent types (as in LF).

Hindley-Milner: it is restricted version of system F, this is the last one that has type inference. even system F dont has this ability. traditional ML such as haskell 98 and ocaml all based on this.

System F: ploy extendtion of simply typed typed calculus. As a whole it dont has type infenrece. GHC based on this.

There is a hierarchical familay of system F, where
F1 is just the simply typed typed calculus.
and any Fn is actually map from lowwer level to type. and Fw is the union of Fn.