First-Class Subtypes

TL;DR

This paper explores how to encode first-class subtypes in OCaml using existing features and modular implicits, demonstrating their equivalence and practical utility through various examples.

Contribution

It introduces multiple encodings of first-class subtypes in OCaml, showing their interconvertibility and practical applications, advancing type relation representations in functional languages.

Findings

Multiple encodings of first-class subtypes are interconvertible.

Encodings are practical and useful in real OCaml programs.

Modular implicits facilitate more convenient subtype representations.

Abstract

First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in most functional programming languages. We present several encodings of first-class subtypes using existing features of the OCaml language (made more convenient by the proposed modular implicits extension), show that any such encodings are interconvertible, and illustrate the utility of the encodings with several examples.

Equations

$$\forall \varphi .\varphi (T)\to \varphi (S)$$

Full text

We present several encodings of first-class subtypes using existing features of the OCaml language (made more convenient by the proposed modular implicits extension), show that any such encodings are interconvertible, and illustrate the utility of the encodings with several examples.

1 Introduction

One appealing feature of ML-family languages is the ability to define fundamental data structures — pairs, lists, streams, and so on — in user code. For example, although lazy computations are supported as a built-in construct in OCaml, it is also possible to implement them as a library.

Laziness in variants

The following data type can serve as a basis for lazy computations111 The code in this paper uses the proposed modular implicits extension to OCaml [21]. The modular implicits compiler can be installed as the opam switch 4.02.0+modular-implicits. :

[TABLE]

The constructors of a lazy_cell value represent the three possible states of a lazy computation: it may be an unevaluated thunk, a fully-evaluated value, or a computation whose evaluation terminated with an exception. Since the state of a lazy computation may change over time, lazy values are represented as mutable references that hold lazy_cell values:

[TABLE]

Finally, there are two operations: delay creates a thunk from a function, while force either forces a thunk and caches the result, or returns the value or exception cached by a previous call.

[TABLE]

Laziness invariants

The characterising feature of lazy computations is that each computation is run only once, although the result may be read many times. The delay and force functions enforce this property. For simplicity, we assume that lazy computations do not invoke themselves recursively. (More sophisticated implementations of laziness generally include a fourth state In_progress to guard against this occurrence).

Concealing the representation type of lzy behind a module interface ensures that other parts of the program cannot violate this invariant:

[TABLE]

Laziness invariance

This simple implementation has the same behaviour as the built-in lazy type. However, there is one notable difference: unlike the built-in type, our Lzy.t is not covariant.

Covariant types are parameterised types that preserve the subtyping relationships between parameters. For example, if u is a subtype of v then, because option is covariant, u option is a subtype of v option. In OCaml, types may be marked as covariant by adding a + before a type parameter. For example, here is a definition of the covariant type option:

[TABLE]

Not every type can be marked as covariant in this way. For example, it would not be safe to allow ref, the type of mutable cells, to behave covariantly. If ref were covariant then a program could coerce a value of type u ref to v ref, and then store a value of another subtype of v, unrelated to u, in the cell. OCaml therefore prohibits covariance for type parameters that appear under ref, as in the definition of lzy.

The lack of covariance in our Lzy.t has two significant consequences for programmers. First, computations constructed using the built-in type can be coerced, while computations constructed using our Lzy.t cannot. Here is a coercion that eliminates a method m from the type of a built-in lazy computation:

[TABLE]

An attempt to similarly coerce our Lzy.t fails:

[TABLE]

Second, let-bound computations constructed using the built-in lazy receive polymorphic types, following the relaxed value restriction, which generalizes type variables that appear only in covariant positions [13]:

[TABLE]

In contrast, types built using our Lzy.t are ungeneralized, as the leading underscore on the type variable ’_a indicates:222See https://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html

[TABLE]

The interface to Lzy.t only exposes read operations, and so it would be safe for the type to be treated as covariant in its parameter. However, the assignment of variance considers only the use of the parameter in the definition of Lzy.t, not the broader module interface. Since the type parameter is passed to the the invariant type ref of mutable cells, the type Lzy.t is also considered invariant.

These shortcomings in the Lzy interface can be overcome with more flexible treatment of subtyping and variance\cprotect333An alternative solution is to switch to a higher-order representation of lazy computations:

. In particular, making subtypes first-class makes it possible to tie together the type definition and the functions exposed in the interface in the consideration of variance assignment, and so make Lzy.t covariant.

