This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Polymorphic variant typing
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2005-02-16 (00:37) From: Jacques Garrigue Subject: Re: [Caml-list] Polymorphic variant typing
```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);;
>
> (([> `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

```