OCaml 5.5 Polymorphic functions as function arguments

Learning
1

I have been trying to remove a use of a single field polymorphic record using OCaml 5.5 polymorphic functions as function arguments.

While I can see the feature being useful in some restricted cases. I didn’t succeed to get rid of my use. For example in:

type observer = { observe : 'a. (unit -> 'a) -> 'a }
let blind = { observe = (fun f -> f ()) }

module Observe : sig
  val run : ?observer:observer -> (unit -> 'a) -> 'a
end = struct
  let run ?(observer = blind) f = observer.observe f
end

I would have liked to simply remove the field:

type observer = 'a. unit -> 'a -> 'a

But that’s not possible I have to reveal the 'a and quantify all over the place when I use observer arguments. First that’s rather noisy, second it doesn’t seem to work with optional arguments. This code fails with:

type 'a observer = (unit -> 'a) -> 'a
let blind f = f ()

module Observe : sig
  val run : ?observer:('a. 'a observer) -> (unit -> 'a) -> 'a
end = struct
  let run ?(observer = blind) f = observer f
end

File "poly/poly.ml", line 4, characters 22-39:
4 |   val run : ?observer:('a. 'a observer) -> (unit -> 'a) -> 'a
                          ^^^^^^^^^^^^^^^^^
Error: Optional parameter observer cannot be polymorphic

Did I miss something or is that a limitation we are going to have for the foreseeable future?

2

My understanding is that this is a hard limitation (but typing experts will confirm). Basically, optional arguments are sugar for arguments of type 'a option, so you are asking to instantiate 'a at a polymorphic type, something like ('b. unit -> 'b -> 'b) option which is not really supported in any general way in OCaml’s type system.

Cheers,
Nicolas

3

Polymorphic types with an explicit universal quantification are still second-class citizen in the type system after the polymorphic parameters change.

My summary would be that polymorphic parameters remove the need to define a record with a polymorphic field which is used once in one function. However, as soon as the code is using values with such type as a first-class citizens, it is still required to define a record definition. This is at least partially for theoretical reasons: the record boxing and unboxing make it explicit which view of the type one should adopt. As an illustration of this double vision issue, in

type id = { f: 'a. 'a -> 'a }
let id x = x
let f a = a {f=id} 0 "0"
let g a = a id 0 "0"

the function f and g have distinct requirement over the function a.

From this point of view, polymorphic parameters is identifying that for a function, there is a relatively intuitive choice on when to box (during function call) and unbox (in the function body) the parameters of the function.

4

Before I forget to mention it, there are valid usability points: it might be nice to be able to define abbreviation for polymorphic type or to have a form of polymorphic optional parameters.
These changes would possibly help to reduce the number of polymorphic records in library API.

But my impression is also that both features have potentially sharp usability edges that would require some careful design to circumvent.