Re: [Caml-list] Problem with universal functions in a module

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/01/09 01:25, Leo White wrote:
> 
>> I don't see how there can be much added complexity involved. The
>> higher-rank polymorphism is already allowed in records and objects so
>> the type system knows how to deal with them. At least when they are
>> annotated. I wouldn't need ocaml to infere those types.
> 
> It is possible that higher-rank types would not add too much complexity
> to OCaml.
> 
> However, there is an important difference between that and the
> higher-rank polymorphism provided by records and objects: whether to
> instantiate a type or not must be inferred.

Actually the formal system for polymorphic methods use a notion of boxing/unboxing
of first-class polymorphic values. It would be trivial to add it to ocaml's type system.
There was not much demand originally, but with the introduction of GADTs it becomes
more interesting.

   let f (x : ['a. 'a -> 'a]) =
     let poly =
       if true then x
       else (Poly (fun x -> x) : ['a. 'a -> 'a])
     in
     let mono =
       let Poly x = x in
       if true then x
       else (fun x -> x + 1)
     in
       (poly, mono)

Note also that first-class modules already provide another flexible approach to first-class
polymorphism, and while you need to define a package type, equality of package
types is structural since 4.02.

   module type T = sig val f : 'a -> 'a end

   let f (module X : T) =
     let poly : (module T) =
       if true then (module X)
       else (module struct let f x = x end)
     in
     let mono =
       if true then X.f
       else (fun x -> x + 1)
     in
       (poly, mono)

As you can see here, the only slightly heavy part is the syntax for building modules.

Jacques Garrigue