Type of explicitly polymorphic function

Learning
1

In reading the paper “Lightweight higher-kinded polymorphism”, I found some some syntax that I found useful but hadn’t known about before, specifically record fields with explicitly polymorphic functions.

Here’s a contrived example:

(** An enumeration of conversions from ['a] to ['b] *)
type ('a, 'b) conv = 
  | Int_to_float : (int, float) conv
  | Int_to_string : (int, string) conv
  | Float_to_int : (float, int) conv

(** A function that, for all conversions on ['a], returns a value of ['b] *)  
type 'a f = {
  f: 'b. 'a -> ('a, 'b) conv -> 'b 
}

let ex : int f = 
  let f = fun (type b) i (conv : (int, b) conv) : b ->
    match conv with
    | Int_to_float -> float_of_int i
    | Int_to_string -> string_of_int i
  in
  {
    f
  }
  
(** Doesn't compile since [float] is less general than ['b] *)
let bad_ex : int f = 
  let f = fun i (conv : (int, float) conv) : float ->
    match conv with
    | Int_to_float -> float_of_int i
  in
  {
    f
  }

This does exactly what I want it to, and I can add [@@unboxed] to type f to reduce the runtime representation to just the function.

However, my question is why isn’t

type 'a f = 'b. 'a -> ('a, 'b) conv -> 'b

or even

type 'a f = F : 'b. 'a -> ('a, 'b) conv -> 'b

valid syntax?

The first case might make sense to me because f is just an alias, but the second case is less clear. I looked in the manual and it seems like poly-typexpr only appears in record fields, which lines up with the behavior I see, but I can’t find an answer as to why that’s the case. This obviously isn’t the end of the world, I was mostly just curious.

Thanks!

1 Like
2

Maybe you know it, but this syntax is allowed at the let-binding level when you don’t use the “function arguments” syntax sugar: let ex: 'b. 'a -> ('a, 'b) conv = .... (It wasn’t always there, the record-field variant predates it IIRC.)

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.

6 Likes
4

Note that you can use inline records to have universal quantification in constructor arguments.

type 'a f = F of { f : 'b. 'a -> ('a, 'b) conv -> 'b }
1 Like
5

Wow, thanks @octachron for such a detailed response! I think this part

answers the core of my question.

As an aside, I’m not super clear on this, though:

Maybe this particular example is hampering my understanding, but I would have assumed that the same type printable without the 'elt. would exhibit the same behavior. Is there a particular construction that your version allows that the other does not?

Also thanks @thierry-martinez, I hadn’t considered that inline records would have the same syntax.

6

In case of GADT constructors, the typechecker infers the universal quantifications by itself if you don’t do it by hand. In other words, the typechecker reads

Printable: ('elt -> string) * 'elt -> printable

as

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

because otherwise the type variable 'elt would be unbound in the definition of the constructor, which is not allowed.

1 Like
7

Ah ok that squares with my understanding. Thanks again!