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.