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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id B037F7F20B for ; Mon, 11 Feb 2013 16:31:46 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of sebastien.mondet@gmail.com) identity=pra; client-ip=74.125.82.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sebastien.mondet@gmail.com"; x-sender="sebastien.mondet@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of sebastien.mondet@gmail.com designates 74.125.82.182 as permitted sender) identity=mailfrom; client-ip=74.125.82.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sebastien.mondet@gmail.com"; x-sender="sebastien.mondet@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f182.google.com) identity=helo; client-ip=74.125.82.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="sebastien.mondet@gmail.com"; x-sender="postmaster@mail-we0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgMCAHcNGVFKfVK2jWdsb2JhbAA/Bg6GQKdgiUsBiRgIFg4BAQEBCQkLCRIGI4IfAQEEASMEGQEbEgwDAQsGAwILGh0CAiIBEQEFAQoSBgESEodtAQMJBgyTBo8di2VPgnuDfQoZJwMKWYh8AQUMjVGDHYETA4hmjT6BHY1UFimDal0 X-IPAS-Result: AgMCAHcNGVFKfVK2jWdsb2JhbAA/Bg6GQKdgiUsBiRgIFg4BAQEBCQkLCRIGI4IfAQEEASMEGQEbEgwDAQsGAwILGh0CAiIBEQEFAQoSBgESEodtAQMJBgyTBo8di2VPgnuDfQoZJwMKWYh8AQUMjVGDHYETA4hmjT6BHY1UFimDal0 X-IronPort-AV: E=Sophos;i="4.84,643,1355094000"; d="scan'208";a="2342909" Received: from mail-we0-f182.google.com ([74.125.82.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 Feb 2013 16:31:46 +0100 Received: by mail-we0-f182.google.com with SMTP id t57so4978391wey.41 for ; Mon, 11 Feb 2013 07:31:46 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:mime-version:in-reply-to:references:from:date:message-id :subject:to:content-type; bh=NOZqShR8C7j954Bi/WKxaDAhoOHEqfZEr8gQ5UQUHuo=; b=PPZg3kPy0mV4iZWBJhBB1Q22neQMq5S0Jw5gn4b+dXKhigYdS0oFNibWHM+G0BQpbn aIdG2HF9T0wKD7RN6prisKa6CVE1GH7Hi4xYaHR9iuGXp2UNXY7YRWa/PjeCWtVjLyUQ zsKHjb5Jpm+4qYnhLAzqshI5gXfmFYXMsnNfsCj3e87nicqTasP868kaMI76Me3CUnY8 RHg8/BWuSyp97CPiSY8S79Tp4shh7D69vaoDL2UbMiO7/FEsXAIYlOPhUkrVjdFUy76X C7afSeOpBcqQLIHCJttzhb0MrnWiuw9Id92e+vS78pKWSswiFOG4ZQLakJkj86qGy8uT OPoQ== X-Received: by 10.194.89.167 with SMTP id bp7mr24658991wjb.0.1360596705949; Mon, 11 Feb 2013 07:31:45 -0800 (PST) MIME-Version: 1.0 Received: by 10.194.123.196 with HTTP; Mon, 11 Feb 2013 07:31:25 -0800 (PST) In-Reply-To: References: From: Sebastien Mondet Date: Mon, 11 Feb 2013 10:31:25 -0500 Message-ID: To: "caml-list@inria.fr" , Jacques Garrigue Content-Type: multipart/alternative; boundary=047d7bf10a8657368804d5749bb0 Subject: Re: [Caml-list] Propagating types to pattern-matching --047d7bf10a8657368804d5749bb0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi Jacques I don't know if this directly related, or if it is actually intended, but this looks like a regression to me: With OCaml version 4.00.1+dev2_2012-08-06 (4.00.1+short-types in Opam): # let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;; val f : int -> [> `one | `some | `zero ] =3D # let g x =3D match f x with `one -> 1 | `zero -> 0;; Error: This pattern matches values of type [< `one | `zero ] but a pattern was expected which matches values of type [> `one | `some | `zero ] The first variant type does not allow tag(s) `some which is the nice behavior we were used to, but with OCaml version 4.01.0+dev10-2012-10-16 (a.k.a. 4.01.0dev+short-paths), the error has been downgraded to a warning: # let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;; val f : int -> [> `one | `some | `zero ] =3D # let g x =3D match f x with `one -> 1 | `zero -> 0;; Warning 8: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: `some val g : int -> int =3D Is it intended? Cheers Seb On Tue, Jan 15, 2013 at 12:59 AM, Jacques Garrigue < garrigue@math.nagoya-u.ac.jp> wrote: > Dear Camlers, > > It is a bit unusual, but this message is about changes in trunk. > > As you may be aware from past threads, since the introduction of GADTs > in 4.00, some type information is propagated to pattern-matching, to allow > it to refine types. > More recently, types have started being used to disambiguate constructors > and record fields, which means some more dependency on type information > in pattern-matching. > > However, a weakness of this approach was that propagation was disabled > as soon as a pattern contained polymorphic variants. The reason is that > typing rules for polymorphic variants in patterns and expression are subt= ly > different, and mixing information without care would lose principality. > > At long last I have removed this restriction on the presence of polymorph= ic > variants, but this has some consequences on typing: > > * while type information is now propagated, information about possibly > present constructors still has to be discarded. For instance this means > that > the following code will not be typed as you could expect: > > let f (x : [< `A | `B]) =3D match x with `A -> 1 | _ -> 2;; > val f : [< `A | `B > `A ] -> int > > What happens is that inside pattern-matching, only required constructors > are propagated, which reduces the type of x to [> ] (a polymorphic > variant > type with any constructor=E2=80=A6) > As before, to give an upper bound to the matched type, the type > annotation > must be inside a pattern: > > let f =3D function (`A : [< `A | `B]) -> 1 | _ -> 2;; > val f : [< `A | `B ] -> int =3D > > * the propagation of type information may lead to failure in some cases > that > where typable before: > > type ab =3D [ `A | `B ];; > let f (x : [`A]) =3D match x with #ab -> 1;; > Error: This pattern matches values of type [? `A | `B ] > but a pattern was expected which matches values of type [ > `A ] > The second variant type does not allow tag(s) `B > > During pattern-matching it is not allowed to match on absent type > constructors, > even though the type of the patterns would eventually be [< `A | `B], > which allows > discarding `B. ([? `A | `B] denotes a type obeying the rules of > pattern-matching) > > * for the sake of coherence, even if a type was not propagated because it > was not known when typing a pattern-matching, we are still going to fail > if a > matched constructor appears to be absent after typing the whole functio= n. > (This only applies to propagable types, i.e. polymorphic variant types > that > contain only required constructors) > > In particular the last two points are important, because previously such > uses > would not have triggered even a warning. > > The idea is that allowing propagation of types is more important than > keeping some not really useful corner cases, but if this is of concern > to you, I'm interested in feedback. > > Jacques Garrigue > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs --047d7bf10a8657368804d5749bb0 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Hi Jacques
I don't know if this directly related, or if it is actually = intended, but this looks like a regression to me:


