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 Integers, 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.

Conclusion

If you’d like to learn more about bidirectional type-checking then I recommend reading:

As I mentioned earlier, bidirectional type-checking has a lot of cultural cachet within the programming language theory community, so even if you don’t plan on using it, understanding it will help you speak the same language as many others within the community.

2 comments:

  1. It's funny, I just gave a talk on combining Hindley-Milner with subtyping today! The prevailing view for many years was indeed that this is difficult to do, but I think these days that is changing. In particular the work of Stephen Dolan (https://dl.acm.org/doi/10.1145/3093333.3009882) put to rest some of the concerns that people had about subtyping. I'm not sure what the 'cute hack' referred to in this post is, but if it refers to unification then Dolan describes a very similar biunification procedure that handles subtyping just fine. Parreaux (https://dl.acm.org/doi/10.1145/3409006) provides another perspective on Dolan's approach.

    One of the often-cited early papers on bidirectional typing is Pierce & Turner (https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf). Benjamin Pierce often emphasizes the distinction between the two different ideas used in that paper: (1) local type inference and (2) bidirectional type inference. Local type inference refers to avoiding the use of 'global' constraint solving techniques like unification. Bidirectional typing, to him, is a particular way of dividing a type inference procedure up into a synthesizing part and a checking part. It works with both local and global approaches. I could be wrong about this, but I have heard GHC actually structures type inference in a bidirectional way while also using global HM-style equality constraints. Anyway, I think it has become fairly common to conflate (1) and (2) in casual conversation these days, so maybe the difference is seen by some as a technicality.

    ReplyDelete
  2. Nick, is your talk available online anywhere?

    ReplyDelete