Home

On Decidability of Nominal Subtyping with Variance

On Decidability of Nominal Subtyping with Variance. Andrew J. Kennedy, Benjamin C. Pierce. FOOL'07. January 2007

We investigate the algorithmics of subtyping in the presence of nominal inheritance and variance for generic types, as found in Java 5, Scala 2.0, and the .NET 2.0 Intermediate Language. We prove that the general problem is undecidable and characterize three different decidable fragments. From the latter, we conjecture that undecidability critically depends on the combination of three features that are not found together in any of these languages: contravariant type constructors, class hierarchies in which the set of types reachable from a given type by inheritance and decomposition is not always finite, and class hierarchies in which a type may have multiple supertypes with the same head constructor. These results settle one case of practical interest: subtyping between ground types in the .NET intermediate language is decidable; we conjecture that our proof can also be extended to show full decidability of subtyping in .NET. For Java and Scala, the decidability questions remain open; however, the proofs of our preliminary results introduce a number of novel techniques that we hope may be useful in further attacks on these questions.

The undecidability of subtyping is proved by reduction from the Post Correspondence Problem. Section 5 presents several decidable fragments.

Hot stuff!

By Ehud Lamm at 2007-02-02 11:28 | Type Theory | other blogs | 5910 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

moving forward

I share Ehud's enthusiasm, because this paper deepens our understanding of generic types quite a bit. Although it was known to the Scala team for quite some time that variance typing brings troubles, seeing the formal proof and the restrictions on decidability is a good step forward.

I wonder if in functional programming, there are any similar discussions? Subtyping papers seems to restrict themselves to structural subytping (for arrow and *maybe* pair constructor), with nonstructural typing being only dealt with through top and bottom. The usage of variance (or polarity, if you like) in this result seems to hint at the fact that such a concept of nonstructural subtyping misses out on an important point.

Does nonstructural subtyping have an application in functional programming? module systems?

I think a paper with an object encoding into some "F-omega sub with polarized kinds" that preserves subtyping of variant generic types would probably help to get those connections right...

By Burak Emir at Thu, 2007-02-08 08:37 | login or register to post comments