Re: [Caml-list] Polymorphic variant typing

[Gilles Dubochet <gilles.dubochet@epfl.ch>]

>> let incr g x = match x with
>>     | `Int i -> `Int (i+1)
>>     | x -> (g x);;
>> Receives type:
>> (([> `Int of int ] as 'a) -> ([> `Int of int ] as 'b)) -> 'a -> 'b
>
>    Now, how about this :
>
> let incr x g = match x with
>   | `Int i -> `Int (i+1)
>   | x -> g x;;
>
>    Doesn't it look like your code ? OCaml 3.08.2 types it as follows :
> val incr : ([> `Int of int ] as 'a) -> ('a -> ([> `Int of int ] as 
> 'b)) -> 'b = <fun>
>
>    This is more like it !
I am afraid I can't agree with you: As far as I can tell, this type 
with the 'x g' version is exactly equivalent to the type I obtained 
with the 'g x' version. If you remember that "... as 'a" is the binding 
of a type variable, it is quite intuitive why.

> incr (`Int 1) (fun (`Int i) -> (`Int (i+1)));;
> - : [> `Int of int ] = `Int 2

> incr (`Float 1.0) (fun x -> match x with (`Float f) -> (`Float (f +. 
> 1.0)) | x -> x);;
> - : [> `Float of float | `Int of int ] = `Float 2.
Yes, but in your case the g function you pass as a parameter has a last 
generic case. This means it has type "([> `Float of float ] as 'a) -> 
'a" which is an "at least" instead of a "at most" variant type. With 
that function it works also with my original 'g x' version. The goal is 
to be able to make this run:
incr (`Float 1.0) (fun x -> match x with (`Float f) -> (`Float (f +. 
1.0)));;
And your solution doesn't more than mine.

Just to make things clear, I am not looking for a workaround to this 
problem. I am rather looking for an explanation about why the mentioned 
type is inferred for this expression. I am developing a type inference 
system for a language with similar variants to O'Caml's polymorphic 
variants. My inference algorithm calculates a different type than 
O'Caml's for a equivalent expression. I try to understand why O'Caml 
does it that way to decide how I should do it. To make it even more 
clear, the type I obtain with my algorithm is (in row variable 
notation): (['a] -> [#int:int | 'b]) -> [#int:int | 'a] -> [#int:int | 
'b]

Voilà, but thanks for the answer anyway,
Cheers,
Gilles.