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
_
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
involving 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).