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 144317EF5E for ; Tue, 26 Jul 2016 11:36:41 +0200 (CEST) IronPort-PHdr: 9a23:bRy/PBeqnpTfoyXn/+O/eFfSlGMj4u6mDksu8pMizoh2WeGdxc64ZR7h7PlgxGXEQZ/co6odzbGH6+a+AidZuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkb7psMSKKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLWKD+OqA5VqBwDTI8Mmlz6te4mwPESF6r63xUbWUXjhcAVwzI6zn+Roir7238u/Yri3rSBtH/Ub1hAWfq1KxsUhK90Co= Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=leo@lpw25.net; spf=None smtp.mailfrom=leo@lpw25.net; spf=None smtp.helo=postmaster@out5-smtp.messagingengine.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=pra; client-ip=66.111.4.29; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=mailfrom; client-ip=66.111.4.29; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@out5-smtp.messagingengine.com) identity=helo; client-ip=66.111.4.29; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="postmaster@out5-smtp.messagingengine.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AzAgBlLpdXhh0Eb0JehRG4eYF9hh0CgTM5EwEBAQEBAQEBEQEBAQgLCwkZL4IyFYIWAQQBQDoECwtGLCuIQgitZYYegnYBAQEHAQEBARsIiCqCTYUMgmCCL5k1AZBniAuFSJAlHwGCVYFzIDKIQgEBAQ X-IPAS-Result: A0AzAgBlLpdXhh0Eb0JehRG4eYF9hh0CgTM5EwEBAQEBAQEBEQEBAQgLCwkZL4IyFYIWAQQBQDoECwtGLCuIQgitZYYegnYBAQEHAQEBARsIiCqCTYUMgmCCL5k1AZBniAuFSJAlHwGCVYFzIDKIQgEBAQ X-IronPort-AV: E=Sophos;i="5.28,424,1464645600"; d="scan'208";a="185966697" Received: from out5-smtp.messagingengine.com ([66.111.4.29]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 26 Jul 2016 11:36:39 +0200 Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 354672056D for ; Tue, 26 Jul 2016 05:36:38 -0400 (EDT) Received: from web1 ([10.202.2.211]) by compute2.internal (MEProxy); Tue, 26 Jul 2016 05:36:38 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=lpw25.net; h= content-transfer-encoding:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-sasl-enc :x-sasl-enc; s=mesmtp; bh=I/5Kdzb/elvOry/trSkNRU5xvxY=; b=u4yETa CW1QMIht3fw45B7PDKZ5qg32B0ADinwNNXc9n40rvYI7p7jK+xG1pEjrifxdqhTB U2MBtSFrrFuO/v72MRP8VLzuUIVnpOO08ggo8UZflM82l6Af69stRcKidVXKwvrV qevqW4CiaDSDsTpX4cPn7nilV/EHbSucUo8aw= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-sasl-enc:x-sasl-enc; s=smtpout; bh=I/5Kdzb/elvOry/ trSkNRU5xvxY=; b=jinuHjvpM1O2MZ3nJITyvNExtI8Qj/OQlKzT2pZv/pOTbCJ HGC1VNTFdsTWkZG7LcsvqzJG5bIt/Dhupf6kOZJzfZ9lPdy7Zgjpn4i3HnBJiFhr OA1J+hOu3cn+FRGp1bq3jTC8JHHV9o6OKd7H1sEtoY2DIxPigY3EFocw5t/c= Received: by mailuser.nyi.internal (Postfix, from userid 99) id 07CDA6A4C7; Tue, 26 Jul 2016 05:36:38 -0400 (EDT) Message-Id: <1469525797.2529112.676963937.25E14FD6@webmail.messagingengine.com> X-Sasl-Enc: chE7XMSjd5yOxI6Xq+8lcsW08a8K6FjQRLk1gnVR7w0j 1469525797 From: Leo White To: caml-list@inria.fr MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain X-Mailer: MessagingEngine.com Webmail Interface - ajax-3c2832c2 In-Reply-To: References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> Date: Tue, 26 Jul 2016 05:36:37 -0400 Subject: Re: [Caml-list] exception Foo = Bar.Baz > 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