With type inference, structural records types can make a statically typed language feel almost like a scripting language, without giving up type safety:

// Works for any record with the fields width, height : Float
area2d v = v.width * v.height

Row polymorphism can be used to implement this, and can also be used for polymorphic variants, effect systems and stack types in concatenative languages. This post gives a few quick examples of how it works.

Suppose we have two functions that work on row polymorphic records:

f : forall row1. {a: Int, …row1} -> Int
g : forall row2. {b…


At the end of this article, we can infer generic types like these.

Continuing where we left off in part 6, let’s add in mutually recursive functions with generics.

Consider the following example:

function even(x) { return x == 0 || odd(x - 1); }
function odd(x) { return x != 0 && even(x - 1); }

We say that these functions are mutually recursive: even calls odd and odd calls even. Because of that, we can’t infer the types of each function in isolation — we must consider both at the same time. Let’s add support for such mutually recursive functions to our syntax tree:

case class EFunctions(
functions : List[GenericFunction]…


Wow, I’m glad we didn’t have to type all that!

Continuing where we left off in part 5, let’s extend the language and reconstruct the missing type annotations in the syntax tree.

First, we’ll extend the lambda function syntax and application so that it supports multiple arguments.

case class ELambda(
parameters : List[Parameter],
returnType : Option[Type],
body : Expression
) extends Expression

case class EApply(
function : Expression,
arguments : List[Expression]
) extends Expression

Apart from multiple arguments, we’ve also added optional type annotations. The Parameter contains a name and an optional type.

case class Parameter(
name : String,
typeAnnotation : Option[Type]
)

We’ll introduce let for local variables:

case…


First demo—type inference for lambda calculus.

Continuing where we left off in part 4, let’s finish implementing a first version of the type inference — and see a small demo.

The first thing we’ll need is a language to infer types for. Let’s start with the lambda calculus:

sealed abstract class Expression
case class ELambda(x : String, e : Expression) extends Expression
case class EApply(e1 : Expression, e2 : Expression) extends Expression
case class EVariable(x : String) extends Expression

We’ll also need a representation of constraints. For now, we only have equality constraints:

sealed abstract class Constraint
case class CEquality(t1 : Type, t2 : Type) extends…


Using unification to turn each equality constraint into a substitution.

Continuing where we left off in part 3, let’s take a look at unification.

The first thing we’ll need is a representation for types. Let’s look at the types we’ve seen so far:

  • Int — a plain type
  • Array<Int> — a generic type
  • (Int, Int) => Int — a function type
  • $1 — a type variable

The Array thing up there is called a type constructor — not to be confused with constructors in object oriented programming.


Inferring types for generic calls

Continuing where we left off in part 2, we’ll now consider calling a generic function:

function map<A, B>(array : Array<A>, body : A => B) : Array<B>

So this is the classic map function that applies a lambda function body to each element of the array and returns a new array with the results. Note that map takes two type parameters, A and B.

Here’s a function that squares each element of an array:

function square(items) {
return map(items, x => x * x);
}

Now, to add in the missing type annotations, we first must instantiate the type for…


Type inference for the empty array.

Continuing where we left off in part 1, let’s look at a more advanced example that uses local variables and type constructors:

function range(from, to) {
let numbers = [];
for(let i = from; i <= to; i++) {
numbers[i - from] = i;
}
return numbers;
}

As in the previous installment, we add in fresh type variables:

function range(from : $1, to : $2) : $3 {
let numbers : $4 = [];
for(let i : $5 = from; i <= to; i++) {
numbers[i - from] = i;
}
return numbers;
}

Now, on the very first…


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 {…

Joakim Ahnfelt-Rønne

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

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