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: -- (:) From: David Brown Subject: Re: [Caml-list] Polymorphic variant typing
```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);;
>
> (([> `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

```