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

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

[Goswin von Brederlow]

Hi,

I have a functor that boxes a GADT type into an universal container.
But then the problem is how to get the type back out again.
Specifically I want to pass the data to a polymorphic function that
doesn't care what type it gets since it will pattern match the GADT to
determine the right type.

But, because the argument is a GADT, ocaml complains after unboxing
the type would escape its scope (see call_unboxed below). One can only
call an universal function with the unboxed data and only records (and
objects) can have universal functions.

Problem is that I would like to keep the implementation of the helper
record abstract and only provide a constructor (helper function
below). But the constructor needs an universal function and function
argument are only polymorphic (less general).

A) why is a polymorphic function less general here?

The print function is good enough for List.iter below or for
constructing a helper but not indirectly via "M.helper fn".

Why are function arguments less general than their original function?

B) is there some way around this I'm not seeing?

MfG
	Goswin

--

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

[Goswin von Brederlow]

Somehow the example code got lost:

module M = struct
  type _ t = Int : int -> int t | Float : float -> float t
  let print : type a . a t -> unit = function
    | Int i -> Printf.printf "%d\n" i
    | Float f -> Printf.printf "%f\n" f
  (* should be abstract *)
  type box = Box : 'a t -> box
  let box t = Box t

  (*
  let call_unboxed fn (Box t) = fn t
  Error: This expression has type a#0 t but an expression was expected of type
         a#0 t
       The type constructor a#0 would escape its scope
  *)

  (* should be abstract *)
  type 'a helper = { fn : 'b . 'b t -> 'a }

  (*
  let helper fn = { fn }
  Error: This field value has type 'c t -> 'd which is less general than
         'b. 'b t -> 'a
  *)

  let call helper (Box t) = helper.fn t
end  

open M
let t = [box (Int 1); box (Float 2.0)]  

(* Works but is not possible if box is abstract *)
let () = List.iter (function Box x -> print x) t

(* Use conversion helper to call unboxed values with a function *)
let h = { fn = print }
let () = List.iter (call h) t

MfG
	Goswin

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

[Jeremy Yallop]

On 7 January 2015 at 13:50, Goswin von Brederlow <goswin-v-b@web.de> wrote:
> Why are function arguments less general than their original function?

Polymorphic arguments complicate type checking and make type inference
impossible, so OCaml doesn't allow them.

> B) is there some way around this I'm not seeing?

I don't think that there's any way of passing polymorphic arguments
that works out simpler than using a record.

Of course, in your simple example code it's possible to eliminate the
GADT altogether, which would also eliminate the need for polymorphic
arguments.  Perhaps GADTs play a more essential role in your real
code, though.

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 1592 bytes --]

Parametric polymorphic values in OCaml's type system can be thought of as
"choose an assignment of the variables in this type, and you can use this
value with that monomorphic type". But there's no monomorphic type that
lets 'helper' do the right thing, so you actually need something more
expressive than ordinary polymorphic types.

In Haskell there's higher-rank polymorphism, which in this case would look
something like 'helper :: (forall a. T a -> b) -> Helper b', so that you
could only pass sufficiently-polymorphic arguments to helper. However, as
Jeremy said, there's a lot of added complexity involved.

On 7 January 2015 at 17:26, Jeremy Yallop <yallop@gmail.com> wrote:

> On 7 January 2015 at 13:50, Goswin von Brederlow <goswin-v-b@web.de>
> wrote:
> > Why are function arguments less general than their original function?
>
> Polymorphic arguments complicate type checking and make type inference
> impossible, so OCaml doesn't allow them.
>
> > B) is there some way around this I'm not seeing?
>
> I don't think that there's any way of passing polymorphic arguments
> that works out simpler than using a record.
>
> Of course, in your simple example code it's possible to eliminate the
> GADT altogether, which would also eliminate the need for polymorphic
> arguments.  Perhaps GADTs play a more essential role in your real
> code, though.
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

[-- Attachment #2: Type: text/html, Size: 2399 bytes --]

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

[Goswin von Brederlow]

On Thu, Jan 08, 2015 at 09:45:47AM +0000, Ben Millwood wrote:
> Parametric polymorphic values in OCaml's type system can be thought of as
> "choose an assignment of the variables in this type, and you can use this
> value with that monomorphic type". But there's no monomorphic type that
> lets 'helper' do the right thing, so you actually need something more
> expressive than ordinary polymorphic types.
> 
> In Haskell there's higher-rank polymorphism, which in this case would look
> something like 'helper :: (forall a. T a -> b) -> Helper b', so that you
> could only pass sufficiently-polymorphic arguments to helper. However, as
> Jeremy said, there's a lot of added complexity involved.

In ocaml that is 'a . 'a -> 'b, or for GADTS: type a . a -> 'b.
The problem is the former is only allowed in records and objects, not
for function arguments and the later is only for annotating code and
not for signatures.


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.

> On 7 January 2015 at 17:26, Jeremy Yallop <yallop@gmail.com> wrote:
> 
> > On 7 January 2015 at 13:50, Goswin von Brederlow <goswin-v-b@web.de>
> > wrote:
> > > Why are function arguments less general than their original function?
> >
> > Polymorphic arguments complicate type checking and make type inference
> > impossible, so OCaml doesn't allow them.
> >
> > > B) is there some way around this I'm not seeing?
> >
> > I don't think that there's any way of passing polymorphic arguments
> > that works out simpler than using a record.
> >
> > Of course, in your simple example code it's possible to eliminate the
> > GADT altogether, which would also eliminate the need for polymorphic
> > arguments.  Perhaps GADTs play a more essential role in your real
> > code, though.

