From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3HMTCgU028600 for ; Wed, 18 Apr 2012 00:29:12 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArABAATujU/RVdQ2kGdsb2JhbABEDoVYq1AIIgEBAQEHCw0HFAQjggkBAQEDARICDwQZARsdAQMBCwYDAgs3AgIiAREBBQEcBjWHXQEDBgWbMwqLUk6Cc4RvChknDVeIdgEFC49AgRgElW+OVj2DU1M X-IronPort-AV: E=Sophos;i="4.75,438,1330902000"; d="scan'208";a="154478932" Received: from mail-vb0-f54.google.com ([209.85.212.54]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 18 Apr 2012 00:29:06 +0200 Received: by vbmv11 with SMTP id v11so8674959vbm.27 for ; Tue, 17 Apr 2012 15:29:05 -0700 (PDT) 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=FZ0X183NabmxYOLCrNMOZ+R+dFaetMIP2EPImVmgrY8=; b=OQXEIqX7FK4W5eoewIpuM7gnlM9CjL4pQMlyIN3pZDfndFMK7rSPz8TXLUZsimDGPK Lig1QJe1alXch0WaemkPkY1NvcW1zrAx9AaKMs/qIaemGvWK6vJNAjlMMixNsGnZ4edD T5WJefe5at0hPbs8L6XuFtSKA63jZ3cbaFLu1D6O8OABo8Gfc+mWk3Y6Q5TUTh6bZbbf ukDsWFaxTuoQKfoxqCuvJKpm2YOeY5rcmsQxVPC0LOMcKdsSZOeU8+sscoVyzVangCnU j8+HWR+DF2pyP12hhpu8GtseYal/U13Z6OnO3EAKFQF2DKZDjIuLworxLMl+IerR4QLv Q93w== Received: by 10.52.17.82 with SMTP id m18mr7196223vdd.89.1334701745206; Tue, 17 Apr 2012 15:29:05 -0700 (PDT) MIME-Version: 1.0 Received: by 10.52.37.137 with HTTP; Tue, 17 Apr 2012 15:28:44 -0700 (PDT) In-Reply-To: <08857D21-9495-4332-8BB9-315368430349@math.nagoya-u.ac.jp> References: <08857D21-9495-4332-8BB9-315368430349@math.nagoya-u.ac.jp> From: Sebastien Mondet Date: Tue, 17 Apr 2012 18:28:44 -0400 Message-ID: To: Jacques Garrigue Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=bcaec50405d66776fc04bde77762 Subject: Re: [Caml-list] Potential Feature Request: "Remove poly-variants from match-with statements" --bcaec50405d66776fc04bde77762 Content-Type: text/plain; charset=UTF-8 > > > This has been asked for repeatedly. > Sorry, I swear I have searched through Mantis for this :-/ > I admit this could be useful in some cases but there are difficulties. > > One first question is, what are you really asking for? > > If you just want to be able to omit the pattern before "as", > then it is probably doable (not easy, as in your example one has > to detect that while the return type of how_much is open, other cases > cannot happen), but would not add any expressivity. > > As there is already a nice form of "at least" exhaustiveness check, I had the impression that enough information is available at some point (?) let three_is_a_lot_3 x = match how_much x with | `Three -> `A_lot | `Two | `A_lot as any -> any;; ^^^^^^ Error: This pattern matches values of type [< `A_lot | `Three | `Two ] but a pattern was expected which matches values of type [> `A_lot | `One | `Three | `Two ] The first variant type does not allow tag(s) `One If you want the real thing, i.e. the ability to have functions that "skim" > a variant > type, then this gets much more difficult. > > After a few years trying to follow this list, I start to have an idea of what it means when J. Garrigue says that something is difficult :) So, no, the "real thing" is really not worth the complexity. > let remove_Three = function > `Three -> failwith "Three" > | any -> any > > What kind of type should we give to this function? > Probably something like: > > [`Three | 'a] -> [ 'a ] > > Note here that 'a is a new kind of type variable, that can only > be used as a polymorphic variant row variable. > Such type systems have been studied in the literature, and I think > there is even an Haskell extension doing that, but this can easily > get complicated. > > OCaml avoids introducing such new type variables by requiring > that if two types share the same row variable they must be identical. > In particular this rules out the above type. Removing this restriction > would be a major design change. > > Jacques Garrigue --bcaec50405d66776fc04bde77762 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

This has been asked for repeatedly.

Sorry, I swear I have searched through Mantis for this :-/
=C2=A0
I admit this could be useful in some cases but there are difficulties.

One first question is, what are you really asking for?

If you just want to be able to omit the pattern before "as",
then it is probably doable (not easy, as in your example one has
to detect that while the return type of how_much is open, other cases
cannot happen), but would not add any expressivity.


As there is already a nice form of =C2= =A0"at least" exhaustiveness check, I had the
impressio= n that enough information is available at some point (?)


let three_is_a_lot_3 x =3D
=C2=A0 match = how_much x with
=C2=A0 | `Three -> `A_lot
=C2=A0 | `= Two | `A_lot as any -> any;;
=C2=A0 =C2=A0 =C2=A0 ^^^^^^
=
Error: This pattern matches values of type [< `A_lot | `Three | `Tw= o ]
=C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was expected which matches va= lues of type
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0[> `A_lot | `On= e | `Three | `Two ]
=C2=A0 =C2=A0 =C2=A0 =C2=A0The first variant = type does not allow tag(s) `One



If you want the real thing, i.e. the ability to have functions that "s= kim" a variant
type, then this gets much more difficult.


After a few years trying to follow thi= s list, I start to have an idea of what it
means when J. Garrigue= says that something is difficult =C2=A0:)

So, no,= the "real thing" is really not worth the complexity.

=C2=A0
=C2=A0let remove_Three =3D function
=C2=A0 =C2=A0 =C2=A0`Three -> failwith "Three"
=C2=A0 | any -> any

What kind of type should we give to this function?
Probably something like:

=C2=A0[`Three | 'a] =C2=A0-> [ 'a ]

Note here that 'a is a new kind of type variable, that can only
be used as a polymorphic variant row variable.
Such type systems have been studied in the literature, and I think
there is even an Haskell extension doing that, but this can easily
get complicated.

OCaml avoids introducing such new type variables by requiring
that if two types share the same row variable they must be identical.
In particular this rules out the above type. Removing this restriction
would be a major design change.

=C2=A0 =C2=A0 =C2=A0 =C2=A0Jacques Garrigue

--bcaec50405d66776fc04bde77762--