With OCa= ml version 4.00.1+dev2_2012-08-06=C2=A0 (4.00.1+short-types in Opam):

# let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;;
= val f : int -> [> `one | `some | `zero ] =3D <fun>

# let= g x =3D match f x with `one -> 1 | `zero -> 0;;
Error: This patte= rn matches values of type [< `one | `zero ]
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 but a pattern was expected which match= es values of type
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 [>= `one | `some | `zero ]
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 The first v= ariant type does not allow tag(s) `some

which is the nice= behavior we were used to,
but with OCaml version 4.01.0+dev10-2012-10-16=C2=A0 (a.k.a.=C2=A0 4.= 01.0dev+short-paths), the error has been downgraded to a warning:

# let f =3D function 0 -> `zero | 1 -> `one | _ -> `some;;
= val f : int -> [> `one | `some | `zero ] =3D <fun>

# let= g x =3D match f x with `one -> 1 | `zero -> 0;;
Warning 8: this p= attern-matching is not exhaustive.
Here is an example of a value that is not matched:
`some
val g : int = -> int =3D <fun>


Is it intended?

Che= ers
Seb





















On Tue, Jan 15, 2013 at 12:59 AM, Ja= cques Garrigue <garrigue@math.nagoya-u.ac.jp> wro= te:
Dear Camlers,

It is a bit unusual, but this message is about changes in trunk.

As you may be aware from past threads, since the introduction of GADTs
in 4.00, some type information is propagated to pattern-matching, to allow<= br> it to refine types.
More recently, types have started being used to disambiguate constructors and record fields, which means some more dependency on type information
in pattern-matching.

However, a weakness of this approach was that propagation was disabled
as soon as a pattern contained polymorphic variants. The reason is that
typing rules for polymorphic variants in patterns and expression are subtly=
different, and mixing information without care would lose principality.

At long last I have removed this restriction on the presence of polymorphic=
variants, but this has some consequences on typing:

* while type information is now propagated, information about possibly
=C2=A0 present constructors still has to be discarded. For instance this me= ans that
=C2=A0 the following code will not be typed as you could expect:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 let f (x : [< `A | `B]) =3D match x with `A = -> 1 | _ -> 2;;
=C2=A0 =C2=A0 =C2=A0 =C2=A0 val f : [< `A | `B > `A ] -> int

