Type-checking is easy for fully type-annotated (Church-style) terms of Girard's System Fω but undecidable for non-annotated (Curry-style) terms. Hence, the type checker we implemented is necessary incomplete. Nevertheless, it succeeds on most typical terms occurring in Fω programs and has proven to be a practical tool for my own purposes.
If you are wondering why we need Fω when we have ML, you can find a simple λ-term which breaks Hindley-Milner type inference here.
The first example shows how to encode cartesian products impredicatively in Fomega.
type prod : * -> * -> * = \A\B forall X. (A -> B -> X) -> X ; term pair : forall A forall B. A -> B -> prod A B = \a\b\f. f a b ; term fst : forall A forall B. prod A B -> A = \p. p (\a\b a) ; term snd : forall A forall B. prod A B -> B = \p. p (\a\b b) ;
The second example defines pointwise implication for type constructors of kind (* -> *) -> * -> *.
type sub2 : ((*->*) -> * -> *) -> ((*->*) -> * -> *) -> * = \F\F' forall X:*->* forall A. F X A -> F' X A;
More examples can be found in the distribution.
Last modified: Thu Feb 5 23:00:42 CET 2004