On Tue, Feb 15, 2005 at 09:28:52PM +0000, Gilles Dubochet wrote:
> Hello everyone,
> 
> The following O'Caml expression:
> 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
> 
> Why? I am quite astonished. I would have expected a type more like:
> ([> ] -> [> ]) -> [> `Int of int ] -> [> `Int of int ]
>
> or in Wand or Rémy-like row variable notation with which I am a little 
> more comfortable (I am not exactly sure the preceding type is correct 
> in the 'at leat - at most' notation of O'Caml):
> ([ 'a ] -> [ 'b ]) -> [ `Int of int | 'a ] -> [ `Int of int | 'b ]
> 
> Could anyone be kind enough to give me some clues about where to look 
> at to find an explanation or even better, explain me what is going on? 
> I am particularly puzzled by the fact that the g function's *argument* 
> type is 'at least `Int of int'. This rejects the following code which 
> seems intuitively correct:
> incr (function `Float f -> `Float (f+.1.));;

We know that 'incr' can take a [> `Int of int] for 'x', since it matches
is.  The only way to know that it isn't going to call 'g' with one of these
would be to do a flow analysis of the code.  The type system is not based
on this type of analysis, but is determined statically.

The polymorphic types are not really dynamic types.  A particular type used
in a given call will have a specific type, and in this instance, it must
always contain [> `Int of int].

Dave