Dive C1.01.2

Type inference

Static types, almost none of them written by hand.

F# is statically typed, yet a typical F# file has few type annotations. The reason is inference: the compiler reads a type for every binding from how the value is used. The literal 5 is an int; an n + 1 forces n to be an int; a function that places no constraint on its argument is given a generic type that works for any. The result is the safety of static types with little of the typing. This dive works through the rule: where a type comes from, and how F# generalises to the most general type it can.

Infer an expression Module hub

C1.01.2 · part 1

Where a type comes from

A binding gets its type from the most specific thing the compiler can pin it to. For a plain value, the literal settles it: let x = 5 makes x an int, and let y = 5.0 makes y a float, because 5 and 5.0 are literals of those types. For a function, F# reads the parameter types from the operations applied to them.

Take let inc n = n + 1. The body adds n to the int literal 1; addition needs both sides to be the same type, so n is fixed to int, and the function is int -> int. Take let area r = 3.14159 * r * r. The multiplications involve the float literal 3.14159, so r is a float and the function is float -> float. The constraint comes from a single literal in each case.

let x = 5                  // val x : int = 5
let y = 5.0                // val y : float = 5.0
let s = "hi"               // val s : string = "hi"

let inc n = n + 1           // val inc : int -> int      ( + 1 pins n to int )
let area r = 3.14159 * r * r // val area : float -> float ( 3.14159 pins r to float )

F# reads types left to right, top to bottom. A value must be defined before it is used, and the inference flows in that order — which is why the constraints above resolve from the literals already in scope.

C1.01.2 · part 2

Generalisation: the most general type

When a function places no constraint on a value, F# does not guess a concrete type — it keeps the type generic, written with a type variable such as 'a. Consider let first (a, b) = a. The function returns the first element of a pair and never touches the second, so nothing fixes either element. F# infers 'a * 'b -> 'a — for any first type 'a and any second type 'b, return the first. The function works on a pair of anything.

The same applies to higher-order functions. let twice f x = f (f x) applies f to x, then to the result. For that to type-check, f must take and return the same type, and x must be that type — but the type itself is unconstrained. F# infers ('a -> 'a) -> 'a -> 'a, the most general type that fits. This is parametric polymorphism: one definition, sound for every type that satisfies the shape.

let first (a, b) = a       // val first : 'a * 'b -> 'a
let twice f x = f (f x)    // val twice : ('a -> 'a) -> 'a -> 'a

// twice works at any type that fits the shape:
twice (fun n -> n + 1) 0    // => 2     ( 'a = int )
twice (fun s -> s + "!") "hi" // => "hi!!" ( 'a = string )

Where a use pins the type, F# fixes it; where nothing pins it, F# keeps it generic. One definition, the most general type that is still sound.

Inference explorer

Select an expression below. The readout shows the type F# infers — exactly as FSI prints the binding's signature — and the one constraint that pins it. Every signature was checked against dotnet fsi.

Pick an expression · read the inferred type and its reason

val inc : int -> int

The body adds n to the int literal 1; addition forces both sides to one type, so n is int and the function is int to int.

Read off the screen the work the compiler does: a literal or an operator pins a type, and where none does, the type stays a variable that fits all.

The idea

A type is determined by use. Where use leaves it open, the most general type — a type variable — is kept.

F# today

let twice f x = f (f x) needs no annotation; F# infers ('a -> 'a) -> 'a -> 'a and it works at every type.

C1.01.2 · part 3

When to annotate

Inference covers most cases, but a type annotation is written when the compiler has too little to go on, or when an explicit type makes the intent clearer at a boundary. The syntax puts the type after a colon. On a value: let x : int = 5. On a parameter: let add (a: float) (b: float) = a + b, where without the annotation + would default a and b to int. On a return type: let f x : int = x, which fixes both the result and, through it, x to int.

An annotation never changes how inference works; it only adds a constraint the compiler must satisfy. If the annotation disagrees with the use, that is a type error reported at compile time, before the program runs.

let x : int = 5            // val x : int = 5         ( value annotation )
let add (a: float) (b: float) = a + b
                           // val add : float -> float -> float
let f x : int = x          // val f : int -> int      ( return-type annotation )

Annotate at a boundary, or where inference has too little to go on. Everywhere else, the type is already known — let the compiler write it.

From inference to the REPL

Inference is a compile-time process, but the fastest way to see its result is to ask the tool directly. Type a binding into FSI and it prints the inferred signature on the next line — the val inc : int -> int shown throughout this dive is FSI's own output. The final dive of this module covers FSI itself: how to start it, how to read what it prints, and the directives that load scripts and time code.

↑ C1.01 · Values ← C1.01.1 · Primitive types C1.01.3 · F# Interactive →

References

Sources

Microsoft — F# documentation — type inference, generic functions, and annotations.
The F# Language Specification — the inference algorithm and generalisation rules.
FSharp.Core API documentation — the generic signatures F# infers across the core library.

Related in this course

C1.01.3 — F# Interactive — the REPL that prints the signatures shown here.
C1.01 — Values, types & FSI — the module hub and its three dives.
Elixir — Immutability — values fixed at the bind point, on the BEAM.