Authors
Gregory D. Collins
Zhong Shao
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.