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

[Goswin von Brederlow <goswin-v-b@web.de>]

On Fri, Jan 09, 2015 at 10:02:30AM +0900, Jacques Garrigue wrote:
> 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

Modules don't improve anything here. The problem is still that you
can't hide the implementation of the boxing:

# let make : ('a -> 'a) -> (module T) = function
  | fn -> (module struct let f = fn end);;
Error: Signature mismatch:
       Modules do not match: sig val f : '_a -> '_a end is not included in T
       Values do not match:
         val f : '_a -> '_a
       is not included in
         val f : 'a -> 'a

And you need different modules for different kind of types. Like 'a t,
('a, 'b) t, ... So I think modules are just as unflexible as objects
and records here.

MfG
	Goswin