Fomega Home Page

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.

Example code

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.

Download

Fomega 0.10 alpha is available as source distribution and has been tested on a X86-Linux platform. It requires OCaml 3.06. Download: Have fun!

Date Version Download Instructions
01.09.2003 0.10 alpha fomega-0.10.tar.gz fomega-0.10-INSTALL

Related Projects

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