Hindley and Milner Walk Into a Bar
Jared Forsyth's talk breaks down type inference, showing how it automatically adds missing type annotations to code. He explains why this matters: understanding type inference helps you deal with errors in languages like TypeScript and better evaluate different type systems.
Using a Fibonacci function example, Jared shows how the algorithm creates type variables for declarations, then unifies expressions with expected types to discover concrete types through substitution. The unification process simply aims to make two types identical by substituting variables, revealing type errors when incompatible types meet.
Jared points out that while Hindley-Milner can't handle classes or inheritance like TypeScript, it's better at inferring function parameter types, recursive return types, and empty array types. For those interested in going deeper, he's created a type inference debugger tool that visualizes the entire process.
The talk positions type inference not just as a practical feature but as an exciting research area worth exploring further.
Share this talk
Transcript
Alrighty. We just had a two hour lunch break, so I'm gonna need everybody to stand up. I will do squats. That's right. We're doing squats. Only six because it's we just had lunch. Arms in front if you can. Count with me. One, two, three, four, five, six. We made it. Alright. Hopefully
hopefully some of your blood has made it up into your head so we can learn about Henley Milner type inference. I'm Jared Forsyth. I work for Khan Academy. And I'd like to thank the nice people at the bottom of the slide for giving me feedback on early versions of this talk. So, what is Type Inference?
You can think about it as the process of going from code without any type annotations and automatically adding them in. Here on the left, we have, some blank spots where in TypeScript you would be adding annotations and on the right they've been filled in for us.
It will also do type checking at the same time, finding type errors. For example, if you made a mistake of using a string where you should have used an int, it will find that for you and give you some kind of a type error.
The quality of the type error depends on the algorithm and how much, effort went into making those look nice. So why should you care? First of all, understanding the guts of type inference will help you better deal with type errors that you encounter in TypeScript, in Go or any other statically typed language.
It'll also help you better evaluate the pros and cons of different languages and their type systems and the features of those type systems. It's also just fun to learn stuff. And Type Inference and Type Systems is an exciting area of exploration, with a lot of ongoing research.
And I hope that this talk inspires some of you to go out and write your own type inference algorithms and extend the state of the art. Now, Hindley Milner specifically is quite an old algorithm, but it forms the core of some languages you may have heard about.
And it can actually be implemented in not very many lines of code but there are a lot of extensions to make the type system more flexible and more powerful. You might be thinking, well, what about TypeScript? Doesn't it have some inference? And it does but TypeScript's type inference is both more and less powerful than Henley Milner.
For example, TypeScript can't infer the types of function parameters. You have to fill those in yourself. It also can't infer the return type of a function that calls itself and it can't infer if you have an empty array and you assign it to a variable TypeScript just throws up its hands.
On the other hand, Hindley Milner can't represent classes and inheritance and subtyping. It also can't run doom, which we recently discovered TypeScript's type system can do. So hard to tell which one's better.
Let's talk about the algorithm. And we're gonna be looking at this recursive Fibonacci function. The first thing we do is create type variables for each variable declaration. We've got these blanks. We fill them in with the variables a, b, and c. These are placeholders that were are going to be replaced with the concrete types that we discover.
Then we go through each expression in the code and unify the current type with the expected type. Here on line two, we've got n is less than or equal to one. So the expected type here is gonna be an integer because it's being compared to one and the current type is this type variable B.
Unification gives us substitutions that we apply to eliminate the type variables. In this case, it's very simple. B goes to integer. We apply that and now N has a concrete type. And that's it. You go through the rest of the code and it will discover the types for you. Let's dive in a little bit more to unification.
The goal is to make two types identical by substituting type variables. Here we have two function types and we can dive into them and see that in the first argument, there's a type variable. So we can make a substitution, apply that and now we have bool and bool. We move on. The second arguments are the same.
In the return type, we have an array of something and in that something, we find another type variable, make another substitution and now the types are equivalent. If, as you're going through, you find two types that are incompatible for example, in this example, we have int and bool as the first argument that's a type error.
So to summarize, unification has the goal of making two types identical by substituting type variables. We walk through the types comparing each part. If we find on one side a type variable then that's a substitution. If we have two incompatible types then you found a type error.
For those that wanna go deeper into this, I made a type inference stepping debugger that will show you the whole process of Henley Milner working through a much, more detailed example, showing you how unification works, how the current and expected types are calculated, and how, substitution gets applied across the board.
And, for the very brave, I would recommend some, academic research papers about, Type Inference. These ones are written in mostly plain English. So I recommend them and they also go into some of the extensions to the type system to make it more powerful. Thank you very much.
