Writing about subtyping

I want programmers to stop using subtyping, yet I keep bringing it up, in article after article. Partly that is because it is very hard to avoid subtyping-related issues in Scala, and I find myself concerned with Scala when I ought to be devoting mental cycles to simpler, more powerful languages. But that may simply feed into what I suppose is the greater reason:

Subtyping is an amusing puzzle for my mind. I enjoy the mental diversion of the needlessly complex puzzle of practical programming techniques making use of subtyping.

I can justify this self-gratification by saying to myself, “the more they read about what subtyping really means, the more their desire to avoid this mess will grow”. I think this is more rationalization than honest motivation for myself, though I do think those who learn more about subtyping are more likely to avoid it, just as those who learn more about typing are more likely to advocate it.

Yet, it does have a kind of beauty. So I take it out here and there, and appreciate its facets for a while. Then I carefully return it to its display case, lest I am afflicted with the subtyping bug again.

Advanced type system features are [usually] a good thing

The desire to allow more programs to be typed—by assigning more accurate types to their parts—is the main force driving research in the field. – Benjamin Pierce, Types and Programming Languages

Type system design is a major factor in whether you can write programs, and how easily you can do so. Simplicity is an important consideration, but that entails a trickier question to start: “what is simplicity?”

In this article, I want to consider two questions about type system simplicity by comparing two—relatively good as these things go—type systems, Haskell’s and TypeScript’s.

First: what dangers come from an excess of pragmatism in type system design? By pragmatism, I mean the elevation of design compromise as the highest virtue. The pragmatist seeks to compromise even those “pure” designs that are entirely suitable when considering the practical constraints in play.

I don’t use this word, ‘pragmatist’, because I think it’s nice and accurate. Nor do I think that it’s fair to those who don’t fit the definition I’ve just given, yet still think of themselves as “pragmatic” in the broader sense. I use this word because the people I describe have claimed the mantle of “pragmatism”, and reserved it for themselves, quite successfully in the world of programming. And first, we must name the enemy.

Second: what is so compelling about advanced type system features? New type systems are often beset with users requesting features like rank-N types, higher-kinded types, GADTs, existential quantification, &c. There are good, practical reasons these features are requested; they result in a kind of “simplicity” that cannot be had simply by having a small number of features.

An unsound feature in TypeScript

Function parameters are a contravariant position; contravariance and invariance are the only sound choices for them. So TypeScript’s “function parameter bivariance” is a deliberately unsound choice; if you’re unfamiliar with it, I strongly recommend stopping now and reading the linked documentation, along with the explanation of why they do it; it’s a good piece of documentation, describing an eminently practical circumstance in which it might be used.

However, this example is worth examining more closely. Think about it from the perspective of a type system designer: how would you support the call to addCallback below?

enum EventFlag {
  MousePress,
  KeyPress
}

interface Event;
interface MouseEvent extends Event {/*...*/}
interface KeyEvent extends Event {/*...*/}

function addCallback(
  flag: EventFlag,
  callback: (Event) => void): void {
  // ...
}

addCallback(EventFlag.MousePress, (e: MouseEvent) =>
  { } // handle e
);

The temptation of pragmatism

TypeScript’s design choice to support this sort of call is unsound. This is explained by the documentation; again, please refer to that if you haven’t yet.

There is always the temptation to poke a hole in the type system when dealing with the problem, “how do I express this?” That’s because you can then do something you want, without having gone through the bother of proving that it’s safe. “You can’t do whatever you feel like doing” is exactly what a sound type system must say. The benefits of soundness diffuse across your program, filling in the negative space of the tests that you no longer need to write; they can seem far away when confronted with a problem here to be solved now.

In this way, unsound features are the greatest ally of the pragmatist. They’re an asymmetric weapon, because sound features can never say “just do what you like, here; don’t worry about the distant consequences”.

We who have a strong distaste for pragmatism must make do instead with research.

A sound alternative, in Haskell

Haskell is a testbed for many advanced type system features, demarcated by extension flags. One of the joys of working with Haskell is learning about a new extension, what it means, and thinking of ways to use it.

