Scrap your type applications

Mathematics of Program Construction (MPC'08) |

System F is ubiquitous in logic, theorem proving, language meta-theory, compiler intermediate languages, and elsewhere. Along with its type abstractions come type applications, but these often appear redundant. This redundancy is both distracting and costly for type-directed compilers.

We introduce System IF{}, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. Experiments with Haskell suggest that it could be used to reduce the amount of intermediate code in compilers that employ System F.

System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is both useful in practice and interesting in its own right.