Introduction

So you've just finished generating the abstract syntax tree for your language, and you want to implement some kind of type inference. Or maybe you're fascinated by the scarce amount of type annotations you need in a language like Haskell or Rust and you want to know how it works. You search around but all you can find are tutorials using functional languages that you struggle to understand or notation heavy research papers that you feel you need a master’s degree to even read.

This series is for you.

But first, what is a type system?

Let's clear up some misconceptions you may have. There are many type systems used across a multitude of programming languages. At its core, a type system is, by definition, a set of formal mathematical rules that specify what type a variable or expression is given some information we have about the program. Consider this code you might find in a C program:

int index;

If we were to write down C's type system on paper, we might have a rule that informally states:

If we see a variable declaration with the word int written in front of it, the type of that variable is int.

At first glance, this looks like an absolutely useless rule. But note carefully the two different meanings of int. The first time it's used, it's referring to the syntax int (what we literally see in our code). The second time it's used, it's referring to the type int (something a type checker can understand).

Here's another example written in C++:

auto flag = true;

Here we might see a rule stating:

If we see a variable initialization with the word auto written in front of it, the type of the variable is the type of the expression it's assigned to.

We can imagine how changing or adding new rules can result in wildly different and unique type systems. Of course, some rules (and by extension, type systems) make more sense than others. As a simplistic example, it wouldn't make sense to have a rule stating: the expression true has the type float (unless of course, you're trying to prank someone). As such, the design of useful and practical rules and type systems is an active area of research.

Type systems and type inference

You may have read the previous section and wondered, "Hey, can't we turn those rules into a type inference algorithm?", and you'd be right. Most type systems are syntax directed which means that each rule matches with a piece of syntax in a language. We will leverage this property when we write a bidirectional type checker later in the series. For now however, we will make one thing clear:

A type system is not the same as a type inference algorithm itself.

Just because a type system is capable of sophisticated type inference doesn't mean an algorithm for that system fulfills that level of sophistication. There are often many algorithms and one might opt for a less powerful one if it improves the quality of error messages or makes implementation easier. Directly translating a type system's rules into an algorithm (with the aforementioned syntax directed approach) does not usually yield the most powerful algorithm for that type system and, more importantly, isn't often directly applicable to your language. Take the rules for the Hindley-Milner type system:

It's not obvious how one might turn these rules into an algorithm for an imperative language (if you can understand them!). There aren't any syntactic constructs specific to a language like C like for or while loops. It's clear we'll have to take a different approach.

The Hindley-Milner type system

Throughout this series we will be implementing type inference for the Hindley-Milner type system (or lesser variants thereof). Yes, the same type system as that frightful picture describes. Don't worry, we won't need to comprehend those rules for our approaches.

Hindley-Milner has actually been around since 1969¹ and was independently discovered by both, you guessed it, Hindley and Milner. It forms the basis of type systems in many influential functional languages such as ML, Clean, and Haskell and is also used in some imperative languages (perhaps most notably, Rust²). People have written many articles on it for futher reading. Here are some neat features of Hindley-Milner:

• Types are completely inferable
• Has practically efficient type inference algorithms
• Supports generics (also known as parametric polymorphism)

Here are some features that it does not support:

• Traits (also known as typeclasses and similar to C++ concepts)
• Subtyping (inheritance)

We'll explore how we might implement extensions of Hindley-Milner in future chapters.