Variants of first-class subtypes may be found in advanced type systems in the research literature, such as Cretin and Rémy’s F${}_{\_}\iota$ [10]. Our contribution here is to show that first-class subtypes can be encoded using the features of an existing real-world functional programming language.

First-class subtypes can be defined using a binary type constructor:

[TABLE]

that has a single constructor:

[TABLE]

and an operation that turns a sub value into a function:

[TABLE]

These three elements, considered in more detail in Section 2 are sufficient to define a covariant variant of Lzy. Section 2 adds an additional constuctor, lift that, together with the three elements above, suffices as a basis to define a range of useful subtyping operations.

Here is a second, covariant interface to lazy computations:

⬇

module CovLzy :

sig

type +’a t

val delay : (unit $\to$ ’a) $\to$ ’a t

val force : ’a t $\to$ ’a

end

The implementation of CovLzy can be constructed from the combination of Lzy and first-class subtypes. Here is the definition of CovLzy.t

[TABLE]

That is, a value of type ’a CovLzy.t is a pair of a lazy computation of type ’a Lzy.t and a value of type (’a, ’b) sub that supports coercions from ’a to ’b.

Now CovLzy.delay builds on Lzy.delay, pairing a lazy computation with a sub value444A reviewer observes that the permission-oriented language Mezzo [5] uses a related approach. In Mezzo, a witness that s is a subtype of t can be encoded as a permission of the form id @ a $\to$ b, which can be read as “the identity function has type a $\to$ b”, and these witnesses are also used in Mezzo to make the lazy type covariant: http://protz.github.io/mezzo/codesamples/lazy.mz.html.:

[TABLE]

Finally, the definition of CovLzy.force calls Lzy.force and applies a coercion to the value returned:

[TABLE]

These additions to make CovLzy covariant bring its behaviour closer to the behaviour of the built-in lazy. For example, let-bound values built by CovLzy.delay receive polymorphic types:

[TABLE]

2 First-class subtypes defined

2.1 Subtypes à la Liskov & Wing

The first ingredient in a representation of subtyping proofs is a definition of subtyping. Here is Liskov and Wing’s characterisation [16]:

Let $\phi(x)$ be a property provable about objects $x$ of type $T$. Then $\phi(y)$ should be true for objects $y$ of type $S$ where $S$ is a subtype of $T$.

For instance, properties of a record type $r$ should also hold for a widening of $r$, since the extra fields can be ignored. And dually, properties of a variant type $v$ should also hold for a narrowing of $v$: any property that holds for all constructors also holds for a subset of constructors.

2.2 Subtypes à la Curry & Howard

The Curry-Howard correspondence turns Liskov and Wing’s characterisation of subtyping into an executable program.

With a propositions-as-types perspective [19], a property provable about objects of type $T$ is represented as a type $\phi(T)$ involving $T$, and a proof of that property is a term of that type 555At least, in total languages. In OCaml the waters are muddied by side-effects and nontermination.. Liskov and Wing’s proposition that $S$ is a subtype of $T$ corresponds to the following (poly)type:

[TABLE]

Two points deserve note.

First, although Liskov and Wing’s characterisation is couched in terms of objects $x$ and $y$, it is really about their types $T$ and $S$. To see this, consider that, in the characterisation, it is sufficient to know $y$’s type to know that $\Phi(y)$ holds. Since the characterisation only involves properties about all the objects of a type, not properties of individual objects, there is no need for dependent types in the type corresponding to the subtyping proposition.

Second, a “property about objects” is a context that consumes an object. For example, consider the property “for every object of type $T$ there is an object of type $R$”, which can reasonably be described as a property about objects of type $T$, but not as a property about objects of type $R$. In a propositions-as-types setting, a proof of this property is a context that consumes an object of type $T$ and produces an object of type $R$. Since the properties of interest are consumers of objects, $\phi$ ranges over negative contexts.

2.3 Contexts and variance

Figure 1 defines OCaml signatures, POS and NEG, of positive and negative type contexts. The - preceding the type parameter ’a indicates that ’a can only appear in negative (contravariant) positions in instantiations of the signature. The Id module and Compose functors represent the identity context and the composition of two contexts. Each composition of variance in the argument contexts requires a separate Compose (but see §4 for a generalization).

2.4 Encoding subtypes