Many of these features are guarded by an extension flag; we’re going to call on one such feature by placing at the top of the Haskell source file

{-# LANGUAGE GADTs #-}

One of the things this enables is that you can attach type parameters to enum members. EventFlag gets a type parameter indicating the associated type of event.

data EventFlag e where
  MousePress :: EventFlag MouseEvent
  KeyPress :: EventFlag KeyEvent

-- MouseEvent and KeyEvent can be
-- related types, but don't have to be
data MouseEvent = -- ...
data KeyEvent = -- ...

addCallback :: EventFlag e
            -> (e -> IO ())
            -> IO ()

e is a type parameter; when you pass an EventFlag to addCallback, the callback type (e -> IO () above) changes to reflect what event type is expected.

λ> :t addCallback MousePress
(MouseEvent -> IO ()) -> IO ()
λ> :t addCallback KeyPress
(KeyEvent -> IO ()) -> IO ()

This is a better design in two ways.

1. It is sound; you cannot screw up the relationship between the EventFlag argument and the event type that will be passed to the callback.
2. It is more convenient; if you pass a lambda as the callback argument, it will simply “know” that the argument type is KeyEvent or MouseEvent; your editor’s coding assistance can act accordingly, without you having to declare the lambda’s argument type at all.

I would go so far as to say that this makes this addCallback simpler; it’s easier and safer to use, and can even be implemented safely. By contrast, function parameter covariance requires you, the user of the function, to think through in your head whether it’s really OK, without type-checker assistance, and even then the library function can’t offer any help to callers if they declare the lambda argument type wrong.

What’s simpler?

A type system without powerful features for polymorphism makes it difficult or impossible to describe many programs and libraries in fully sound ways. A more powerful type system simplifies the task of the programmer—its features give you a richer language with which to describe generic APIs.

When the core of a type system doesn’t give you a way to type an interface, you might follow the pragmatist’s advice, and poke a hole in the type system. After that, you won’t be able to generally trust the conclusions of the type checker throughout the program, anymore.

Instead, you might look at the leading edge of type system research, for a sound way with which to express the API. This is not so expedient, but yields APIs that are safer and more convenient to use and implement.

With an unsound feature, the pragmatist can offer you the world, but cannot offer the confidence that your programs don’t “go wrong”. Powerful type system features might bend your mind, but promise to preserve that confidence which makes type systems, type systems.

This article was tested with TypeScript 2.4 and GHC 8.0.2.

The missing diamond of Scala variance

This article is an expanded version of my LambdaConf 2016 talk of the same name (video, slides). The below covers every topic from that talk, and much more on possible extensions to variance polymorphism, but the talk is a gentler introduction to the main concepts here.

As part of its subtyping system, Scala features variance. Using variance lets you lift the subtyping relation into type constructors, just like type equality (~) already does.

type Endo[A] = A => A     // invariant
type Get[+A] = Foo => A   // covariant
type Put[-A] = A => Foo   // contravariant

X ~ Y → Endo[X] ~ Endo[Y] // invariant
X <: Y → Get[X] <: Get[Y] // covariant
X <: Y → Put[Y] <: Put[X] // contravariant
             ↑reversed!↑

Subtyping is incomplete without variance

With simple type equality, you have four properties:

1. Reflexivity: A ~ A
2. Symmetry: A ~ B → B ~ A
3. Transitivity: A ~ B ∧ B ~ C → A ~ C
4. Congruence: A ~ B → F[A] ~ F[B]

Just try to use GADTs without equality congruence! That’s what’s expected in a subtyping system without variance.

1. Reflexivity: A <: A
2. Antisymmetry: A <: B ∧ B <: A → A = B
3. Transitivity: A <: B ∧ B <: C → A <: C
4. Congruence: A <: B → Put[B] <: Put[A]

Completing subtyping: variables

val aCat = Cat("Audrey")
val anAnimal: Animal = aCat

A bare type is in a covariant position. You can’t abstract over something as simple as a value box without variance.

Completing subtyping: the harmony of a function call

def speak(a: Animal): IO[Unit]
speak(aCat)

This is how functions and their arguments form a more perfect union. One way to think of the mechanics here is that Cat upcasts to Animal. But there’s no way to tell that what is really happening isn’t that the function is upcasting from Animal => IO[Unit] to Cat => IO[Unit]! Or that they aren’t meeting in the middle somewhere; maybe Cat upcasts to Mammal, and Animal => IO[Unit] upcasts to Mammal => IO[Unit].

So I don’t think there’s really subtyping without variance; there’s just failing to explicitly model variance that is there anyway. Since you cannot have subtyping without variance, if variance is too complicated, so is subtyping.

What else is there? What else is needed?

There is one advanced feature that fans of higher-kinded types would have found a deal-breaker to live without in Scala, even if they are unaware of its existence.

def same[A, F[_]](fa: F[A]): F[A] = fa
def widen[A, B >: A, F[+_]](fa: F[A]): F[B] = fa

All of Endo, Get, and Put can be passed as the F type parameter to same. However, only Get can be passed as the F type parameter to widen. This works because you can only “use” variance if you know you have it, but don’t need to make any assumptions about your type constructors’ variances if you don’t “use” it.

Variance exhibits a subkinding relation

same takes an invariant type constructor F, but you are free to pass covariant and contravariant type constructors to it. That’s because there is a subtype relationship between these at the type level, or a subkind relationship.

Invariance is the ‘top’ variance, the most abstract, and co- and contravariance are its subvariances. When you pass a covariant or contravariant type constructor as F to same, its variance “widens”.

Because variance is part of the “type of type constructor”, not the specific parameter where the variance annotation appears, it’s an element of the kind of that type constructor, just as arity is. For example, when we talk about the kind of Get , we don’t say that A has a covariant kind, because this variance has nothing to do with A. Instead, we say that Get has kind +* -> *, because this particular variance annotation is all about the behavior of types referring to Get. Moreover, subvariance is just a restricted flavor of subkind.

Flipping variances

I started to find it odd that this order of subclassing was enforced as a result of the subvariance relation.

mutable.Seq[A] extends Seq[+A]

CovCoy[F[+_]] extends Coy[F[_]]

It makes perfect sense empirically, though; you can easily derive unsafeCoerce if you assume this exact ordering isn’t enforced.

Then I found, while working on monad transformers, that this is the only way that makes sense, too.

InvMT[T[_[_]]] extends CovMT[T[_[+_]]]

CovMTT[W[_[_[+_]]]] extends InvMTT[W[_[_[_]]]]

I had seen this before.

Type parameter positions are variance-contravariant

The kinds of type constructors (type-level functions) work like the types of value-level functions. Both sorts of functions are contravariant in the parameter position. So every extra layer of nesting, “flips” the variance, just like with functions. Below is the version of this for value-level functions, akin to the examples above.

type One[-A] = A => Z
type Two[+A] = (A => Z) => Z
type Three[-A] = ((A => Z) => Z) => Z
type Four[+A] = (((A => Z) => Z) => Z) => Z

A bottom variance: the diamond, completed

Scala wisely included a bottom type, Nothing, to go with its top type Any. That helps complete its subtyping system, but a bottom variance was unfortunately left out of its subkinding system. Here’s something that might work.

type ConstI[👻A] = Int

ConstI[A] ~ ConstI[B] // phantom, or 👻

This is exactly what you’d get if you applied both the covariant and contravariant rules to a type parameter. Therefore, phantom variance or anyvariance is more specific than either, and as the ‘bottom’ variance, completes the diamond. It is the perfect choice, because it is truly a greatest lower bound; it is both more specific than either by itself and no more specific than both together.

Whence monad transformer variance?

There are two competing flavors of the monad transformers, like OptionT.

final case class NewOptionT[F[_],   A](run: F[Option[A]])

final case class OldOptionT[F[+_], +A](run: F[Option[A]])

The first remains invariant over A, but conveniently doesn’t care about the variance of F—its declared variance is the “top” variance. The latter gives the more specific covariance over A, but requires the F to be covariant (or phantom), which can be very inconvenient. These two transformers can’t be practically unified.

If you look at the structure, the variance of A’s position is always of a piece with the variance of F.

Variance variables

final case class OptionT[😕V, F[V😕_], V😕A]

1. The “variance variable” V is declared with the syntactic marker 😕.
2. 😕 appears infix before _ to say “F has the variance V for the type parameter in this position”.
3. 😕 appears infix before A to say “the parameter A has the variance V”.

Therefore, when you specify variance V = +, the remaining parameters have kind F[+_] and +A, and similarly for other variances.

I’ve chosen the confused smiley 😕 to represent likely reactions to this idea, and especially to my complete lack of consideration for elegant syntax, but it’s really just a limited form of a kind variable in PolyKinds—after all, variance is part of the kind of the surrounding type constructor. And, as seen above, we already have subkind-polymorphism with respect to variance, so what’s wrong with parametric kind polymorphism? “Variance variables” are just parametric kind polymorphism, but not as powerful.

Variance bounds

The OptionT example is a simple case; it supports all possible variances, and features a simple relationship: whatever you select for V is exactly the variance used at the various places V appears. It’s easy to break this simple scheme, though.

final case class WrenchT[F[_], A](run: F[Option[A]], wrench: A)

Now the variance of the A position isn’t strictly the variance of F, as it was with OptionT; it can only be covariant or invariant, due to the wrench being in covariant position.

Well, we have variables over something with a conformance relation, let’s add bounds!

final case class WrenchT[😕V >: +, F[V😕_], V😕A]

And these bounds themselves could be determined by other variance variables, &c, but I don’t want to dwell on that because the complications aren’t over yet.

No easy unification

final case class Compose[F[_], G[_], A](run: F[G[A]])

This type complicates things even further! There are numerous possibilities based on the variances of F and G.

F,G	G,F	A
Inv	Inv	Inv
Inv	+	Inv
Inv	-	Inv
Inv	👻	👻
+	+	+
+	-	-
+	👻	👻
-	-	+
-	👻	👻
👻	👻	👻

(The order of F and G doesn’t matter here, so I’ve left out the reverses here.) So the variance of A’s position is the result of multiplying the variance of F and G. The multiplication table is just above. Guess we need a notation for that.

[😕FV, 😕GV, 😕V >: FV × GV, F[FV😕_], G[GV😕_], V😕A]

The bound here only means that V is in variance-covariant position, but bounded by FV × GV.

Another wrench

We can privilege F a little bit to make things more interesting.

final case class ComposeWr[F[_], G[_], A](run: F[G[A]], fa: F[A])

F×G	F	A
	Inv,+,-	Inv
Inv,+,-,👻	Inv	Inv
+,👻	+	+
-	+	Inv
-,👻	-	-
+	-	Inv
👻	👻	👻

Here’s another level to the function that determines the A-position variance: it’s now lub(F×G, F), where lub is the least upper bound, the most specific variance that still holds both arguments as subvariances.

Variance families? Really?

I hope you guessed where I was going when I said “function”: the rules determining the lower bound on the A-position variance can be specified by the programmer with a variance-level function—a mapping where the arguments and results are variances—or a variance family. Again, I don’t think this is terribly novel; it’s just a kind family, but more restricted.

You’d want it closed and total, and I can see the Haskell now.

variance family LUBTimes a b where
  LUBTimes - + = -
  LUBTimes 👻 Inv = 👻
  …

Only because I’m not sure where to begin making up the Scala syntax.

There are four variances

When I started looking for ways to describe the variances of the datatypes I’ve shown you, I noticed the relationship between variance and kinds, converted the problem to a kind-level problem, and started thinking of solutions in terms of PolyKinds. That’s where variance variables come from, and everything else follows from those.

However, I think I’ve made a mistake. Not with variance variables themselves, mind you, nor the variance-conformance already built in to Scala. But, to deal with the problems that arise with only these, I’ve hypothesized tools—described above—that are way too powerful. They work on open domains of unbounded complexity—the kinds of types—and there are only four variances.

There are two reasons I think there must be a better approach.

First, there are finitely many variance families for a given sort.

Second, there are only so many ways to put variables in positions of variance. You get argument and result position of methods, within other type constructors, and that’s it. Things are simple enough that, discounting desire for working GADTs (which will be discussed in a later post, “Choosing variance for a phantom type”), it is always possible to infer which of the four variances a type parameter ought to have, in a first-order variance situation.

A “good” polyvariance constraint system

Since there are only four variances, and only so many ways to combine them, it might be possible to design something more refined and suited for the task than the too-powerful variance families.

It might be that there are only a few useful variance relations, like × and lub, and a good solution would be to supply these relations along with an expression model to combine them. Or maybe not. Instead, I’ll stop hypothesizing and instead say what a I think a “good” system would look like.

1. It must be writable. Just as it is desirable to write a stronger type role than the inferred one in GHC Haskell ≥ 7.8, there are very common reasons to want a more general variance than the one that would be inferred. So the convenience of writing out the rule explicitly matters a great deal.
2. It must be checkable. For variance variables, that means every possible variance you can choose puts every type parameter only in positions consistent with its variance. For example, our fully generalized OptionT always places A only in positions matching the variance of the F type constructor.

   We can just check every possible variance—up to four for each variable—but I think this is the wrong way to go. We don’t just enumerate over every possible type to check type parameters—that would take forever—we have a systematic way to check exactly one time, with skolemization. Variance is simpler—it should be an easier problem.

3. Not a requirement—but it ought to be inferrable. In the same way that skolemization gives us a path to automatic generalization, if there is a similar way to do quantified variance checking, it should be possible to use the output of that decision procedure to determine the relationships between and bounds on variance variables.

   How that decision is expressed is another question.

Variance & GHC type roles

It might seem that Haskell, with no subtyping, might not care about this problem. But GHC 7.8 type roles are similar enough to variances; the main difference is that Scala variance is about the congruence/liftability of the strong conformance relation, while type roles are about the congruence/liftability of the weak type equality/“coercibility” relation.

nominal:          a ~ b → f a ~ f b
representational: a ~w b → f a ~w f b
phantom:          f a ~w f b

This is pretty useful from a practical, performance-minded perspective, but the problem is

newtype MaybeT m a = MaybeT (m (Maybe a))

there is no way to describe the role of the a parameter in the most general way. It’s stuck at nominal, even if m’s parameter is representational.

Just as the integration of variance and higher kinds in Scala is incomplete without something like the polyvariance system I’ve been describing, Haskell’s type roles are not fully integrated with higher kinds.

I hope if one of these language communities finds a good solution, it is adopted by the other posthaste. The Haskell community is attempting to tackle these problems with roles; perhaps Scala can profit from its innovations. Much of the prose on the GHC matter can be profitably read by replacing “role” with “variance” where it appears. For example, this should sound familiar.

This design incorporates roles into kinds. It solves the exact problems here, but at great cost: because roles are attached to kinds, we have to choose a types roles in the wrong place. For example, consider the Monad class. Should the parameter m have type */R -> *, requiring all monads to take representational arguments, or should it have type */N -> *, disallowing GND if join is in the Monad class? We’re stuck with a different set of problems.

Subtyping or higher kinds?

As things stand, you will have a little trouble combining heavy use of subtyping and of higher kinds in the same system.

I’m not saying for certain that it comes down to one or the other. In Scalaz, we weakened support for subtyping to have better support for higher kinds, because its users typically do not want to use subtyping. However, this preference doesn’t generalize to the Scala community at large. This was only a real concern for monad transformers; most Scalaz constructs, for now, have fine subtyping support.

My suggestion is that you should favor higher kinds; they’re a more powerful abstraction mechanism, and ultimately easier to understand, than subtyping; they also happen to be less buggy in Scala. If you must use subtyping, be warned: it’s much more complex than it first seems.

Further reading

• “Choosing variance for a phantom type” builds upon this post to connect variance and pattern matching
• “Of variance and functors” by Adelbert Chang, provides some foundational intuition for variance
• SI-2066 “Unsoundness in overriding methods with higher‐order type parameters”, easily the most important surfacing of the interaction of higher kinds and variance, revealing the existence of subvariance
• The Liskov type, which builds every other subtyping property on reflexivity and contravariance