ocaml

What is the difference between 'a and '_l?


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

Solution

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