Intensional Analysis of Higher-Kinded Recursive Types

Last modified: Fri Oct 25 23:19:57 2002 GMT.

Authors

Abstract

Recursive types are ubiquitous in modern programming languages, as they occur when typing constructs such as datatype definitions. Any type-theoretic framework must effectively deal with recursive types if it purports to be applicable to real languages such as ML and Haskell. Intensional Type Analysis and Certified Binaries are two such type-theoretic frameworks. Previous work in these areas, however, has not adequately supported recursive types. In this paper we present a new formulation of recursive types which subsumes the traditional one. We show that intensional analysis over these types (including higher-kinded recursive types) can be supported via inductive elimination. Our solution is simple, general, and extensible; the typing rules for higher-kinded recursive types are concise and very easy to understand.

PDF (technical report YALEU/DCS/TR-1240) [357k]

colophon