Re: variant filtering

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

From: Manuel Fahndrich <maf@microsoft.com>

> Variants are great, but pattern matching should filter used cases in the
> default branch. This seems to be a dual of the record modification problem
> we've seen some time ago on this list.
> 
> Consider the following code:
> 
> 
> type 'a status = [`Success 'a | `FailureA | `FailureB | `FailureC ];;
> 
> let f () = (`Success "Yeah" :> string status)
> 
> 
> let g () =
>    match f () with
>      `Success s -> `Success 1
>    | other      -> (other :> int status)

Indeed the above code will cause a type error.
However, with variants there is a workaround:

let g () =
  match f () with
    `Success s -> `Success 1
  | `FailureA | `FailureB | `FailureC as other -> other

Compared to Pottier's Wallace (or Pessaux's exceptions), you have to
explicitely give the list of the cases matched by other. Still this
will produce the same code as your example would have (had it be
typable).

Originally, this was a design choice to avoid having to handle
specifically row variables: now you cannot name them, but only the
variant type containing them. This means that two different variant
types cannot share the same row variable, as would be needed in your
example.

With the conjunctive typing in ocaml 2.99 variants, there may also be
new theoretical problems for an approach where rows can be shared. I
did not really check.

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>