[Caml-list] Clarification needed: use of "as" in patterns (with GADTs)

[Caml-list] Clarification needed: use of "as" in patterns (with GADTs)

[Sebastien Furic]

  Hello,

  Would someone be kind enough to explain me what's going on with the 
following code:

type empty
and nonempty
type ('a, _) my_list =
   | Nil: ('a, empty) my_list
   | Cons: 'a * ('a, 'b) my_list -> ('a, nonempty) my_list

(* Works fine *)
let rec max = function
   | Cons (x, Nil) -> x
   | Cons (x, Cons (x', xs)) when x <= x' -> max (Cons (x', xs))
   | Cons (x, Cons (_, xs)) -> max (Cons (x, xs))

(* Fails *)
let rec max = function
   | Cons (x, Nil) -> x
   | Cons (x, (Cons (x', _) as xs)) when x <= x' -> max xs
   | Cons (x, Cons (_, xs)) -> max (Cons (x, xs));;

Characters 97-99:
   | Cons (x, (Cons (x', _) as xs)) when x <= x' -> max xs
                                                        ^^
Error: This expression has type ('a, nonempty) my_list
        but an expression was expected of type ('a, nonempty) my_list
        This instance of nonempty is ambiguous:
        it would escape the scope of its equation

  I remember having seen similar issues in the past, involving "as" and 
polymorphic variants (but I can't find it in the archives). Is it the 
same issue? Why does Ocaml need to "break the continuity" of types in 
presence of "as"?
  BTW, what is the recommended way to write the code above (I want to 
avoid having to reconstruct the list)?

  Cheers,

  Sébastien.

Re: [Caml-list] Clarification needed: use of "as" in patterns (with GADTs)

[Jacques Garrigue]

On 2012/10/19, at 23:05, Sebastien Furic <programming.languages@furic.org> wrote:

> Hello,
> 
> Would someone be kind enough to explain me what's going on with the following code:
> 
> type empty
> and nonempty
> type ('a, _) my_list =
>  | Nil: ('a, empty) my_list
>  | Cons: 'a * ('a, 'b) my_list -> ('a, nonempty) my_list
> 
> (* Works fine *)
> let rec max = function
>  | Cons (x, Nil) -> x
>  | Cons (x, Cons (x', xs)) when x <= x' -> max (Cons (x', xs))
>  | Cons (x, Cons (_, xs)) -> max (Cons (x, xs))
> 
> (* Fails *)
> let rec max = function
>  | Cons (x, Nil) -> x
>  | Cons (x, (Cons (x', _) as xs)) when x <= x' -> max xs
>  | Cons (x, Cons (_, xs)) -> max (Cons (x, xs));;
> 
> Characters 97-99:
>  | Cons (x, (Cons (x', _) as xs)) when x <= x' -> max xs
>                                                       ^^
> Error: This expression has type ('a, nonempty) my_list
>       but an expression was expected of type ('a, nonempty) my_list
>       This instance of nonempty is ambiguous:
>       it would escape the scope of its equation
> 
> I remember having seen similar issues in the past, involving "as" and polymorphic variants (but I can't find it in the archives). Is it the same issue? Why does Ocaml need to "break the continuity" of types in presence of "as"?
> BTW, what is the recommended way to write the code above (I want to avoid having to reconstruct the list)?

Actually, this is not the same issue: the problem here is related to ambiguity inference, which in the case of OCaml is required for soundness in presence of GADTs.
What happens here is that you Cons constructor introduces an existential variable, which is immediately forced to nonempty by matching against the nested Cons. However is inferred as using this existential variable.
When typing the recursive call the existential variable is forced to expand to nonempty, but as a result of this expansion it is marked as ambiguous.

When you get such an error message, there is an easy solution: add a type annotation on the faulty expression, using exactly the printed type:

   max (xs : ('a, nonempty) my_list)

This is enough to make this program accepted.

It could be argued that in this case there is no ambiguity, since the existential cannot be exported anyway.
I'll look into that, but you must keep in mind that we must be very careful, as soundness is at stake.

Jacques Garrigue

Re: [Caml-list] Clarification needed: use of "as" in patterns (with GADTs)

[Sebastien Furic]

On 10/20/2012 09:27 AM, Jacques Garrigue wrote:
> Actually, this is not the same issue: the problem here is related to ambiguity inference, which in the case of OCaml is required for soundness in presence of GADTs.
> What happens here is that you Cons constructor introduces an existential variable, which is immediately forced to nonempty by matching against the nested Cons. However is inferred as using this existential variable.
> When typing the recursive call the existential variable is forced to expand to nonempty, but as a result of this expansion it is marked as ambiguous.
>
> When you get such an error message, there is an easy solution: add a type annotation on the faulty expression, using exactly the printed type:
>
>     max (xs : ('a, nonempty) my_list)
>
> This is enough to make this program accepted.
>
> It could be argued that in this case there is no ambiguity, since the existential cannot be exported anyway.
> I'll look into that, but you must keep in mind that we must be very careful, as soundness is at stake.

  Thank you Jacques, for the explanation and for the hint.

  Cheers,

  Sébastien.