Type inference, polymorphism and type errors

let count = List.fold_left (fun acc _ -> acc + 1) 0 looks harmless, yet the toplevel gives it the odd type '_weak1 list -> int, and the first list you count decides forever what it may count. Every type in that answer was worked out by OCaml itself, from how the values are used.

Here you read the types the compiler infers, see why a function bound with let can be used at many types while a parameter cannot, recognise weak type variables and remove them, and trace an error message back to the line that is really wrong.

OCaml works out every type from how the values are used

You rarely write a type in OCaml. The compiler starts each name with an unknown type and collects facts as it reads the body: a value passed to + must be an int, a value applied to an argument must be a function, two branches of an if must agree. This is type inferencetype inference: Working out the types of values and functions from how they are used, so most types need not be written; OCaml prints them in the toplevel. More in “What OCaml is and where it is used”, and it ends either with a type for every expression or with an error at the first place where two facts disagree. When nothing forces a type, it stays a type variabletype variable: A placeholder such as 'a in an inferred type, standing for any type; every occurrence of the same letter is the same type., written with a quote: 'a, 'b, read “alpha” and “beta”. A type variable means “any type, the same one wherever this letter appears”.

The session below defines a few small functions and prints what OCaml inferred for each:

from session import toplevel

# The toplevel prints the type it inferred for every definition. Type variables such as 'a stand for "any type", and a
# let-bound polymorphic value can be used at two types in one expression, while a function parameter cannot unless
# its annotation makes it polymorphic, which OCaml 5.5 allows.
toplevel("""
let id x = x;;
let pair = (id 1, id "one");;
let pair_of f = (f 1, f "one");;
let both = let id2 x = x in (id2 1, id2 "one");;
let pair_of (f : 'a. 'a -> 'a) = (f 1, f "one");;
pair_of Fun.id;;
let twice f x = f (f x);;
twice (fun n -> n * 3) 2;;
let compose f g x = f (g x);;
let swap (a, b) = (b, a);;
let first_or default l = match l with [] -> default | x :: _ -> x;;
List.map;;
fun x -> x +. 1.;;
let count = List.fold_left (fun acc _ -> acc + 1) 0;;
count [10; 20; 30];;
count ["a"];;
let count_all l = List.fold_left (fun acc _ -> acc + 1) 0 l;;
""")

$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# let id x = x;;
val id : 'a -> 'a = <fun>
# let pair = (id 1, id "one");;
val pair : int * string = (1, "one")
# let pair_of f = (f 1, f "one");;
Line 1, characters 24-29:
1 | let pair_of f = (f 1, f "one");;
                            ^^^^^
Error: This constant has type string but an expression was expected of type
         int
