Type Inference by Example

Type inference, in a nutshell

If you’re implementing a programming language, you might be pondering how to do type inference. Instead of going through the theory, we’ll go through some examples to build an intuition for how it works, and finally see how to put that into code.

Consider the following function:

function f(x) {
return x * 2;
}

Since there’s no type annotation for x, and no explicit return type, we'll have to infer those.

For this, we can generate two fresh type variables $1 and $2, and add those to our syntax tree:

function f(x : $1) : $2 {
return x * 2;
}

What are type variables? They are integers that act as placeholders for types that we don’t yet know. During type inference, they will be replaced with other types and thus disappear from the syntax tree.

For the expression x * 2, we know the type of * : (Int, Int) => Int, so we check x and 2 both with the expected type Int. We know that x : $1 and 2 : Int, so we get the type constraints:

$1 == Int
Int == Int

What are type constraints? They are a way to record things we discover about types and their relations to each other, as we go through the type inference. An equality constraint may literally be represented in code as a pair of types.

For the statement return x * 2; we know from the type of * that x * 2 returns an Int, and from return that this must be the return type, so we get the constraint:

$2 == Int

Now that we have a set of constraints, we need to solve them. Perhaps you can solve a system of equality constraints with pen and paper, but the algorithm to do it is called unification. We will cover the implementation of that later, but the output is a substitution — in this case the following:

$1 := Int
$2 := Int

What is a substitution? It’s a map from type variables to types.

Applying the substitution to our syntax tree — replacing each type variable on the left hand side with the type on the right hand side — we get:

function f(x : Int) : Int {
return x * 2;
}

And we’re done.

Stay tuned for part 2, where we’ll go through a more advanced example.

--

--

--

MSc Computer Science, working with functional programming in the industry — github.com/ahnfelt

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Hey Google! Talk to…

CS373 Fall 2021: Craig Leeson: Final Entry

DialogFlow(formerly API.AI): Let’s create a Movie ChatBot in minutes

Rails and the Seven RESTful Routes

Back in the saddle, what’s been going on, and… hire #1 (Week 50)

Analyzing League of Legends dataset with Pandas and Python3

Bouncer: Simple AWS Auto Scaling Rollovers

2D Galaxy Shooter: Setting Enemy Explosions

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Joakim Ahnfelt-Rønne

Joakim Ahnfelt-Rønne

MSc Computer Science, working with functional programming in the industry — github.com/ahnfelt

More from Medium

Programming 101: Declarative vs Imperative Paradigm

Memory Management : Aligned malloc() and free( )

Firestore Full-Text Search With Elastic Search Part 1: Setup

How to Prepare for and Do Well During the Technical Interview