ocaml - What is the difference between 'a and '_l?

Question

What is the difference between 'a and '_l?

I was looking at this error, and couldn't comprehend it:

Error: This expression has type ('a -> float polynomial) list but an expression was expected of type float polynomial list derivlist: ('_l → float polynomial) list

Answer 1

_ denotes a weakly polymorphic variable : it is in a position where it cannot be generalized.

There are two explanations related to weak polymorphism in the OCaml FAQ: see A function obtained through partial application is not polymorphic enough and the next one.

This generally happens when you're using a non-local reference (whose type cannot be generalized), or when defining polymorphic functions that are not syntactically functions (they do not begin with fun x -> .. but rather a function application). In some cases there is an easy fix (eta-expansion, see the FAQ), sometimes there isn't, and sometimes your program was just unsound.

An easy example : let a = ref [] does not get the polymorphic a list ref type. Otherwise you could use both as a int list and a bool list, and mix elements of different types by mutating the reference. It instead get a '_a list ref type. This mean that the type is not polymorphic, but merely unknown. Once you do something with a with a particular type, it fixes '_a once and for all.

# let a = ref [];;
val a : '_a list ref = {contents = []}
# let sum_of_a = List.fold_left (+) 0 !a;;
val sum_of_a : int = 0
# a;;
- : int list ref = {contents = []}

For an in-depth explanation of value restriction and the "relaxed" value restriction actually implemented in the OCaml type checker, see the Relaxing the Value Restriction paper by Jacques Garrigue (2004).