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.
