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.

Date | Version | Download | Instructions |
---|---|---|---|

01.09.2003 | 0.10 alpha | fomega-0.10.tar.gz | fomega-0.10-INSTALL |

- B. Pierce's
`fomega`: Church-style type checker (no longer supported) - C. Raffalli's type checkers for System F
^{η}

Andreas Abel,
http://www.tcs.informatik.uni-muenchen.de/~abel/fomega/
Last modified: Thu Feb 5 23:00:42 CET 2004 |