Re: [Caml-list] Polymorphic variant typing

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Gilles Dubochet <dubochet@urbanet.ch>

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

The reason is simple enough: variants in ocaml are not based on Remy's
rows, but on a type system with kinded variables, more in Ohori's style.
This is described in detail in "Simple type inference for structural
polymorphism", which you can find at
  http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/

The main reason for this choice is avoiding making rows explicit,
i.e. having a multi-sorted type algebra. Note also that ocaml object
types, while originally based on Remy's system, are hiding their
row-variables, and can be described in the same formalism.

> 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.));;

Pragmatic reasons for this choice are given in Section 3 of
  "Typing deep pattern-matching in presence of polymorphic variants"
which you can find at the same place.

Cheers,

Jacques Garrigue