Parametric subtyping for structural parametric polymorphism

Recursive types, generics (sometimes called parametric polymorphism), and subtyping are all essential features for modern programming languages across numerous paradigms. Whereas recursive types describe unbounded data structures, generics are used to define parametrized data structures by abstracting from the concrete types on which they operate. Subtyping provides flexibility by enabling a more specific data type to be treated as its more general supertype, promoting code reuse. Structural subtyping is especially flexible and expressive.

The combination of these features is present to varying degrees in many of today’s widely used languages, such as Scala, Go, Rust, TypeScript, and Java, but this combination is difficult to manage. In particular, structural subtyping is undecidable in the presence of recursive types and generics. To overcome this difficulty, various restrictions on types’ structure have been proposed. We contend that these restrictions can be too limiting or unintuitive in practice.

In our POPL 2024 paper and its accompanying implementation, we propose a reconstruction of the interaction between recursive types, generics, and structural subtyping from first principles. We present a notion of parametricity for type constructors that forms the basis of a suitable, decidable fragment of structural subtyping, which we call parametric subtyping.

Parametric subtyping establishes that a pair of type constructors t[α₁,…,α_n] and u[β₁,…,β_m] is considered parametric if the subtyping problem t[α₁,…,α_n] ⩽ u[β₁,…,β_m] can be reduced to (finitely many) subtyping problems among the arguments α₁,…,α_n and β₁,…,β_m alone.  In this sense, parametric subtyping constitutes a clear and simple declarative characterization of subtyping where:
Parametric subtyping thus adapts Reynolds’s characterization of parametric functions as those that map related arguments to related results, modifying it for parametric type constructors.

(For a comparison of parametric subtyping with the forms of subtyping available in Java and Scala, please see the end of this post.)

To delve into parametric subtyping, consider an interface for stack objects, parameterized by a type α of stack elements.  A stack is an object that offers push and pop methods, where the pop method accounts for the possibility that the stack may be empty by using the auxiliary constructor maybe[κ].

Programmers sometimes want to ensure that a stack can be used according to a particular protocol, and subtyping plays a crucial role in ensuring that stacks are compatible regardless of the particular protocol they follow. For example, when implementing a queue with a pair of stacks, the stacks should adhere to the protocol that all pushes occur before all pops. This protocol can be described by the pushes[β] and pops[γ] type constructors. Whenever the first pop from a stack of type pushes[β] occurs, the remaining stack has type pushes[β], which does not offer a push method.

Under the standard structural subtyping rules, there exists an infinite derivation of stack[α] ⩽ pushes[β] whenever α and β are mutual subtypes. This gives rise to an admissible subtyping rule:
This rule is admissible in the sense that the corresponding infinite derivation of stack[α] ⩽ pushes[β] can always be inlined in its place. More importantly, this is a valid parametric subtyping rule because the premises involve only arguments, α and β.

Similarly, there exists an infinite derivation of stack[α] ⩽ pops[γ] whenever α ⩽ γ, which gives rise to an admissible subtyping rule:

As an example of a subtyping rule that is not parametric, consider a type natstack and the rule “nat ⩽ γ implies natstack ⩽ pops[γ]”:
This rule is not parametric because it relates a type argument, γ, to another, non-argument type, nat.

Before we delve into any more specifics of parametric subtyping, let’s revisit structural subtyping using a simpler, familiar example: even and odd natural numbers. This example operates within the realm of monomorphic types (i.e., types without type parameters), where structural subtyping is decidable. We now sketch a saturation-based decision procedure for structural subtyping of monomorphic types that will serve as a stepping stone for understanding how the decision procedure for parametric subtyping works in the polymorphic setting.

Consider a type nat of natural numbers. Natural numbers can be built in two ways: either as zero or as the successor of another natural number. Similarly, an even number is either zero or the successor of an odd number, whereas an odd number is always the successor of an even number.

To prove that the types even and odd are subtypes of nat, we will use saturating forward inference. Intuitively, we will assume that even ⩽ nat and try to find a contradiction by inferring more and more consequences of this assumption. Once we have saturated by inferring all the facts we can, if we still have not uncovered a contradiction, then we will know that the type even is indeed a subtype of nat.

For this purpose, we keep a database with the assumed subtyping relations and proceed by forward inference. More specifically, we start by assuming that even ⩽ nat, expand according to definitions, invert structural subtyping rules, and conclude that the subtyping odd ⩽ nat should be further analyzed.

Now we can consider odd ⩽ nat, once more expanding according to definitions and inverting structural subtyping rules. We conclude that odd ⩽ nat holds only if even ⩽ nat holds. However, this new instance of even ⩽ nat is subsumed by the one that already exists in the database:

At this point, we have reached saturation — no new facts can be inferred from even ⩽ nat and odd ⩽ nat. Because we still haven’t uncovered a contradiction, we may conclude that the types even and odd are indeed subtypes of nat. Saturation is guaranteed because a given program uses finitely many type names.

Unfortunately, we can’t just use the previous algorithm to decide structural subtyping once we have generics (i.e., recursive parameterized type constructors). Saturation is not guaranteed because, with type constructors and type nesting, infinitely many pairs of types can be formed. For example, we might infer t[nat] ⩽ u[nat] and later infer t[t[nat]] ⩽ u[u[nat]] and so on.

