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 6BAF97EF5E for ; Tue, 26 Jul 2016 18:28:00 +0200 (CEST) IronPort-PHdr: 9a23:aN/V+RS4Xq+wM2xU6Dme6OcN1dpsv+yvbD5Q0YIujvd0So/mwa65ZhON2/xhgRfzUJnB7Loc0qyN4vimBzdLsMnJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mj6bsoNaCPE1hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFm0vb2rgHORhej4X4VU2Ne0kYZQluN0BavcZ77qCr3sqJG0ymXJ8DsBeQ7UD647qpvDgTjiCodOiQR/2Tei8g2h6Ve9lbpgxF4i7HUYZ2YfK56c6T1ecsFHzcHWMtNAX9vGIS5OqILBusHdchCrpL2pxNapB+3BA/qCvnu0TRIrnv7zaw00qIqFgSQj19oJM4HrHmB9Ia9D6wVS+3gifSRwA== Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=alain.frisch@lexifi.com; spf=None smtp.mailfrom=alain.frisch@lexifi.com; spf=None smtp.helo=postmaster@mx20.yaziba.net Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain.frisch@lexifi.com) identity=pra; client-ip=85.233.204.164; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain.frisch@lexifi.com"; x-sender="alain.frisch@lexifi.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of alain.frisch@lexifi.com) identity=mailfrom; client-ip=85.233.204.164; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain.frisch@lexifi.com"; x-sender="alain.frisch@lexifi.com"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mx20.yaziba.net) identity=helo; client-ip=85.233.204.164; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="alain.frisch@lexifi.com"; x-sender="postmaster@mx20.yaziba.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0D9BADxjpdXh6TM6VVVCYQVKlKnPJM/JIV5AoE6PBABAQEBAQEBAREBAQEKCwkJGS+CMgQBEoIUAQUjBBE2CxALGAICCR0CAkUSBgEMBgIBAQ6IBQMbCqtIiUUDhBgBAQEBAQEEAQEBAQEBAQEfgQGFKYF4glWEBxIngwGCWgEEhlgMhzGLHIFghDiIY4FsTocaI4VIjC2DdgI1gi4SC4FObIhJAQEB X-IPAS-Result: A0D9BADxjpdXh6TM6VVVCYQVKlKnPJM/JIV5AoE6PBABAQEBAQEBAREBAQEKCwkJGS+CMgQBEoIUAQUjBBE2CxALGAICCR0CAkUSBgEMBgIBAQ6IBQMbCqtIiUUDhBgBAQEBAQEEAQEBAQEBAQEfgQGFKYF4glWEBxIngwGCWgEEhlgMhzGLHIFghDiIY4FsTocaI4VIjC2DdgI1gi4SC4FObIhJAQEB X-IronPort-AV: E=Sophos;i="5.28,425,1464645600"; d="scan'208";a="186014481" Received: from mx20.yaziba.net ([85.233.204.164]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 26 Jul 2016 18:27:59 +0200 Received: from mta10.int.yaziba.net (mta10.int.yaziba.net [10.4.20.30]) (using TLSv1 with cipher ADH-AES256-SHA (256/256 bits)) (No client certificate requested) by mx20.yaziba.net (mx10.yaziba.net) with ESMTPS id EAC531A7ACC; Tue, 26 Jul 2016 18:27:57 +0200 (CEST) Received: from mta10.int.yaziba.net (localhost [127.0.0.1]) by mta10.int.yaziba.net (Postfix) with ESMTPS id 12C59CA73C; Tue, 26 Jul 2016 18:27:58 +0200 (CEST) Received: from localhost (localhost [127.0.0.1]) by mta10.int.yaziba.net (Postfix) with ESMTP id EE8C3CA75A; Tue, 26 Jul 2016 18:27:57 +0200 (CEST) X-Virus-Scanned: amavisd-new at mta10.int.yaziba.net Received: from mta10.int.yaziba.net ([127.0.0.1]) by localhost (mta10.int.yaziba.net [127.0.0.1]) (amavisd-new, port 10026) with ESMTP id 1f5ZCVNfglfM; Tue, 26 Jul 2016 18:27:57 +0200 (CEST) Received: from [10.0.210.146] (unknown [185.23.92.144]) by mta10.int.yaziba.net (Postfix) with ESMTPSA id AEF13CA73C; Tue, 26 Jul 2016 18:27:57 +0200 (CEST) To: Gabriel Scherer , Leo White References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> <1469525797.2529112.676963937.25E14FD6@webmail.messagingengine.com> Cc: caml users From: Alain Frisch Message-ID: <14e4dd61-7ff6-fdef-c103-a33c4f728bd9@lexifi.com> Date: Tue, 26 Jul 2016 18:27:54 +0200 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-DRWEB-SCAN: ok X-VRSPAM-SCORE: -51 X-VRSPAM-STATE: legit X-VRSPAM-CAUSE: gggruggvucftvghtrhhoucdtuddrfeeltddrieefgddutdduucetufdoteggodetrfcurfhrohhfihhlvgemucggtfgfnhhsuhgsshgtrhhisggvpdgjtegkkfeuteenuceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrghinhculdegledmnecujfgurhepuffvfhfhkffffgggjggtgfesthejredttdefjeenucfhrhhomheptehlrghinhcuhfhrihhstghhuceorghlrghinhdrfhhrihhstghhsehlvgigihhfihdrtghomheqnecuffhomhgrihhnpehinhhrihgrrdhfrhdphigrhhhoohdrtghomhenucfkphepudekhedrvdefrdelvddrudeggeenucfrrghrrghmpehmohguvgepshhmthhpohhuth X-VRSPAM-EXTCAUSE: mhhouggvpehsmhhtphhouhht Subject: Re: [Caml-list] exception Foo = Bar.Baz 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 >