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 D14107EF5E for ; Tue, 26 Jul 2016 14:38:34 +0200 (CEST) IronPort-PHdr: 9a23:HqlVzxXomjter9ymNOCcEei2Dz7V8LGtZVwlr6E/grcLSJyIuqrYZhKBt8tkgFKBZ4jH8fUM07OQ6PG4HzJbqsrR+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0pcaYP1UArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoXzNNbSajxY4g/SLVZCnxmbzF0t4XXskznQAzH2XsdTmhexh5FBCDB9A6gA9H3vzes5cRn3yzPEsT8V7E5XXyZ5KdmUhLywHMIPjQj8WzTzNd7jK9BrQiJqBl2woqSa4aQYqktNpjBdM8XEDISFv1aUDZMV9/tYg== Authentication-Results: mail3-smtp-sop.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-it0-f52.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.52; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.52 as permitted sender) identity=mailfrom; client-ip=209.85.214.52; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-it0-f52.google.com) identity=helo; client-ip=209.85.214.52; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-it0-f52.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CgAQDBWJdXhjTWVdFVCYQVfAanMoYAi0KBfSSFeQKBLwc4FAEBAQEBAQEBEQEBAQgLCwkZL4IyBAOCJAEFEhEEGQEbEgsBAwwGBQsNAgIJHQICIgERAQUBChIGExIQh3QBAxcOnAiBMj4xizuBaoJaBYQtChknAwpUgzoBAQEBAQUBAQEBARoCBhBxhSmETYQHEoMogloBBIZYDJJNgWCEOIhjgWxOhz2FSIwtgjkSHoEPHoJXgXMgMohJAQEB X-IPAS-Result: A0CgAQDBWJdXhjTWVdFVCYQVfAanMoYAi0KBfSSFeQKBLwc4FAEBAQEBAQEBEQEBAQgLCwkZL4IyBAOCJAEFEhEEGQEbEgsBAwwGBQsNAgIJHQICIgERAQUBChIGExIQh3QBAxcOnAiBMj4xizuBaoJaBYQtChknAwpUgzoBAQEBAQUBAQEBARoCBhBxhSmETYQHEoMogloBBIZYDJJNgWCEOIhjgWxOhz2FSIwtgjkSHoEPHoJXgXMgMohJAQEB X-IronPort-AV: E=Sophos;i="5.28,424,1464645600"; d="scan'208";a="185986193" Received: from mail-it0-f52.google.com ([209.85.214.52]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 Jul 2016 14:38:33 +0200 Received: by mail-it0-f52.google.com with SMTP id u186so110076212ita.0 for ; Tue, 26 Jul 2016 05:38:33 -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=L+2YYxcUAoRtGKHAaBgFc7YjnT5eoTTb2XDGaVU/s5M=; b=SCZTcOGNT6Ie6vUb0YuFXduW5qZoPGTb8lG4JI6I2SIBYFJuaiw3we3LbxvvYjR1+Y trMMbwBN9ZZelR/7APK3d7cvamps7XKXGBR0shKcxZsRTYdbjyKk2JmqiWw4oMeUuZtz l5kbHjH8MM1ha5xsoRMWqDKxdervBuz6tYwy0V/CzjaQNunNrB/zQOzmkxBXTETkKs/S Tcz1tyjf7b65DCRxK1lGw3k3R7fST0qAeJZJGJAb1H9bgfo/9tqvgymo1Q99f07IliYm kxtOGYfbkctOuXIW/znTCd7MiDrblACdS1WetUF3ArNr4rUA9kap+BA0JIURbe6yY5hD jucg== 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=L+2YYxcUAoRtGKHAaBgFc7YjnT5eoTTb2XDGaVU/s5M=; b=H7NZ8iEE8i2a9K4AqHRVpxjyNosVU4F/ZIqwNdxLMXlTRttTCE/DFJrtSag46PTGhR dlgdVT87MNVQVBB35VJkI/Qa5uuk/UGcwtSxQc7dJSRbImB2dmaQeMtrsi9GhbI6yojB U+fXlmvxuSBltKVtGbXnhn7/MobPJ8QdOAplcgczenzkMSzNV6PcQJVbJiGi0/UfVeqH OvDE2XAKxwqzBE3ubJ8ZoiLHg/imWg45XEwWrNf4gV9T2twl9FR4TOk1xZ3NWvw3E2Fm F7gNddvw3tHIBkiQN9xARHizGJuQXZrIh5jqy5Io4sJDexrEAEBsvjMS5UOoSKDw/R1F LZww== X-Gm-Message-State: AEkoouuSfmOD/LBx7cJwN8NPF2fS+hA+lmz9JlmVmFe6KASZjksHio49Q2soqLx+q7OH2WEVcTWuzpJCNBw8Ew== X-Received: by 10.36.55.133 with SMTP id r127mr25252033itr.15.1469536711980; Tue, 26 Jul 2016 05:38:31 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.20.67 with HTTP; Tue, 26 Jul 2016 05:37:52 -0700 (PDT) In-Reply-To: <1469525797.2529112.676963937.25E14FD6@webmail.messagingengine.com> References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> <1469525797.2529112.676963937.25E14FD6@webmail.messagingengine.com> From: Gabriel Scherer Date: Tue, 26 Jul 2016 08:37:52 -0400 Message-ID: To: Leo White Cc: caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] exception Foo = Bar.Baz 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