[Caml-list] OR-patterns with GADTs

[Caml-list] OR-patterns with GADTs

[Ashish Agarwal]

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

The following works fine:

type foo
type bar
type _ t =
| Foo : string -> foo t
| Bar : string -> bar t

let to_string : type a . a t -> string = function
  | Foo x -> x
  | Bar x -> x


However, if you try to avoid the redundant code of the two branches, you
get a compile error:

let to_string : type a . a t -> string = function
  | Foo x
  | Bar x -> x

Error: This pattern matches values of type foo t
       but a pattern was expected which matches values of type a t
       Type foo is not compatible with type a

Is there a real reason for this?

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

Re: [Caml-list] OR-patterns with GADTs

[Leo White]

Ashish Agarwal <agarwal1975@gmail.com> writes:

> The following works fine:
>
> type foo
> type bar
> type _ t =
> | Foo : string -> foo t
> | Bar : string -> bar t
>
> let to_string : type a . a t -> string = function
>   | Foo x -> x
>   | Bar x -> x
>
> However, if you try to avoid the redundant code of the two branches, you get a compile error:
>
> let to_string : type a . a t -> string = function
>   | Foo x
>   | Bar x -> x
>
> Error: This pattern matches values of type foo t
>        but a pattern was expected which matches values of type a t
>        Type foo is not compatible with type a
>
> Is there a real reason for this?

I think the reason is that full support for or-patterns with GADTs is
difficult. Matching on one GADT pattern generates one set of equations
and matching on the other generates a different set of equations and you
then need to check the body under the (parts of the) equations that are
in both patterns. There might be something simpler than full support
which wouldn't be that hard, but its not clear what that would be, so at
the moment things just fail if you use GADTs in an or-pattern.

There is a Mantis issue for it
(http://caml.inria.fr/mantis/view.php?id=5736), so hopefully it will be
resolved one day.

Regards,

Leo

Re: [Caml-list] OR-patterns with GADTs

[Ashish Agarwal]

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

Thanks for the link to the Mantis issue.

On Fri, Nov 21, 2014 at 4:04 PM, Leo White <lpw25@cam.ac.uk> wrote:

> Ashish Agarwal <agarwal1975@gmail.com> writes:
>
> > The following works fine:
> >
> > type foo
> > type bar
> > type _ t =
> > | Foo : string -> foo t
> > | Bar : string -> bar t
> >
> > let to_string : type a . a t -> string = function
> >   | Foo x -> x
> >   | Bar x -> x
> >
> > However, if you try to avoid the redundant code of the two branches, you
> get a compile error:
> >
> > let to_string : type a . a t -> string = function
> >   | Foo x
> >   | Bar x -> x
> >
> > Error: This pattern matches values of type foo t
> >        but a pattern was expected which matches values of type a t
> >        Type foo is not compatible with type a
> >
> > Is there a real reason for this?
>
> I think the reason is that full support for or-patterns with GADTs is
> difficult. Matching on one GADT pattern generates one set of equations
> and matching on the other generates a different set of equations and you
> then need to check the body under the (parts of the) equations that are
> in both patterns. There might be something simpler than full support
> which wouldn't be that hard, but its not clear what that would be, so at
> the moment things just fail if you use GADTs in an or-pattern.
>
> There is a Mantis issue for it
> (http://caml.inria.fr/mantis/view.php?id=5736), so hopefully it will be
> resolved one day.
>
> Regards,
>
> Leo
>

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