Re: [Caml-list] Auto-closing polymorphic variants ?

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

On Wed, 20 Feb 2008, David Teller wrote:

>   Dear list,
>
> There are still a number of things I don't quite understand about
> polymorphic variants. For instance, polymorphic variants seem to be open
> by default.
>
> # let a = `a ;;
> val a : [> `a ] = `a
> # let b = `b ;;
> val b : [> `b ] = `b
>
> I can only assume this was done to keep the property that in
>  if ... then some_p else some_q
> it must be possible to unify the types of some_p and some_q, which
> wouldn't be possible with closed types.
>
> However, as mentioned in the discussion regarding exceptionless error
> management, in conjunction with wildcards, sanity checks become
> irrelevant, which may lead to hard-to-track errors, e.g.
>
> # let safe_div x = function
>  | 0. -> `Div_by_zero
>  | y -> `Ok (x /. y) ;;
> val safe_div : float -> float -> [> `Div_by_zero | `Ok of float ] = <fun>
>
> # let idiv x y =
>  match safe_div (float_of_int x) (float_of_int y) with
>  | `Success x -> x
>  | _          -> nan ;;
> val idiv : int -> int -> float = <fun>
>
>
> Here, because of the wildcard, ocamlc didn't notice that we wrote
> `Success where no such variant could happen.
>
> Now, it seems to me that this wouldn't a real problem if we had a way to
> auto-close safe_div during the match, i.e. something like
>
> # let idiv x y =
>  match close (safe_div (float_of_int x) (float_of_int y)) with
>  | `Success x -> x
>     ^^^^^^^^^
>  | _          -> nan ;;
>
> This pattern matches values of type [> `Success of 'a ]
> but is here used to match values of type [ `Div_by_zero | `Ok of
> float ]
> The second variant type does not allow tag(s) `Success
>
> Of course, we could do that by manually closing the type of safe_div,
> but this would essentially mean duplicating information.
>
> Either
> # let idiv x y =
>  match (safe_div (float_of_int x) (float_of_int y) :
>         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>  [ `Success of float | `Div_by_zero ] ) with
>  | `Success x -> x
>  | _          -> nan ;;
> This expression has type [> `Div_by_zero | `Ok of float ]
> but is here used with type [ `Div_by_zero | `Success of float ]
> The second variant type does not allow tag(s) `Ok
>
> or
> # let idiv x y =
>    match(safe_div (float_of_int x) (float_of_int y) :
>    [`Div_by_zero | `Ok of float]) with
>    | `Success x -> x
>      ^^^^^^^^^^^
>    | _          -> nan ;;
> This pattern matches values of type [> `Success of 'a ]
> but is here used to match values of type [ `Div_by_zero | `Ok of
> float ]
> The second variant type does not allow tag(s) `Success
>
> Unfortunately, I can't seem to find anything comparable to that "close"
> operator in the documentation, nor any design pattern which would attain
> the same effect.
>
> Does anyone have ideas on this subject ?

Yes: don't use wildcards mixed with concrete cases:

Good: function `A -> ... | `B -> ...
Good: function _ -> ...

Bad: function `A -> ... | _ -> ...



Martin

--
http://wink.com/profile/mjambon
http://martin.jambon.free.fr