=C2=A0 What happens is that inside pattern-matching, only required construc= tors
=C2=A0 are propagated, which reduces the type of x to [> ] (a polymorphi= c variant
=C2=A0 type with any constructor=E2=80=A6)
=C2=A0 As before, to give an upper bound to the matched type, the type anno= tation
=C2=A0 must be inside a pattern:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 let f =3D function (`A : [< `A | `B]) -> = 1 | _ -> 2;;
=C2=A0 =C2=A0 =C2=A0 =C2=A0 val f : [< `A | `B ] -> int =3D <fun&g= t;

* the propagation of type information may lead to failure in some cases tha= t
=C2=A0 where typable before:

=C2=A0 =C2=A0 =C2=A0 =C2=A0 type ab =3D [ `A | `B ];;
=C2=A0 =C2=A0 =C2=A0 =C2=A0 let f (x : [`A]) =3D match x with #ab -> 1;;=
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Error: This pattern matches values of type [? `= A | `B ]
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0but a pattern was ex= pected which matches values of type [ `A ]
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0The second variant t= ype does not allow tag(s) `B

=C2=A0 During pattern-matching it is not allowed to match on absent type co= nstructors,
=C2=A0 even though the type of the patterns would eventually be [< `A | = `B], which allows
=C2=A0 discarding `B. ([? `A | `B] denotes a type obeying the rules of patt= ern-matching)

* for the sake of coherence, even if a type was not propagated because it =C2=A0 was not known when typing a pattern-matching, we are still going to = fail if a
=C2=A0 matched constructor appears to be absent after typing the whole func= tion.
=C2=A0 (This only applies to propagable types, i.e. polymorphic variant typ= es that
=C2=A0 =C2=A0contain only required constructors)

In particular the last two points are important, because previously such us= es
would not have triggered even a warning.

The idea is that allowing propagation of types is more important than
keeping some not really useful corner cases, but if this is of concern
to you, I'm interested in feedback.

=C2=A0 =C2=A0 =C2=A0 =C2=A0 Jacques Garrigue
--
Caml-list mailing list. =C2=A0Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
<= br>
--047d7bf10a8657368804d5749bb0--