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 5DD117EF5E for ; Tue, 26 Jul 2016 18:33:32 +0200 (CEST) IronPort-PHdr: 9a23:s83NYhegtLhEbdxB8LKQm6IglGMj4u6mDksu8pMizoh2WeGdxc+6ZB7h7PlgxGXEQZ/co6odzbGH6+a+AidRvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkb7psMyMKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjMD39DwrRTIUSeI43IdVC1WzksJUED560TTWp7wtGPUrOtm0ynSacTyRLEyHzq47rxgSDfshTcGOT9/+2bS3J9elqVe9T2orQZ+zoqcW4qVOeBzZOuJctoQX2tMWoBKXCxMGI6mR4QKBusFe+1fqt+u9BM1sRKiCFz0V6vUwThSiyqzgPQ3 Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f180.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.180 as permitted sender) identity=mailfrom; client-ip=209.85.223.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-io0-f180.google.com) identity=helo; client-ip=209.85.223.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AyBADlj5dXf7TfVdFEEQmEFXwGpzaGAItCgX0khXkCgTMHORMBAQEBAQEBAREBAQkLCwkXMYIyBAESghQBBRIRBBkBGxILAQMMBgULDQICCR0CAiIBEQEFAQoSBhMSEId0AQMXDi2dQoEyPjGLO4FqgloFhDIKGScDClSDOgEBAQEBAQQBAQEBAQEBGAIGEHGFKYRNhAcSgyiCWgWGWAyHMYscgWCEOIhjgWxOhz2FSIc3hHaCORIegQ8fAYJDHYFoIDIBiEgBAQE X-IPAS-Result: A0AyBADlj5dXf7TfVdFEEQmEFXwGpzaGAItCgX0khXkCgTMHORMBAQEBAQEBAREBAQkLCwkXMYIyBAESghQBBRIRBBkBGxILAQMMBgULDQICCR0CAiIBEQEFAQoSBhMSEId0AQMXDi2dQoEyPjGLO4FqgloFhDIKGScDClSDOgEBAQEBAQQBAQEBAQEBGAIGEHGFKYRNhAcSgyiCWgWGWAyHMYscgWCEOIhjgWxOhz2FSIc3hHaCORIegQ8fAYJDHYFoIDIBiEgBAQE X-IronPort-AV: E=Sophos;i="5.28,425,1464645600"; d="scan'208";a="228031644" Received: from mail-io0-f180.google.com ([209.85.223.180]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 Jul 2016 18:33:31 +0200 Received: by mail-io0-f180.google.com with SMTP id 38so29329781iol.0 for ; Tue, 26 Jul 2016 09:33:31 -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; bh=Pnkw0W7qLQ+VKwmBBDvEqXUPZ4ZVSpOl9ROjRl+nmXQ=; b=h+sQXanNNqzcpFgKeKhLyC2gZKVFIEV7yA7N2ZkD8DjWE0pZI9GX5XF0fyPZ5+oj8R yMExWuyTO/Pr45bXa80xF3FYTqvkrW5cgHyB9h8HImfZQcKj9+1QqIu4qTZg4y+KWzVy ++iUtJ4e1+O2x2Q83KqXRNM7jnLPApAflXUqqZGGIs11YcOmprkXj+u1UptJBxUZqYwp YeA2NpU07D21LBa3lmsI64gx140RvBz4AWDKzl/ynFWs9522VZyn2ZBsD8Au45HMmCei dF6cMaGJ1Y2gvp8pxbl5NwtIB1C4w7KLWeZ/HMnDjmmyTQQxs8eNoPNY9qXhrp7TpSuZ TRtQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=Pnkw0W7qLQ+VKwmBBDvEqXUPZ4ZVSpOl9ROjRl+nmXQ=; b=ZfYB8WQUx1MBN4I6SsN5aM2u/Z/KCk3LeFYhN6E1cFqc1GxfGc5OMvuFY2ynF/zs5F Lxx3Mm+/dT0JSCR451s98hAsfMCU1ssljTuomxQI6YUAG/gy9Kq9EbEQa6xDtfOy2msw KSSzTdhzUrbCfv+Vy5qPrAbPUAWWLjGJ3FfyjajqwGy1kTY+T0urRTyHduLhH9wkgJE1 MZVU5dDjhJilB7U8M3K3Ynw530Uax+OJ85x9HUvaiZEa9BqlD4XIf68r15k75ZvFQVRz 00QSJub53sDT0GV3XaIcMvGqOx+5FSvQ8NnPQt0JaMOpH+585cuh25421/53/AuLfAHQ BnTw== X-Gm-Message-State: AEkoouujj0ir9taK4JeC62gxw3Vf4vxRsJg1egQEeK/6R7DgcMTvWmBg0MnXYsoFgeNTPWDSYgjZfZEqz0KlCw== X-Received: by 10.107.169.40 with SMTP id s40mr26530368ioe.19.1469550809464; Tue, 26 Jul 2016 09:33:29 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.20.67 with HTTP; Tue, 26 Jul 2016 09:32:50 -0700 (PDT) In-Reply-To: <14e4dd61-7ff6-fdef-c103-a33c4f728bd9@lexifi.com> References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> <1469525797.2529112.676963937.25E14FD6@webmail.messagingengine.com> <14e4dd61-7ff6-fdef-c103-a33c4f728bd9@lexifi.com> From: Gabriel Scherer Date: Tue, 26 Jul 2016 12:32:50 -0400 Message-ID: To: Alain Frisch Cc: Leo White , caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] exception Foo = Bar.Baz I would see some use in being able to rename variant constructors, see MPR#7102: Ability to re-export a variant definition with renamed constructors? http://caml.inria.fr/mantis/view.php?id=7102 On Tue, Jul 26, 2016 at 12:27 PM, Alain Frisch wrote: > Not strictly related to this discussion, but I've been wondering whether > allowing to change the name of exception/extension constructors while > rebinding is a good idea. For regular constructors, this is not allowed, > and disallowing them for exception/extension as well would give some useful > information to the compiler: two constructors with different names cannot be > equal. This could be used in particular to compile pattern matching more > efficiently by first dispatching on the constructor name (with optimized > string equality that we now have) or on its hash (stored in the constructor > slot). Efficient compilation of pattern matching is perhaps not critical > for exceptions, but with extensible sum types in general, this might be more > important. > > So: do people see some use in being able to rename extension constructors? > > > Alain > > > > On 26/07/2016 14:37, Gabriel Scherer wrote: >> >> To elaborate a bit on your comment, Leo, the analogous situation I >> think is more the declaration >> >> module F (X : S) : sig type t = Foo end = struct type t = Foo end >> module N = F(M) >> >> that indeeds generates the signature >> >> module N : sig type t = F(M).t = Foo end >> >> Variant declaration are also generative (two distinct declarations are >> incompatible), but in a different sense than exceptions: identity of >> type identifiers relies on static equality of module paths, while >> identity of exception constructors is the dynamic moment of their >> evaluation -- same for extension constructors of extensible variant >> types, for which similarly equations cannot be exposed in signatures. >> >> Performing equational reasoning on exception constructors would >> suggest a change in language semantics, where type-compatible modules >> would also share their exception constructors. It is very unclear that >> changing this would be a good idea (in particular wrt. compatibility), >> but one could argue that the mismatch today between type identities >> and value identities in applicative functors is also a problem. That >> relates to Andreas Rossberg's proposal of enforced purity for >> applicative functors at ML 2012, although the main argument was that >> creating private impure state while exposing type equalities could >> break abstraction. >> >> For curiosity only, below is an example of such a mismatch between the >> two forms of generativity: >> >> module type S = sig >> type t >> exception Bot >> val something : unit -> t >> val ignore : (unit -> t) -> unit >> (* invariant: >> ignore something = () *) >> end >> >> module M = struct end >> module F (M : sig end) = struct >> type t >> exception Bot >> let something () = raise Bot >> let ignore something = >> try something () with Bot -> () >> end >> >> module N1 = F(M) >> module N2 = F(M) >> >> let () = N1.ignore N1.something >> let () = N2.ignore N2.something >> >> let () = N1.ignore N2.something (* invariant-breaking *) >> >> >> On Tue, Jul 26, 2016 at 5:36 AM, Leo White wrote: >>>> >>>> I think it would be nice for users that only read .mli files to know >>>> equalities between exceptions, for example if they want to reason on >>>> exhaustiveness of exception handling clauses with respect to a given >>>> (informal) exception specification. >>> >>> >>> I think this is more difficult than it appears. If you track equations >>> on exceptions then you need to make those equations behave properly with >>> respect to the various module operations. For example, you would need: >>> >>> module M : sig exception E end = ... >>> >>> module N = M >>> >>> to end up with N having (a subtype of): >>> >>> sig exception E = M.E end >>> >>> This gets tricky when you have applicative functors. For OCaml's other >>> equations (i.e. types, modules, module types) the following code: >>> >>> module F (X : S) : sig type t end = ... >>> >>> module M : S = ... >>> >>> module N = F(M) >>> >>> gives N the type: >>> >>> module N : sig type t = F(M).t end >>> >>> So you would expect the same to happen with exceptions: >>> >>> module F (X : S) : sig exception E end = ... >>> >>> module M : S = ... >>> >>> module N : sig exception E = F(M).E = F(M) >>> >>> Unfortunately exception declarations are generative, so this equation is >>> "unsound". So either exception equations would need to be handled >>> completely differently from the other equations, or exception >>> definitions would need to be banned from applicative functors. >>> >>> This is quite a lot of effort to go to for maintaining information that >>> is not providing any direct guarantees about program behavior. It is >>> also not particularly clear to me how materially different it is from >>> ordinary values: it would be nice to expose when they were aliases in >>> their types sometimes, but it does not really seem worth the cost. >>> >>> Regards, >>> >>> Leo >>> >>> -- >>> 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 >> >> >