# let both = let id2 x = x in (id2 1, id2 "one");;
val both : int * string = (1, "one")
# let pair_of (f : 'a. 'a -> 'a) = (f 1, f "one");;
val pair_of : ('a. 'a -> 'a) -> int * string = <fun>
# pair_of Fun.id;;
- : int * string = (1, "one")
# let twice f x = f (f x);;
val twice : ('a -> 'a) -> 'a -> 'a = <fun>
# twice (fun n -> n * 3) 2;;
- : int = 18
# let compose f g x = f (g x);;
val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun>
# let swap (a, b) = (b, a);;
val swap : 'a * 'b -> 'b * 'a = <fun>
# let first_or default l = match l with [] -> default | x :: _ -> x;;
val first_or : 'a -> 'a list -> 'a = <fun>
# List.map;;
- : ('a -> 'b) -> 'a list -> 'b list = <fun>
# fun x -> x +. 1.;;
- : float -> float = <fun>
# let count = List.fold_left (fun acc _ -> acc + 1) 0;;
val count : '_weak1 list -> int = <fun>
# count [10; 20; 30];;
- : int = 3
# count ["a"];;
Line 1, characters 7-10:
1 | count ["a"];;
           ^^^
Error: This constant has type string but an expression was expected of type
         int
# let count_all l = List.fold_left (fun acc _ -> acc + 1) 0 l;;
val count_all : 'a list -> int = <fun>

let id x = x got 'a -> 'a: whatever goes in comes out, so the argument and the result share one variable. swap got 'a * 'b -> 'b * 'a, two variables because the two parts of the pair may differ. List.map itself has the type ('a -> 'b) -> 'a list -> 'b list, which says everything about it except its name: give it a function from 'a to 'b and a list of 'a, and it returns a list of 'b. fun x -> x +. 1. got float -> float, because +. adds floats only.

Step through how the facts fix the type of twice, whose body applies f two times:

The second application is what ties the result type to the argument type. A function applied to its own result must return the type it takes, which is why twice wants a function of type 'a -> 'a and why twice (fun n -> n * 3) 2 gave 18.

A function bound with let works at many types, a parameter at only one

let pair = (id 1, id "one") type-checked and gave (1, "one"): one expression used id at int and at string. That works because a let binding is generalisedgeneralisation: Turning the type variables of a let-bound value into ones each use may choose afresh, which lets id work at int and at string.. Once id is defined, its 'a may stand for a different type at each use, as if every use received a fresh copy of the type. This is called let-polymorphism, and the core-language chapter of the manual relies on it from its first examples.

A function’s parameter is not generalised. let pair_of f = (f 1, f "one") was refused: the toplevel underlined "one", a string, at a place where only an int could go. Inside the body f has one type, and f 1 had already fixed its argument to int when f "one" came along.

Without such an annotation, the rule is about where a name is bound, not about what it is:

Notice where the error was reported: at "one", the second use, although f 1 is written first and either use alone is fine. A type error marks the point where the checker met a contradiction, which is the subject of the last section.

A weak type variable is one unknown type that the first use fixes

Some definitions get a type variable with an underscore, '_weak1. The manual calls these weakly polymorphic type variables: each one is a placeholder for a single type that is not known yet, not for any type. They come from the value restrictionvalue restriction: The rule that OCaml generalises a let only when its right-hand side is a syntactic value: the result of a call such as ref [] keeps weak type variables such as '_weak1, which its first use fixes. A relaxed form still generalises a variable that appears only in covariant positions.. A definition whose right-hand side is the result of a function call, such as ref [] or List.map (fun x -> x), might hide mutable state, so OCaml does not generalise its type variables. The session shows two of them and what the first use does to each:

from session import toplevel

# The value restriction: a definition that is the result of a computation, not a function written with fun, gets weak
# type variables, '_weak1 and so on, but only where a type variable is left. The first use fixes them; writing the
# parameter out keeps the type polymorphic.
toplevel("""
let r = ref [];;
r := [3];;
r;;
let f = List.map (fun x -> x);;
f [1; 2];;
f;;
f ["a"];;
let lengths = List.map String.length;;
let g l = List.map (fun x -> x) l;;
g [1; 2];;
g ["a"];;
""")

$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# let r = ref [];;
val r : '_weak1 list ref = {contents = []}
# r := [3];;
- : unit = ()
# r;;
- : int list ref = {contents = [3]}
# let f = List.map (fun x -> x);;
val f : '_weak2 list -> '_weak2 list = <fun>
# f [1; 2];;
- : int list = [1; 2]
# f;;
- : int list -> int list = <fun>
# f ["a"];;
Line 1, characters 3-6:
1 | f ["a"];;
       ^^^
Error: This constant has type string but an expression was expected of type
         int
# let lengths = List.map String.length;;
val lengths : string list -> int list = <fun>
# let g l = List.map (fun x -> x) l;;
val g : 'a list -> 'a list = <fun>
# g [1; 2];;
- : int list = [1; 2]
# g ["a"];;
- : string list = ["a"]

let r = ref [] got '_weak1 list ref. After r := [3], r had type int list ref, and it keeps that type: if it were 'a list ref, the program could store ints and then read them back as strings. let f = List.map (fun x -> x) got '_weak2 list -> '_weak2 list; f [1; 2] fixed it to int list -> int list, and the next call, f ["a"], was refused. Only type variables are weakened: let lengths = List.map String.length is a partial application too, but it got the complete type string list -> int list. Writing the parameter out, let g l = List.map (fun x -> x) l, turns the definition into a function written with a parameter, which is generalised again: g took both [1; 2] and ["a"]. Adding the parameter is called eta-expansion. Step through the same definitions:

The count of the opening, at the end of the first session, is the same case. List.fold_left (fun acc _ -> acc + 1) 0 is a partial application, so it got '_weak1 list -> int; count [10; 20; 30] gave 3 and fixed the type to ints, and count ["a"] was refused. Written with its parameter, let count_all l = … l got 'a list -> int.

In the toplevel a weak type can wait for its first use. In a compiled file it cannot, because every module must have a complete type when it is compiled:

from session import run, write

# The toplevel lets a weak type wait for its first use, but a compiled module must have a complete type. ocamlc
# refuses a module whose top-level value still has a weak type; an annotation gives it one.
write("store.ml", "let store = ref []\n")
write("store_fixed.ml", "let store : string list ref = ref []\n")
run("""
cat store.ml
!ocamlc -c store.ml
cat store_fixed.ml
ocamlc -c store_fixed.ml
ocamlc -i store_fixed.ml
""")

$ cat store.ml
let store = ref []
$ ocamlc -c store.ml
File "store.ml", line 1, characters 4-9:
1 | let store = ref []
        ^^^^^
Error: The type of this expression, '_weak1 list ref,
       contains the non-generalizable type variable(s): '_weak1.
       (see manual section 6.1.2)
[exit status 2]
$ cat store_fixed.ml
let store : string list ref = ref []
$ ocamlc -c store_fixed.ml
$ ocamlc -i store_fixed.ml
val store : string list ref

ocamlc -c store.ml stopped with “contains the non-generalizable type variable(s): ’_weak1”, and the annotated let store : string list ref = ref [] compiled, with the type val store : string list ref that ocamlc -i printed.

A type error marks where two types met, not always the mistake

An error message names a place and two types: the type the expression has, and the type the context expected. The place is where the checker found the contradiction, which can be after the line you got wrong. Four broken definitions and their messages:

from session import toplevel

# Four broken definitions and the messages OCaml 5.5.1 gives for them. The last two are the same mistake: a sum that
# starts from the int 0 but adds floats. Without annotations the error appears at a later use; with them, at the 0.
toplevel("""
let add_tip bill = bill + 1.5;;
"Total: " ^ 42;;
String.length ['a'; 'b'];;
let rec sum l = match l with [] -> 0 | x :: rest -> x +. sum rest;;
let rec sum (l : float list) : float = match l with [] -> 0 | x :: rest -> x +. sum rest;;
let rec sum (l : float list) : float = match l with [] -> 0. | x :: rest -> x +. sum rest;;
sum [1.5; 2.25];;
""")

$ ocaml
OCaml version 5.5.1
Enter #help;; for help.

# let add_tip bill = bill + 1.5;;
Line 1, characters 26-29:
1 | let add_tip bill = bill + 1.5;;
                              ^^^
Error: The constant 1.5 has type float but an expression was expected of type
         int
# "Total: " ^ 42;;
Line 1, characters 12-14:
1 | "Total: " ^ 42;;
                ^^
Error: The constant 42 has type int but an expression was expected of type
         string
# String.length ['a'; 'b'];;
Line 1, characters 14-24:
1 | String.length ['a'; 'b'];;
                  ^^^^^^^^^^
Error: This expression should not be a list literal, the expected type is
       string
# let rec sum l = match l with [] -> 0 | x :: rest -> x +. sum rest;;
Line 1, characters 57-65:
1 | let rec sum l = match l with [] -> 0 | x :: rest -> x +. sum rest;;
                                                             ^^^^^^^^
Error: This expression has type int but an expression was expected of type
         float
# let rec sum (l : float list) : float = match l with [] -> 0 | x :: rest -> x +. sum rest;;
Line 1, characters 58-59:
1 | let rec sum (l : float list) : float = match l with [] -> 0 | x :: rest -> x +. sum rest;;
                                                              ^
Error: The constant 0 has type int but an expression was expected of type
         float
Hint: Did you mean 0.?
# let rec sum (l : float list) : float = match l with [] -> 0. | x :: rest -> x +. sum rest;;
val sum : float list -> float = <fun>
# sum [1.5; 2.25];;
- : float = 3.75

The first three point at the mistake itself. bill + 1.5 mixes an int operator with a float, "Total: " ^ 42 joins a number to a string, and String.length ['a'; 'b'] passes a list where a string belongs; OCaml 5.5.1 even says “This expression should not be a list literal”. The fourth is the instructive one. The sum starts with [] -> 0, which makes the result an int, and only later meets x +. sum rest, which needs a float. The message underlines sum rest, a correct expression, because that is where an int met a context that wanted a float:

With the types written down, (l : float list) : float, the checker knew the result type before it read the branches, and the same mistake was reported at the 0, with the hint “Did you mean 0.?”. Annotations never change what a program does; they only give the checker a fact earlier, which moves the message closer to the mistake. The corrected sum [1.5; 2.25] gave 3.75.

Practise: reading types and errors

The questions below give definitions like the ones in the sessions. Decide the type or the error from the rules, then check your answer against the toplevel’s output:

Interview questions

Warm-up (fresher to 2–5 years): what does a type such as ’a -> ’a mean, and who writes it?

OCaml writes it. The compiler infers the type of every definition from how its values are used, and when nothing forces a particular type it leaves a type variable such as 'a. 'a -> 'a is the type of a function that returns a value of the same type it receives, whatever that type is: let id x = x has it. Because a let binding is generalised, each use of id can pick its own type, so (id 1, id "one") is fine. A variable with an underscore, '_weak1, is different: it stands for one type not known yet, which the first use will fix.

Two harder questions follow, about a module that does not compile because of a weak type and about an error message that underlines correct code. Decide your answer, then open each first step:

Key takeaways

• OCaml infers every type from how values are used, and leaves a type variable such as 'a where nothing forces a particular type.
• A let binding is generalised, so id can be used at int and string in one expression, while a function parameter has one type throughout its body.
• A weak type variable such as '_weak1 is a single unknown type caused by the value restriction; the first use fixes it, and a written-out parameter or an annotation removes it.
• A type error marks where two types met, which may be after the real mistake; annotations give the checker the facts earlier and move the message to the cause.