Re: [Caml-list] Initialization of a polymorphic field in a record

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> I really did think there was a way of doing that with the newer (type t)
> features, so I'm hoping for someone to correct my example above :).

I don't think there is. Indeed, as you remarked, the type required for
`make1` to work would use higher-order polymorphism (a quantification
inside the left type of an arrow), which does not exist in the
Hindley-Milner (HM) type system (because it couldn't be completely
inferred), and is not supported by OCaml in the general case. The only
place where polymorphism can happen is on the function type as a whole
(usual HM prenex polymorphism), or in record fields and object methods
-- but then there is no inference.

So as you suggest, `make1` have to take a structure that already has
this first-class polymorphism baked in : a record or an object (which
has the advantage of needing no type declaration), or possibly a
first-class module (I did not check).

  let make1 (f : < poly : 'a . 'a -> bool >) = { check = fun x -> f#poly x }

On Tue, Jul 3, 2012 at 2:33 PM, Jonathan Protzenko
<jonathan.protzenko@gmail.com> wrote:
> The type you would like to assign to make1 is:
>
> make1: (∀x. x → bool) → t
>
> However, as far I understand, the type-system of OCaml introduces the ∀
> quantifier in front of the function, namely:
>
> make1: ∀x. (x → bool) → t
>
> This means by the time you enter your make1 function, the f function has
> already lost its polymorphic type, since x has been "opened" already.
>
> I tried to eta-convert, but that doesn't work either:
>
> let make2 f = let g: 'b. 'b -> bool = fun (type t) (x: t) -> f x in { check
> = g };;
> Error: This expression has type t but an expression was expected of type t
>       The type constructor t would escape its scope
>
> although I *did* think that would be legal.
>
> The only way I know of achieving that is by making make1 take a parameter of
> type t, that is, leave it up to the caller to wrap the function in a record
> with type t so as to keep the polymorphic nature of the function...
>
> I really did think there was a way of doing that with the newer (type t)
> features, so I'm hoping for someone to correct my example above :).
>
> Cheers,
>
> jonathan
>
>
> On Tue 03 Jul 2012 02:25:36 PM CEST, Philippe Veber wrote:
>>
>> Hi,
>>
>> how about that:
>>
>> # type t = { check : 'a. 'a -> bool };;
>> type t = { check : 'a. 'a -> bool; }
>>
>> # let return_true : 'a. 'a -> bool = fun _ -> true;;
>> val return_true : 'a -> bool = <fun>
>>
>> # let make1 () = { check = return_true; };;
>> val make1 : unit -> t = <fun>
>>
>> cheers,
>>   Philippe.
>>
>>
>> 2012/7/3 Jean-Louis Giavitto <jean-louis.giavitto@ircam.fr
>> <mailto:jean-louis.giavitto@ircam.fr>>
>>
>>
>>     Hello.
>>
>>     I am trying to build a record with a polymorphic field and I am
>>     unable to initialize this field. The problem can be summarized as
>>     follow. The following definitions works well:
>>
>>        type t = { check : 'a. 'a -> bool }
>>
>>        let return_true _ = true
>>
>>        let make1 () = { check = return_true; }
>>
>>     But this definition raises an error:
>>
>>        let make2 f = { check = f; }
>>
>>     with the message:
>>
>>       Error: This field value has type 'a -> bool which is less
>>     general than
>>              'b. 'b -> bool
>>
>>     Note that
>>
>>        let return_false _ = true
>>
>>        let make3 c = { check = if c then return_false else return_true; }
>>
>>     is working but that
>>
>>        let g c = if c then return_false else return_true
>>        let make4 c = { check = g c; }
>>
>>     raises the same error message. Making explicit the argument of
>>     make does not helps:
>>
>>       let make5 f = { check = f; }
>>       in make5 return_true
>>
>>     (same error message). And making explicit the type of make does
>>     not help neither:
>>
>>       let make6 : 'a. ('a -> bool) -> t
>>       = function f -> { check = f; }
>>
>>     (same error message).
>>
>>
>>
>>     Do you have an idea how I can specify a function similar to make
>>     to buid a record of type t?
>>
>>     In the real life, the argument f will be the result of a
>>     computation and instead of a simple signature 'a -> bool, I must
>>     deal with a signature
>>
>>        'a 'b. (('b) #SomeClass as 'a) * 'b -> bool
>>
>>
>>     Thanks for your advice,
>>     Jean-Louis Giavitto.
>>
>>     --
>>     Caml-list mailing list.  Subscription management and archives:
>>     https://sympa-roc.inria.fr/__wws/info/caml-list
>>     <https://sympa-roc.inria.fr/wws/info/caml-list>
>>     Beginner's list: http://groups.yahoo.com/group/__ocaml_beginners
>>     <http://groups.yahoo.com/group/ocaml_beginners>
>>     Bug reports: http://caml.inria.fr/bin/caml-__bugs
>>     <http://caml.inria.fr/bin/caml-bugs>
>>
>>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>