church Home Page

church is a simple type-checker for Girard's System Fω in Church-style, i.e., each variable must be annotated with it's type. This requirement makes the type of an expression trivially inferable. The file syntax of church additionally requires the types of expressions to be given; these provided types are compared to the infered types of expressions using Coquand's conversion algorithm (Coquand, An Algorithm for Testing Conversion in Type Theory, 1991).

Implementation

The church type checker was implemented by Jan Peter Gutzmann as a student's project which was supervised by Andreas Abel and Klaus Aehlig. It is written in Haskell 98 and has been tested under Hugs (November 2002 edition) and GHC 5.04. The parser has been generated using Happy 1.13.

Download...

Example: Terms 22...2K

Urzyczyn (MSCS 1997) describes pure lambda-terms 22...2K (where 2 = λfλx.f(fx) and K = λaλb.a) which are not typable in simply-typed lambda-calculus or System F, but make essential use of the typing power of the higher-order polymorphic lambda-calculus System Fω. The normal forms have length superexponentially in the number of 2's: 2, 4, 16, 65536, 265536, ...

A possible typing of these terms can be found in towersOfTwo.church. In our implementation, which makes use of type normalization, only the first three terms 2K, 22K, and 222K can be type-checked, the next term 2222K already causes a stack overflow during normalization of the types for equality checking.


Valid HTML 4.01! Andreas Abel, http://www.tcs.informatik.uni-muenchen.de/~abel/church/
Last modified: Tue Dec 23 16:04:53 CET 2003
Valid CSS!