Type of explicitly polymorphic function

Learning
3

First, as stated by @lukstafi , your use case can be covered by an explicit universal quantification:

type ('a, 'b) conv = 
  | Int_to_float : (int, float) conv
  | Int_to_string : (int, string) conv
  | Float_to_int : (float, int) conv

let int_conv: type a. int -> (int, a) conv -> a   = fun i conv ->
    match conv with
    | Int_to_float -> float_of_int i
    | Int_to_string -> string_of_int i
    | _ -> .

Here I am using type a. ... since we need both the universal quantification and the locally abstract type. I generally recommend to use this variant in all cases.

Polymorphic record fields are needed for higher-rank polymorphic functions: functions that takes other functions as argument and use those functions on multiple types.

For instance, if I try to write a function that convert a integer to both float and int using a conv function taken in argument

let apply_twice conv n =
  Format.printf "%f=%s" (conv n Int_to_float) (conv n Int_to_string)

I end up with a compiler error:

Error: This expression has type (int, string) conv
      but an expression was expected of type (int, float) conv
      Type string is not compatible with type float

because in the body of apply_twice, the function conv is supposed to be monomorphic.
Polymorphic record fields are a solution to this conundrum:

type 'a polyconv = { conv: 'b. 'a -> ('a,'b) conv -> 'b }
let apply_twice {conv} n =
  Format.printf "%f=%s" (conv n Int_to_float) (conv n Int_to_string)

(The polymorphism and its limitation section of manual has more information)

The issue however is that type inference for higher-rank polymorphism is undecidable in general. To alleviate this issue, OCaml limit the use of explicit universal type quantification to either let bindings, record fields and object methods. Those limitations are sufficient to make type inference decidable once again. But this means that it is not possible to allow a type abbreviation to contain explicit universal quantification, like

type t = 'a. 'a -> 'a

and generally it is simpler to have only one way (or two if counting object methods and record fields separately) to box polymorphic type expressions.

Note that for constructors, it is possible to have an explicit universal quantification too. However, in this case the quantification describes the behavior of the constructor. Typically, in

type printable = Printable:  'elt. ('elt -> string) * 'elt -> printable

the type 'a. ('a -> string) * 'a -> printable means that for any type 'a, I can construct a printable value by putting both a printing function of type 'a -> string and a value inside the constructor Printable. However, this is the dual situation compared to the record type: I am declaring how to construct a value of type printable from a value of type 'a . ('a -> string) * 'a rather than defining the content after deconstructing the value.

Consequently, when I peak inside Printable (print,x), I don’t get an universally quantified type, but its dual: an existential quantification. In other words, I know that there is some type 'a, such that the type of print is 'a -> int, and the type of x is 'a. Thus I can write:

let to_string (Printable(print,x)) = print x
let int n = Printable(string_of_int, n)
let string s = Printable(Fun.id, s)
let l = List.map to_string [int 0; string "hi"]

but I don’t know anything else about this type 'a. In particular, I cannot write

let print_int (Printable(print,_)) = print 0

because as stated by the compiler

Error: This expression has type int but an expression was expected of type
$Printable_'elt

I have no idea if the type int is compatible with the type expected by the printer stored inside the constructor Printable.

7 Likes