In our POPL 2024 paper, we prove that structural subtyping is undecidable for recursive type constructors. To mitigate this, we propose parametric subtyping, a fragment of structural subtyping in which the accepted subtypings are exactly those that hold parametrically, i.e., those that map related type arguments to related type results. We provide a relatively simple declarative characterization of parametric subtyping and present an effective decision procedure for it.

Saturation-Based Decision Procedure

Leveraging the structure of the forward-inference algorithm for deciding structural subtyping of monomorphic types, we now present a related algorithm for deciding parametric subtyping of polymorphic types.

The decision procedure consists of two phases: the first phase uses saturating forward inference to derive the most general admissible parametric rules for each pair of defined type constructors; the second phase uses these rules and backward proof construction to build a finite derivation to decide a parametric subtyping problem.

As an example, let’s verify that stack[maybe[even]] ⩽ pops[maybe[nat]] is valid under parametric subtyping.

First Phase: Forward Inference

The parametricity of parametric subtyping means that we first look at the more general stack[α] ⩽ pops[γ]. We will assume that it holds and use saturating forward inference to discover the set of constraints on α and γ that must be satisfied for stack[α] ⩽ pops[γ] to hold. As for the monomorphic case, we expand according to definitions and invert structural subtyping rules, identifying a new pair of type constructors to add to the database: namely, maybe[κ] ⩽ maybe[κ’].

At this point, we leave the last subtyping on hold and proceed with the saturation procedure to determine the set of constraints on κ and κ’ that must be satisfied for maybe[κ] ⩽ maybe[κ’] to hold:

Updating the assumed subtypings with the constraint κ ⩽ κ’ that must be satisfied for maybe[κ] ⩽ maybe[κ’] to hold, we can now return to the postponed judgment, instantiating the constraints for the maybe constructor. Thus, it must be that α ⨉ stack[α] ⩽ γ ⨉ pops[γ]. From this, we infer the constraint α ⩽ γ, update the assumed subtyping, and reach saturation.

Because we have reached saturation, the necessary consequences described by the assumed subtypings are, in fact, sufficient and we arrive at the admissible rules:

Second Phase: Backward Construction

Using the admissible subtyping rules inferred in the first phase, and also the admissible subtyping rule for the types even and nat, we can now proceed by backward construction to build a derivation for stack[maybe[even]] ⩽ pops[maybe[nat]]:

Three possible outcomes: parametric subtype, not a structural subtype, or not a parametric subtype

All in all, our saturation-based procedure for deciding the parametric subtyping problem A ⩽ B yields one of three possible outcomes:

Although our implementation currently does not distinguish between the two categories of contradiction, we could easily incorporate this distinction.

For proofs and further details of parametric subtyping’s declarative characterization, decision procedure, and other technical aspects, as well as additional examples and a brief discussion of the implementation, we refer the interested reader to our POPL 2024 paper.  For our implementation of the decision procedure described in the paper, please see our online repository.

Java and Scala take a primarily nominal approach to subtyping. Generally, the programmer must anticipate and declare upfront any subtyping relationships that may be needed in the future, at the time that the subclass is defined (by using the extends keyword). In contrast, the above system of parametric subtyping is structural, allowing types to be defined independently and be used as subtypes whenever the compiler can verify the subtyping relationship, which is arguably more flexible.

(Scala does include duck typing, as a limited form of structural subtyping, but this duck typing does not support recursive types and requires the result to be an anonymous trait, making it significantly less expressive than our parametric subtyping. Furthermore, Scala’s duck typing is only fully verified at runtime.)

The limitations of subtyping with generics in Java are well-known and can be quite restrictive, regardless of the variance. To mitigate these limitations, Scala permits the programmer to annotate type parameters with variances. In contrast, parametric subtyping naturally infers these variances for free as part of the subtyping algorithm.

On the other hand, Scala’s subtyping includes several features that the above system of parametric subtyping does not. Scala permits non-parametric subtypings (nominally), such as NatStack extends Stack[Nat]; not covering non-parametric subtypings is the price that our system pays for its expressive, decidable structural subtyping. Scala also supports intersection and union types and type bounds, which are not part of the above notion of parametric subtyping, but which we hope to explore in future work.

About the authors: Henry DeYoung is an adjunct professor in the Computer Science Department at Carnegie Mellon University. His research interests center around programming languages and type systems for concurrent programs, with an emphasis on logic-based approaches. Andreia Mordido is an assistant professor in the Department of Informatics of the Faculty of Sciences, University of Lisbon, and an integrated researcher at LASIGE. Her research focuses on programming languages and type systems for the specification and verification of communication protocols and programs. Frank Pfenning is a professor in the Computer Science Department at Carnegie Mellon University. His research interests include programming languages, substructural logics, type theory, logical frameworks, and concurrency. Ankush Das is an assistant professor in the Computer Science Department at Boston University (formerly at Amazon). His research interests are in the intersection of programming languages with cryptographic protocols, distributed systems, and probabilistic and machine learning models.

Disclaimer: These posts are written by individual contributors to share their thoughts on the SIGPLAN blog for the benefit of the community. Any views or opinions represented in this blog are personal, belong solely to the blog author and do not represent those of ACM SIGPLAN or its parent organization, ACM.