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

[Jonathan Protzenko <jonathan.protzenko@gmail.com>]

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>
>
>