[Caml-list] Defeating the value restriction

[Caml-list] Defeating the value restriction

[John Carr]

Can I rewrite this function to have the type I requested
instead of failing type checking?

let f : ('a * 'a -> 'a) -> int * bool = fun x -> x (0,1), x (true,false)

I assume the type error is caused by the value restriction.
The parameter (x) becomes monomorphic when applied, so it
can not be applied to both types (int*int) and (bool*bool).

A top level syntactic function

let x : ('a * 'a -> 'a) = fun (a,b) -> a

retains its original, generalized type under similar circumstances.

My real example that fails type checking is more complicated.
I believe the root cause is the same.

    --John Carr (jfc@mit.edu)

Re: [Caml-list] Defeating the value restriction

[Jeremy Yallop]

On 26 October 2011 21:07, John Carr <jfc@mit.edu> wrote:
> Can I rewrite this function to have the type I requested
> instead of failing type checking?

Yes: see "How to write a function with polymorphic arguments?" in the Caml FAQ:

http://caml.inria.fr/resources/doc/faq/core.en.html#polymorphic-arguments

Re: [Caml-list] Defeating the value restriction

[Jacques Garrigue]

On 2011/10/27, at 5:07, John Carr wrote:

> Can I rewrite this function to have the type I requested
> instead of failing type checking?
> 
> let f : ('a * 'a -> 'a) -> int * bool = fun x -> x (0,1), x (true,false)
> 
> I assume the type error is caused by the value restriction.
> The parameter (x) becomes monomorphic when applied, so it
> can not be applied to both types (int*int) and (bool*bool).

Just a comment that this completely unrelated to the value restriction.
ML type inference simply doesn't support polymorphism in function
arguments.

As Jeremy Yallop already answered, OCaml supports this by wrapping
the argument in various things. The most recent way to do that
(and intuitively related with the toplevel behaviour) is to use a first-class
module:

module type S = sig val c : 'a * 'a -> 'a end
let f x = let module X = (val x : S) in X.x (0,1) , X.x (true, false)

Jacques Garrigue