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...

• Type: Conference
• Year: 1993
• Where: TLCA
• Authors: Giorgio Ghelli
• Keywords: Giorgio Ghelli1 F≤, Recursive Types, Theoretical Computer Science, TLCA 1993, Type Systems