The real use case has a GADT as input for a functor. The functor
defines the boxing, an equality and unbox_with_equal operation and
that helper record. Actually I have a few flavours of the same for
different input types: type 'a t, type ('a, 'b) t and GADTs with
detached witness: type 'a key + type 'a value and so on.

I wish I could make a generic helper record with

    type ('b, 'c) helper = { fn : 'a 'b -> 'c }

*sigh*

MfG
	Goswin

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

[Leo White]

> 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. For example, compare this
example using polymorphic methods:

    let f (x : < m: 'a. 'a -> 'a >) =
      let poly =
        if true then x
        else object method m : 'a. 'a -> 'a = id end
      in
      let mono =
        if true then x#m
        else (fun x -> x + 1)
      in
        (poly, mono)

with this example using proper higher-rank types:

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

Using objects with polymorphic methods we can trivially see that the
first use of `x` is not instantiated whilst the second use of `x` is
instantiated because the first uses the object itself whilst the second
uses the method `m`.

With higher-rank polymorphism, we must infer this information. I don't
think this can be done in a principal way, without adding complexity to
the type langauge (see MLF), so there would need to be some additional
type annotations.

Regards,

Leo

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

[Jacques Garrigue]

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

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

[Goswin von Brederlow]

On Thu, Jan 08, 2015 at 04:25:49PM +0000, 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. For example, compare this
> example using polymorphic methods:
> 
>     let f (x : < m: 'a. 'a -> 'a >) =
>       let poly =
>         if true then x
>         else object method m : 'a. 'a -> 'a = id end
>       in
>       let mono =
>         if true then x#m
                       ^^^ 'a . 'a -> 'a
>         else (fun x -> x + 1)
                ^^^^^^^^^^^^^^ int -> int
>       in
>         (poly, mono)
>
> with this example using proper higher-rank types:
> 
>     let f (x : 'a. 'a -> 'a) =
>       let poly =
>         if true then x
>         else id
>       in
>       let mono =
>         if true then x
                       ^ 'a . 'a -> 'a
>         else (fun x -> x + 1)
                ^^^^^^^^^^^^^^ int -> int
>       in
>         (poly, mono)

> Using objects with polymorphic methods we can trivially see that the
> first use of `x` is not instantiated whilst the second use of `x` is
> instantiated because the first uses the object itself whilst the second
> uses the method `m`.
> 
> With higher-rank polymorphism, we must infer this information. I don't
> think this can be done in a principal way, without adding complexity to
> the type langauge (see MLF), so there would need to be some additional
> type annotations.

I don't see anything to infere there. Only thing I see is that in the
case of mono the universal function has to be unified with a single
type function. But 'a . 'a -> 'a should unify with int -> int
resulting in int -> int without problems.

I see no difference between the record and the plain case. The record
only adds a boxing around the type. It doesn't make the type any
easier to infer or unify for me.

MfG
	Goswin

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

[Goswin von Brederlow]

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

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

[Leo White]

> I don't see anything to infere there. Only thing I see is that in the
> case of mono the universal function has to be unified with a single
> type function. But 'a . 'a -> 'a should unify with int -> int
> resulting in int -> int without problems.

'a. 'a -> 'a cannot unify with int -> int. If it did then 'a. 'a -> 'a
wouldn't be polymorphic: it could not be used as both int -> int and
float -> float. Instead 'a. 'a -> 'a must be instantiated to 'b -> 'b
which can then be unified with int -> int. It is the descision whether
or not to perform this instantiation that needs to be infered.

To understand the full range of issues associated with higher-rank and
impredicative polymorphism I suggest reading the relevant literature
(e.g. "MLF: raising ML to the power of system F", "Semi-explicit
first-class polymorphism for ML", "Flexible types: robust type inference
for first-class polymorphism", "Boxy types: inference for higher-rank
types and impredicativity", ...).

Regards,

Leo

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

[Goswin von Brederlow]

On Sat, Jan 10, 2015 at 06:49:31PM +0000, Leo White wrote:
> > I don't see anything to infere there. Only thing I see is that in the
> > case of mono the universal function has to be unified with a single
> > type function. But 'a . 'a -> 'a should unify with int -> int
> > resulting in int -> int without problems.
> 
> 'a. 'a -> 'a cannot unify with int -> int. If it did then 'a. 'a -> 'a
> wouldn't be polymorphic: it could not be used as both int -> int and
> float -> float. Instead 'a. 'a -> 'a must be instantiated to 'b -> 'b
> which can then be unified with int -> int. It is the descision whether
> or not to perform this instantiation that needs to be infered.
> 
> To understand the full range of issues associated with higher-rank and
> impredicative polymorphism I suggest reading the relevant literature
> (e.g. "MLF: raising ML to the power of system F", "Semi-explicit
> first-class polymorphism for ML", "Flexible types: robust type inference
> for first-class polymorphism", "Boxy types: inference for higher-rank
> types and impredicativity", ...).
> 
> Regards,
> 
> Leo

I acknowledge that I'm weak on the theory here but from the example
the rules seems to be pretty simple:

    When trying to unify a universal function with a polymorphic or
    monomorphic function first instantiate.

As said I don't expect ocaml to infer what functions are universal.
That can be annotated. So the question isn't if we can infer from the
mono case wether the function is universal or monomorphic. The
function must already be annotated as universal. Dropping the
universality to allow unification with other types seems to be
straight forward though.

In laymans terms: A function 'a . 'a -> 'a can always be used where 'b
-> 'b (or in this case int -> int) is expected. That doesn't change
the type of the function itself though.

MfG
	Goswin