Recursive Types Are not Conservative over F

12 years 9 days ago
Recursive Types Are not Conservative over F
d abstract) Giorgio Ghelli1 F≤ is a type system used to study the integration of inclusion and parametric polymorphism. F≤ does not include a notion of recursive types, but extensions of F≤ with recursive types are widely used as a basis for foundational studies about the type systems of functional and object-oriented languages. In this paper we show that adding recursive types results in a non conservative extension of the system. This means that the algorithm for F≤ subtyping (the kernel of the algorithm for F≤ typing) is no longer complete for the extended system, even when it is applied only to judgements where no recursive type appears, and that most of the proofs of known properties of F≤ do not hold for the extended system; this is the case, for example, for Pierce’s proof of undecidability of F≤. However, we prove that this non conservativity is limited to a very special class of subtyping judgements, the “diverging judgements” introduced in [Ghe]. This last...
Giorgio Ghelli
Added 10 Aug 2010
Updated 10 Aug 2010
Type Conference
Year 1993
Where TLCA
Authors Giorgio Ghelli
Comments (0)