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 expressionHindley 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:
- Implicit numeric coercions
- Object-oriented inheritance
- Existential quantification (the dual of universal quantification)
- Refinement types
… 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:
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
This paper provides an all-in-one presentation of how to implement a bidirectional type-checking system
-
This explains the general principles behind bidirectional type-checking so that you can better understand how to extend the type system with new features
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.
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.
ReplyDeleteOne 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.
Nick, is your talk available online anywhere?
ReplyDelete