variant filtering

variant filtering

[Manuel Fahndrich]

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)


Status encodes return values that can take a number of different causes,
along with a success case which carries an arbitrary value. Function g tries
to return an int status in the case where f returns success, and the failure
status of f otherwise.

% ocamlc -c status.ml

This expression cannot be coerced to type
  int status = [`Success int|`FailureA|`FailureB|`FailureC];
it has type string status = [`Success string|`FailureA|`FailureB|`FailureC]
but is here used with type int #status as 'a = 'a

The compiler does not filter the Success case out in the default branch of
the compiler, which could tell it to give other the type

  other : [`FailureA | `FailureB | `FailureC ]

which could then be coerced to int status.


I know that the exception type system of Francois Pessaux does a similar
filtering. How hard would it be to add this feature to OCaml?

-Manuel

Re: variant filtering

[Jacques Garrigue]

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>

RE: variant filtering

[Jacques Garrigue]

From: Manuel Fahndrich <maf@microsoft.com>

> yes, I see that one has to be able to capture the row variable and it would
> be part of two different types. The work-around you suggest is fine when the
> number of variant cases is small and known. However, one nice thing about
> polymorphic variants is their openness. Thus, enumerating all the other
> cases is not really an option in many cases.

There are two different problems here. One of expressiveness (all
cases have to be known, clearly variants in ocaml are not as
expressive as in Wallace), and another of conciseness (the need to
explicitely write all cases).

I think that expressiveness is not the main problem. The added
expressive power is in my view too complex to be used in most
programs. And in general open pattern matching on variants is not a
good idea, beacuse it weakens the type checking (typos do not cause
type errors).

There are solutions for the conciseness problem, like allowing one to
write a name of variant type instead of the complete case list:

type failures = [`FailureA | `FailureB | `FailureC]

let g () =
  match f () with
    `Success s -> `Success 1
  | #failures as other -> other

Would it be enough?

Remark also that most examples that would use the extra expressiveness
of explicit row variables can also be rewritten in this formalism:

# let f0 = function
      `SuccessA x -> x
    | `SuccessB x -> x*2;;
val f0 : [<`SuccessA int|`SuccessB int] -> int

With row variables:
# let protect f x =
    match x with
      `FailureA -> -1
    | `FailureB -> -2
    | `FailureC -> -3
    | other -> f other;;
val protect : (['r] -> int) -> [<`FailureA|`FailureB|`FailureC|'r] -> int
# let g = protect f0;;
g : [<`FailureA|`FailureB|`FailureC|`SuccessA int|`SuccessB int] -> int

Without row variables:
# let handler x =
    match x with
      `FailureA -> -1
    | `FailureB -> -2
    | `FailureC -> -3;;
val handler : [<`FailureA|`FailureB|`FailureC] -> int
# let g = function
    | #success as x -> f0 x
    | #failures as x -> handler x;;
g : [<`FailureA|`FailureB|`FailureC|`SuccessA int|`SuccessB int] -> int

As you can see, the main difference is that you have to add some glue
by hand. This is less abstract than only applying a function, but the
advantage is that you stay at a simpler level of reasonning. In
practice I believe you do not get more verbose.

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