Re: [Caml-list] polymorphic variant

[Martin Jambon <martin.jambon@ens-lyon.org>]

On Thu, 20 Sep 2007, Christophe Raffalli wrote:

> Can someone explain to me why the two following functions are typed so
> differently:
>
> ---------------
>        Objective Caml version 3.10.0
>
> # let f = function
>      `T, y -> y
>    | x, `T -> x
>    | `F, `F -> `F
>    | `F, _ -> `F
> ;;
> Warning U: this match case is unused.
> val f : [ `F | `T ] * [ `F | `T ] -> [ `F | `T ] = <fun>
>
> # let g = function
>    `T, y -> y
>  | x, `T -> `F
>  | `F, `F -> `F
>  | `F, _ -> `F
> ;;
> val g : [< `F | `T ] * ([> `F | `T ] as 'a) -> 'a = <fun>
>
> -------
>
> The decision to close the second column seems to depend upon the right hand side of the pattern, which seems excluded by Jacques Garrigue's paper about deep pattern matching ... According to this paper, the second function is strangely typed. What is implemented in OCaml ?


The difference lies in the pattern: if you use a catch-all such as a 
lowercase identifier, the type of the bound variable will be the same as 
the argument that you are matching.

In the following, x and y will have the same type:
match x with
   y -> y


but here x and y have possibly different types:

match x with
  (`A | `B) as y -> y

(x could be of type [ `A ], which is incompatible with the type of y)


It can be conveniently replaced by the following shortcut:

type ab = [ `A | `B ]

match x with
  #ab as y -> y


Martin

--
http://martin.jambon.free.fr