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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id B35407F1E1 for ; Tue, 15 Jan 2013 06:59:40 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap4EAAjv9FCFBoIF/2dsb2JhbAA+BoY6t1BzgkYBBRwBNzIDCxoDX4grilqaB2sBgkSBEAKGDIcCB4Egi3KDBjVhiGKNLIVril6DBA X-IronPort-AV: E=Sophos;i="4.84,471,1355094000"; d="scan'208";a="189920857" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 15 Jan 2013 06:59:38 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 296926360 for ; Tue, 15 Jan 2013 14:59:36 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id D6BF73962; Tue, 15 Jan 2013 14:59:35 +0900 (JST) DomainKey-Signature: h=Received:From:Content-Type:Content-Transfer-Encoding:Subject:Date:To:Message-Id:Mime-Version:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from [192.168.0.41] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id BD06F24C5; Tue, 15 Jan 2013 14:59:35 +0900 (JST) From: Jacques Garrigue Content-Type: text/plain; charset=iso-2022-jp Content-Transfer-Encoding: quoted-printable Date: Tue, 15 Jan 2013 14:59:34 +0900 To: OCaml List Message-Id: Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) X-Mailer: Apple Mail (2.1499) Subject: [Caml-list] Propagating types to pattern-matching 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 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 present constructors still has to be discarded. For instance this means t= hat 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=1B$B!D=1B(B) 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 constru= ctors, even though the type of the patterns would eventually be [< `A | `B], whi= ch allows discarding `B. ([? `A | `B] denotes a type obeying the rules of pattern-m= atching) * 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 function. (This only applies to propagable types, i.e. polymorphic variant types th= at contain 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. Jacques Garrigue=