Figure 2 defines an interface to subtype witnesses. A value of type (s, t) sub serves as evidence that s is a subtype of t. There are two ways to construct such evidence. First, refl represents the fact that every type is a subtype of itself. Second, lift represents the fact that subtyping lifts through covariant contexts, which are passed as implicit arguments [21]. (Lifts through contravariant contexts are defined below in terms of the minimal interface.) The single destructor, >:, which mimics OCaml’s built-in coercion operator :>, supports converting a value of type s to a supertype t.

This small interface suffices as a basis for many useful subtyping-related functions. For example, the transitivity of subtyping is represented by a function of the following type:

[TABLE]

and may be defined as follows:

[TABLE]

Here the application lift M y builds a value of type (b M.t, c M.t) sub — that is to say, a value of type ((a, b) sub, (a, c) sub) sub — which is used to coerce x from type (a, b) sub to type (a, c) sub.

Similarly, a function that lifts subtyping witnesses through negative contexts

[TABLE]

may also be defined by supplying a suitable implementation of POS to lift:

[TABLE]

Using the variance of sub, refl can be used to define a witness for any subtyping fact that holds in the typing environment. For example, in OCaml the object type < m:int >, with one method m, is a subtype of the type < > of objects with no methods. This fact can be turned into a sub value by coercing refl, either by lowering the contravariant parameter:

[TABLE]

or by raising the covariant parameter:

[TABLE]

The resulting value can be passed freely through abstraction boundaries that conceal the types involved, eventually being used to coerce a value of type <m:int> to its supertype < >.

The generality of the interface in Figure 2 places constraints on the implementation. Most notably, since lift can transport subtyping evidence through any positive context, coercion must pass values through unexamined. For example, lift might be used to build a value of type (s list, t list) sub from a value of type (s, t) sub:

[TABLE]

but applying l cannot involve list traversal, since the subtyping interface says nothing about list structure. A polymorphic interface thus ensures an efficient implementation.

3 Implementations of subtyping

3.1 First-class subtypes via contexts

Figure 3 gives an implementation of Figure 2 based on negative contexts that directly follows Liskov & Wing’s definition666 Edward Kmett has used this approach in the magpie library [15], as we discovered after writing this note. . A value of type (s, t) sub is a proof that t can be replaced with s in any negative context; operationally it must be the identity, as discussed above, and so the two constructors lift and refl both correspond to the identity function. Figure 4 gives a similar but simpler implementation, based on positive contexts. Apart from the variance annotations, these definitions mirror the standard Leibniz encoding of type equality [22].

3.2 First-class subtypes as an inductive type

Consider an ordinary inductive type, say the Peano natural numbers:

[TABLE]

We can write its constructors in the form of a module signature as follows:

[TABLE]

What it means for the type nat to be inductive is that it is an initial algebra for this signature: first, it implements the signature by providing Zero and Suc, and secondly, for any other implementation M, we have a function mapping nat to M.t that maps Zero to M.zero and Suc to M.suc:

[TABLE]

In defining the type nat, we made use of OCaml’s built-in support for inductive types. Lacking this, we could have used the initial algebra definition directly, and defined the type nat as follows:

[TABLE]

This corresponds to the Church encoding of the natural numbers [9], in which a natural number is anything that can produce a M.t from M.zero : M.t and M.suc : M.t $\to$ M.t. Here and elsewhere we’re using the modular implicits extension to OCaml [21] — not for implicit instantiation of arguments, but because modular implicits support higher-kinded quantification with propagation of variance information. Other approaches to higher-kinded polymorphism could perhaps be used instead [23].

This approach to inductive types also makes sense for GADTs, such as the equality GADT defined below [4, 8, 20]:

[TABLE]

This uses OCaml’s GADT syntax, but we can do without it by building a Church encoding of equality [3], using the same technique as before:

[TABLE]

We can use this encoding to implement the standard operations on the equality GADT by providing a suitable implementation of the EQ interface. For instance, we can implement the coercion function

[TABLE]

by supplying an implementation of EQ using function types:

[TABLE]

If we modify the signature EQ by adding co- and contra-variance markers to the parameters of the type t, then we get the Church encoding of first-class subtypes, as shown in Figure 5, from which we can implement the refl, lift and (:>) functions.

3.3 Converting between encodings

Despite the different starting points, the three implementations are interdefinable. In fact, given any two implementations A and B of the subtyping interface, a subtyping witness of type (’a,’b) A.t can be converted to a witness of type (’a,’b) B.t.

The SUB module type contains the four elements of Figure 2 (t, refl, lift, >:):

