Auto-closing polymorphic variants ?

Auto-closing polymorphic variants ?

[David Teller]

   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 ?

Thanks,
 David

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

[Martin Jambon]

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

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

[David Teller]

Well, sure, but that's a bit unsatisfying, as it's a policy which the
type-checker cannot check.

Cheers,
 David

On Thu, 2008-02-21 at 01:29 +0100, Martin Jambon wrote:
> > 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 -> ... | _ -> ...

-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act
brings liquidations. 

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

[Jacques Garrigue]

From: David Teller <David.Teller@univ-orleans.fr>

>  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.

Indeed, having only closed polymorphic variants type would be
self-defeating. You would need to use explicit subtyping for every
single value you want to put in a type with more than one
constructor! Exactly the kind of things polymorphic variants are there
to avoid.

> 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.

Indeed, while this code is probably incorrect, it is probably safe.

> 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

The trouble is that, in the presence of type inference, the semantics
of close is not clear. Namely, type inference requires all typing
operators to be monotonic. That is, if e1 has a type more general than
e2, then you should be able to use e1 wherever e2 can be used.
Now, with open polymorphic variants, a type with less tags is more
general than a type with more types. But your operator would close it,
preventing it from being used with more tags, thus breaking
monotonicity.

Here is an example where closing would be bad:

let f x =
  if x = `A then 1 else
  match close x with
    `B -> 2
  | _ -> 0
in f `B

Of course this is not what you had in mind, but it's hard to get good
properties at the typing level.

This does not mean that we can try nothing. For instance we could
introduce a warning when a pattern matching adds a new tag to a
polymorphic input. The idea is that since the input is polymorphic, it
is sure that it will never actually contain extra tags.
And thanks to the relaxed value restriction, the result of safe_div
would be just polymorphic enough to trigger the warning, while example
like the above, by being not polymorphic, would not trigger it.
But this would not be easy to implement...

> 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

Your two examples reflect the existence of two ways to avoid the
problem: either use a closed subject, or a closed pattern matching.
The problem only arises when both are open.
I don't think that type annotations on the pattern-matching itself are
the good solution for this.
It is better to either define safe_div as returning a closed variant
type (writing interfaces in ocaml _is not_ code duplication, it is
code specification!) or not use wild cards in pattern matchings
on open polymorphic variants.

> 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.

You could use the two "design patterns" above. The first one might be
called the "specify types" pattern, and is good when you don't need
extensibility through polymorphism (which is needed only in rare
cases), while the second one is the "no open doors" pattern (when you
need extensibility, but are afraid of risks). Any approach that
emphasises completely implicit extensibity is going to be risky...

Jacques Garrigue

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

[David Teller]

On Thu, 2008-02-21 at 10:54 +0900, Jacques Garrigue wrote:
> This does not mean that we can try nothing. For instance we could
> introduce a warning when a pattern matching adds a new tag to a
> polymorphic input. The idea is that since the input is polymorphic, it
> is sure that it will never actually contain extra tags.
> And thanks to the relaxed value restriction, the result of safe_div
> would be just polymorphic enough to trigger the warning, while example
> like the above, by being not polymorphic, would not trigger it.
> But this would not be easy to implement...

Sounds like a good idea. How hard would that be ?

> > Of course, we could do that by manually closing the type of safe_div,
> > but this would essentially mean duplicating information.
> > 

> It is better to either define safe_div as returning a closed variant
> type (writing interfaces in ocaml _is not_ code duplication, it is
> code specification!) or not use wild cards in pattern matchings
> on open polymorphic variants.

I agree that, whenever module barriers are crossed, interfaces become
specifications. However, as soon as you're remaining inside one module,
it's nice to be more lightweight and just let inference handle
everything. This is where a warning (or something like a "close"
operator) would come in handy.

Cheers,
 David
-- 
David Teller
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations.