From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 287597FAF6 for ; Sat, 22 Nov 2014 13:44:51 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of agarwal1975@gmail.com) identity=pra; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of agarwal1975@gmail.com designates 209.85.212.172 as permitted sender) identity=mailfrom; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f172.google.com) identity=helo; client-ip=209.85.212.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="postmaster@mail-wi0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AiECAKSEcFTRVdSslGdsb2JhbABCGg6DVVkEgwLHLYFshmsCewcWAQEBAQERAQEBAQcLCwkSMIQDAQEDARIRBBkBGx0BAwELBgMCBAcDNAICIQEBEQEFARwGEyKICQEDCQkNOJlGkFI9MYs7gXKDEYphChknDWiFWgEBAQcBAQEBAQEWAQUOjkCCPQeCeYFVBYwkiyWFHYIUgXOOJ4R+GCmEd14qMAGCSgEBAQ X-IPAS-Result: AiECAKSEcFTRVdSslGdsb2JhbABCGg6DVVkEgwLHLYFshmsCewcWAQEBAQERAQEBAQcLCwkSMIQDAQEDARIRBBkBGx0BAwELBgMCBAcDNAICIQEBEQEFARwGEyKICQEDCQkNOJlGkFI9MYs7gXKDEYphChknDWiFWgEBAQcBAQEBAQEWAQUOjkCCPQeCeYFVBYwkiyWFHYIUgXOOJ4R+GCmEd14qMAGCSgEBAQ X-IronPort-AV: E=Sophos;i="5.07,437,1413237600"; d="scan'208";a="90007890" Received: from mail-wi0-f172.google.com ([209.85.212.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Nov 2014 13:44:30 +0100 Received: by mail-wi0-f172.google.com with SMTP id n3so1650410wiv.17 for ; Sat, 22 Nov 2014 04:44:50 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=hxWL5tn52/P4Cn3bOZMOkzp5wOp6iuXgmf99DhaAoBo=; b=Cp9AAuCfIrTKHQhbMvECQ6r/lk6ICKUaGUy/tPWokyryccIJ0xyOELKoaGpLaWthJG xjmIVfAPwR8k2k3eY4ZBbUw0058i9Y2Mn3iPs+b4oXRFyGxYpIfI6bxFshYuIYylxDKD VAMOol8/pMY/aTKEg4G7jDbbXR5Jq7PHBam4M7xVAxcwdL+Sf2V3pqKckzvQbiXcVZbI 24RKB0YlrEiytF8IeguMDw7vKgtl2yeAEShAvr+BcVOlUA9pKhgy1zbTqvz2ZJ/Y6FQ2 QQ0aosjzyre1N349p0QtaCf8qcUnZOXHjEFcqIOPrRAJek4Mz7gHzpKToVEwAbal1jnN UPDQ== X-Received: by 10.194.193.2 with SMTP id hk2mr16516685wjc.40.1416660290245; Sat, 22 Nov 2014 04:44:50 -0800 (PST) MIME-Version: 1.0 Received: by 10.27.5.203 with HTTP; Sat, 22 Nov 2014 04:44:29 -0800 (PST) In-Reply-To: <877fyoi7tb.fsf@study.localdomain> References: <877fyoi7tb.fsf@study.localdomain> From: Ashish Agarwal Date: Sat, 22 Nov 2014 07:44:29 -0500 Message-ID: To: Leo White Cc: Caml List Content-Type: multipart/alternative; boundary=089e0102f8845e1d76050871eda4 Subject: Re: [Caml-list] OR-patterns with GADTs --089e0102f8845e1d76050871eda4 Content-Type: text/plain; charset=UTF-8 Thanks for the link to the Mantis issue. On Fri, Nov 21, 2014 at 4:04 PM, Leo White wrote: > Ashish Agarwal 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 > --089e0102f8845e1d76050871eda4 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Thanks for the link to the Mantis issue.

On Fri, Nov 21, 2014 at 4:0= 4 PM, Leo White <lpw25@cam.ac.uk> wrote:
Ashish Agarwal <agarwal1975@gmail.com> writes= :

> The following works fine:
>
> type foo
> type bar
> type _ t =3D
> | Foo : string -> foo t
> | Bar : string -> bar t
>
> let to_string : type a . a t -> string =3D function
> =C2=A0 | Foo x -> x
> =C2=A0 | Bar x -> x
>
> However, if you try to avoid the redundant code of the two branches, y= ou get a compile error:
>
> let to_string : type a . a t -> string =3D function
> =C2=A0 | Foo x
> =C2=A0 | Bar x -> x
>
> Error: This pattern matches values of type foo t
> =C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was expected which matches va= lues of type a t
> =C2=A0 =C2=A0 =C2=A0 =C2=A0Type 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 GA= DTs 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 a= t
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=3D5736), so hopefully it wil= l be
resolved one day.

Regards,

Leo

--089e0102f8845e1d76050871eda4--