## Friday, June 3, 2022

### The appeal of bidirectional type-checking

The appeal of bidirectional type-checking

In this post I hope to explain why bidirectional type-checking has a lot of cultural cachet within the programming language theory community. To be clear, I’m an amateur and I have no formal background in computer science or type theory. Nonetheless, I believe I’ve learned enough and compared notes with others to motivate bidirectional type-checking.

#### Subtyping

The fundamental problem that bidirectional type-checking solves well is subtyping. I will not explain why in this post, so for now take it as an article of faith that bidirectional type-checking provides a simple and consistent framework for supporting subtyping within a programming language’s type system.

Bidirectional type-checking does other things well, too (such as inferring the types of inputs from outputs), but subtyping is the thing that bidirectional type-checking does uniquely well. For example, you can infer inputs from outputs using unification instead of bidirectional type-checking, which is why I don't motivate bidirectional type-checking in terms of doing inference "in reverse".

By “subtyping”, I mean that a type `A` is a subtype of type `B` if any expression of type `A` is also a valid expression of type `B`.

For example, we could create a language that provides two numeric types:

• `Natural` - The type of non-negative integers (ℕ)

• `Integer` - The type of all integers (ℤ)

Furthermore, we could define `Natural` to be a subtype of `Integer` (i.e. ℕ ⊆ ℤ). In other words, if a scalar literal like `4` were a valid `Natural` number then `4` would also be a valid `Integer`, too. That would permit us to write something like this Fall-from-Grace code:

``````let x = 4 : Natural

in  [ x, -5 ] : List Integer``````

… and the type-checker would not complain that we put a `Natural` number inside a `List` of `Integer`s, because a `Natural` number is a subtype of an `Integer`.

#### Why subtyping matters

Now, automatic numeric coercions like that are convenient but in the grand scheme of things they are not a big deal from a language implementer’s point of view. The real appeal of subtyping is that subtyping appears in more places than you’d expect.

I’m not even talking about object-oriented subtyping like “The `Dog` class is a subtype of the `Animal` class”. Subtyping occurs quite frequently in even non-OOP languages, in the form of universal quantification (a.k.a. “polymorphism” or “generics”).

For example, we can define a polymorphic identity function, but then use the function as if it had a narrower (more specialized) type:

``````let id : forall (a : Type) . a -> a
= \x -> x

in  id : Text -> Text``````

… and that works because `forall (a : Type) . a -> a` is a subtype of `Text -> Text`.

Yes, you read that right; I didn’t get the subtyping direction backwards. A polymorphic type is a subtype of a more specialized type.

In fact, `forall (a : Type) . a -> a` is a subtype of multiple types, such as:

• `Integer -> Integer`
• `List Natural -> List Natural`
• `{ x: Bool } -> { x: Bool }`

… and so on. This might be a bit counter-intuitive if you come from an OOP background where usually each type is a subtype of at most one other (explicitly declared) supertype.

This type specialization is implicit, meaning that we don’t need the type annotation to use `id` on a value of type `Text`. Instead, the specialization happens automatically, so we can use `id` on any value without annotations:

``````let id : forall (a : Type) . a -> a
= \x -> x

in  id "ABC"``````

If our language didn’t support subtyping then we’d need to explicitly abstract over and apply type arguments. For example, this is how that same `id` example would work in Dhall (which does not support any form of subtyping):

``````let id : forall (a : Type) -> a -> a
= \(a : Type) -> \(x : a) -> x
-- ↑ Explicit type abstraction

in  id Text "ABC"
-- ↑ Explicit type application``````

Typically I refer to a Dhall-style type system as “explicit type abstraction and type application”. Vice versa, I refer to a Grace-style language as “implicit type abstraction and type application”.

The real reason why subtyping matters is because you need to support subtyping in order to implement a language with “implicit type abstraction/application”. In other words, you need some way to automatically produce and consume polymorphic types without explicit types or type annotations from the end user and that is essentially a form of subtyping.

#### Bidirectional type-checking vs unification

Bidirectional type-checking is not the only way to implement a language with implicit type abstraction/application. For example, Hindley-Milner type inference is a type system that is based on unification instead of bidirectional type-checking type system and Hindley-Milner inference still supports implicit type abstraction/application.

The reason why Hindley Milner type inference works, though, is by exploiting a narrow set of requirements that do not generalize well to more sophisticated type systems. Specifically:

• Hindley Milner type inference only permits “top-level polymorphism”

In other words, Hindley Milner type inference only permits universal quantification at the top-level of a program or at the top-level of a `let`-bound expression

• Hindley Milner type inference does not support any other form of subtyping

To expand on the latter point, language implementers often want to add other forms of subtyping to our languages beyond implicit type abstraction/application, such as:

… and if you try to extend Hindley Milner type inference to add any other language feature that requires subtyping then you run into issues pretty quickly. This is because Hindley Milner exploits a cute hack that does not generalize well.

In contrast, bidirectional type-checking is not just a method for handling implicit type abstraction/application. Rather, bidirectional type-checking is a framework for introducing any form of subtyping, of which implicit type abstraction/application is just a special case.