English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
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 <garrigue@m...>
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);;
> 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

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.


Jacques Garrigue