[TABLE]

The function conv takes two implementations of SUB, A and B, and converts a value in A.t to a value of B.t:

[TABLE]

As often, implementing conv is a matter of finding a suitable implementation of POS to pass to lift:

[TABLE]

The function conv works as follows. The value x is a proof that a $\leq_{A}$ b — that is, that a is an A-subtype of b. The type M.t represents the positive context a $\leq_{B}$ -. The call to lift then lifts the proof a $\leq_{A}$ b through the context M.t to produce a proof (a $\leq_{B}$ a) $\leq_{A}$ (a $\leq_{B}$ b). Finally, this proof can be used to coerce a proof of the reflexivity of B-subtyping (at type a) a $\leq_{B}$ a to a proof that a $\leq_{B}$ b. That is, from a proof a $\leq_{A}$ b, the operations of A.sub and B.sub produce a proof a $\leq_{B}$ b.

4 First-class subtypes: further examples

4.1 Arrays and rows

Here is a function that prints arrays by calling the name method of each element:

[TABLE]

To call name, print_array does not need to know the full element type: it needs only to know that there is a method name returning string. OCaml gives print_array a row type, indicating that the element type may have other methods:

[TABLE]

But rows are sometimes too inflexible. Given two arrays a, b, of different element types

[TABLE]

unification will fail:

[TABLE]

Using first-class subtypes it is possible to combine iterations over arrays whose element types belong to the same subtyping hierarchy.

[TABLE]

4.2 Selective abstraction

A third class of examples arises from selective abstraction, where an abstract type comes with a proof of a property about that type. For example, here is a module that exports a type t along with a proof that t is a subtype of int:

[TABLE]

Outside the module, values of type t can be coerced to int, but not vice versa. This approach supports a style similar to refinement types, in which abstraction boundaries distinguish values of a type for which some additional predicate has been shown to hold.

These are known as partially abstract types [7], and are available as a language feature in OCaml [14] and Moby [12]. However, implementing these via first-class subtypes allows more flexibility: for example, they allow some of the methods of an object type to be hidden from the exposed interface, and also support the dual of private types (called invisible types [17]), and zero cost-coercions [6], where coercions in both directions are available, but actual type equality is not exposed.

4.3 Bounded quantification

Dual to abstraction, combining first-class subtypes with OCaml’s first-class polymorphism encodes bounded quantification. For example, the type $\forall\alpha\leq t.\;\alpha\to t$ might be written as follows:

[TABLE]

4.4 Proofs of variance

Finally, first-class subtypes can express proofs of variance. For example, the covariance of list can be represented by a value of the following type:

[TABLE]

4.5 Unsoundness in Java

Amin and Tate [2] present an encoding of first-class subtypes in Java, which they use to demonstrate a soundness bug. They use Java’s bounded quantification to define a type Constrain<A, B> which is well-formed only when A $\leq$ B. Then, the type $\exists\texttt{X}\geq\texttt{T}.\;\texttt{Constrain<}\texttt{U},\texttt{X}\texttt{>}$ corresponds to a subtyping witness (U,T) sub: if this type is inhabited, then some $\texttt{X}\geq\texttt{T}$ exists making Constrain<U, X> well-formed, giving U $\leq$ X $\leq$ T. Unfortunately, in Java (unlike OCaml), the value null inhabits every reference type, giving an invalid subtyping witness that allows any type to be coerced to any other.

5 Discussion

The encodings given here are useful for exploratory work, for demonstrating soundness, and for showcasing OCaml’s expressivity. However, direct language support would make first-class subtypes more usable. Scherer and Rémy [17] discuss design issues and related work (e.g. [11, 18]).

The encodings suffer from some awkwardness, since contexts must be applied explicitly, unlike the equalities revealed by pattern matching with gadts, which the type checker applies implicitly.

Our encodings share another issue with similar encodings of GADTs [22]: they lack inversion principles. Given (’a, ’b) sub, our encodings can be used to derive (’a list, ’b list) sub, from the covariance of the list type constructor. However, going the other direction, from (’a list, ’b list) sub to (’a, ’b) sub, is equally valid but not expressible with our encodings.

With language support for subtype witnesses, coercions would still be explicit, but constraints in scope could be implicitly lifted through contexts, and inversion principles could be applied.

Acknowledgements

We thank François Pottier, Leo White, the ML 2017 reviewers, and the ML & OCaml 2017 post-proceedings reviewers for helpful comments.