Re: [Caml-list] Potential Feature Request: "Remove poly-variants from match-with statements"

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2012/04/17, at 0:24, Sebastien Mondet wrote:

> I don't know if it is theoretically sound or possible, but
> it would be helpful, if the typing of match-with statements with polymorphic
> variants was able to remove one or more variants from the "catch-all" cases
> 
> In the following code, it would mean that three_is_a_lot would be typed like
> three_is_a_lot_2 without having to write all the cases.
> 
> 
> # let how_much = function
>   | 1 -> `One
>   | 2 -> `Two
>   | 3 -> `Three
>   | n -> `A_lot;;
> 
>         val how_much : int -> [> `A_lot | `One | `Three | `Two ] = <fun>
> 
> # let three_is_a_lot x =
>   match how_much x with
>   | `Three -> `A_lot
>   | any -> any;;
> 
>       val three_is_a_lot : int -> [> `A_lot | `One | `Three | `Two ] = <fun>
> 
> # let three_is_a_lot_2 x =
>   match how_much x with
>   | `Three -> `A_lot
>   | `One | `Two | `A_lot as any -> any;;
> 
>       val three_is_a_lot_2 : int -> [> `A_lot | `One | `Two ] = <fun>
> 
> 
> The practical use-case for us is that we use polymorphic variants to encode "semantic" errors in an Error/Result monad.

This has been asked for repeatedly.
I admit this could be useful in some cases but there are difficulties.

One first question is, what are you really asking for?

If you just want to be able to omit the pattern before "as",
then it is probably doable (not easy, as in your example one has
to detect that while the return type of how_much is open, other cases
cannot happen), but would not add any expressivity.

If you want the real thing, i.e. the ability to have functions that "skim" a variant
type, then this gets much more difficult.

  let remove_Three = function
      `Three -> failwith "Three"
   | any -> any

What kind of type should we give to this function?
Probably something like:

  [`Three | 'a]  -> [ 'a ]

Note here that 'a is a new kind of type variable, that can only
be used as a polymorphic variant row variable.
Such type systems have been studied in the literature, and I think
there is even an Haskell extension doing that, but this can easily
get complicated.

OCaml avoids introducing such new type variables by requiring
that if two types share the same row variable they must be identical.
In particular this rules out the above type. Removing this restriction
would be a major design change.

	Jacques Garrigue