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

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

[Sebastien Mondet]

[-- Attachment #1: Type: text/plain, Size: 1033 bytes --]

Hi

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.

What does the list think?

Cheers,
Sebastien

[-- Attachment #2: Type: text/html, Size: 1662 bytes --]

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

[Jacques Garrigue]

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

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

[Sebastien Mondet]

[-- Attachment #1: Type: text/plain, Size: 2084 bytes --]

>
>
> This has been asked for repeatedly.
>

Sorry, I swear I have searched through Mantis for this :-/


> 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.
>
>
As there is already a nice form of  "at least" exhaustiveness check, I had
the
impression that enough information is available at some point (?)


let three_is_a_lot_3 x =
  match how_much x with
  | `Three -> `A_lot
  | `Two | `A_lot as any -> any;;
      ^^^^^^
Error: This pattern matches values of type [< `A_lot | `Three | `Two ]
       but a pattern was expected which matches values of type
         [> `A_lot | `One | `Three | `Two ]
       The first variant type does not allow tag(s) `One



If you want the real thing, i.e. the ability to have functions that "skim"
> a variant
> type, then this gets much more difficult.
>
>
After a few years trying to follow this list, I start to have an idea of
what it
means when J. Garrigue says that something is difficult  :)

So, no, the "real thing" is really not worth the complexity.



>  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

[-- Attachment #2: Type: text/html, Size: 3365 bytes --]