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 66B9E7EF5E for ; Tue, 26 Jul 2016 14:13:57 +0200 (CEST) IronPort-PHdr: 9a23:InGUyBCxhxiM9IBXR/rjUyQJP3N1i/DPJgcQr6AfoPdwSP7ypMbcNUDSrc9gkEXOFd2CrakV06yI6Ou8BCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+KyZrsnLzvs7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgwcT3uBuLbgyU53hUBjhJzEZDW1KU5k+qDpyouXP27LZ0giTLYsb6Eu5oVxyt6q5qTFnjjyJRZBAj92SCpcFqgOpgvBWlvxl2xYicNICTOv1Wca7HcZYBWW1FRsNYUSoHDo7qPNhHNPYIIesN99q1nFAJtxbrQFD0XO4= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=info@gerd-stolpmann.de; spf=None smtp.mailfrom=info@gerd-stolpmann.de; spf=None smtp.helo=postmaster@mout.kundenserver.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=pra; client-ip=212.227.126.131; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=mailfrom; client-ip=212.227.126.131; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.kundenserver.de) identity=helo; client-ip=212.227.126.131; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="postmaster@mout.kundenserver.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A5AgCaU5dXf4N+49RUCoQVfLp3JIV5AoE1PBABAQEBAQEBAREBAQkLCwkXMYIyBAESAYITAQUjMiQQCQIQCCoCAlcGEwmILAEJjBKdII1ZAQEBAQEBBAEBAQEBAQESDoUyhUWEGAUvgnWCWgWII4VyhVqFQoE8AoRaiGOJUASFa4wtg3g1hBlsAYZ+gUMBAQE X-IPAS-Result: A0A5AgCaU5dXf4N+49RUCoQVfLp3JIV5AoE1PBABAQEBAQEBAREBAQkLCwkXMYIyBAESAYITAQUjMiQQCQIQCCoCAlcGEwmILAEJjBKdII1ZAQEBAQEBBAEBAQEBAQESDoUyhUWEGAUvgnWCWgWII4VyhVqFQoE8AoRaiGOJUASFa4wtg3g1hBlsAYZ+gUMBAQE X-IronPort-AV: E=Sophos;i="5.28,424,1464645600"; d="asc'?scan'208";a="227995929" Received: from mout.kundenserver.de ([212.227.126.131]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 26 Jul 2016 14:13:50 +0200 Received: from office1.lan.sumadev.de ([84.59.137.140]) by mrelayeu.kundenserver.de (mreue002) with ESMTPSA (Nemesis) id 0MFljh-1bV42425HJ-00Eef1; Tue, 26 Jul 2016 14:13:49 +0200 Received: from [192.168.5.133] (e130.fritz.box [192.168.5.133]) by office1.lan.sumadev.de (Postfix) with ESMTPSA id D25D5DC05D; Tue, 26 Jul 2016 14:13:48 +0200 (CEST) Message-ID: <1469535221.26353.12.camel@e130.lan.sumadev.de> From: Gerd Stolpmann To: Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> Cc: Alain Frisch , OCaml , Gabriel Scherer Date: Tue, 26 Jul 2016 14:13:41 +0200 In-Reply-To: References: <64e8e1be-7081-d683-e777-6f377968f36c@gmail.com> <07e4f1d2-f61f-4047-b1a0-7339b78825e3@lexifi.com> Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="=-mw3SCyeIB51SWpcWdDgP" X-Mailer: Evolution 3.10.4-0ubuntu2 Mime-Version: 1.0 X-Provags-ID: V03:K0:iNEXedjTOYMiAOBL/qyIdSX/FbX/Jnbc/rWMfUKp4Xs5rLoBh69 F29QdoJdyXu+V6fSe4yaT0tH4l1Rf5BhBc0Nho7R4Uscujcpzb98yHVUlPnnoSbEB4b9xmF O/sUelFgC/H95XCijcu9hNM8uZbOxvDqaHW/0/qSg9UcV1lLOltoErEvG0hjTHRTNRzHdEJ mclbv2ir9fdIvEkPaIUlA== X-UI-Out-Filterresults: notjunk:1;V01:K0:koF6DScPAfw=:/MvxrBHxe/nyaTXDH8U/p5 V5wcOV5UQdeJyM4Z4whaB2ZwIc2qTWIuk5MKPv3raSbyCqHAtb7z28L0eXi3DHByV1I69pAjW OhkDhrpcqUC/G9sSVpRcwB4J2ORJqPQenBhxm+JWjNKOO3inj+cjDT3/wC9ldIEmK2uoIbMms rK2NsAlQ5bPzficUUDbK/l2XtAAVVSJbhCvM4ivrXYZzPcgl7e5tLDb7BOdgqrqt8aFH0PgN9 1VqmjJEP9j6oW0Yvfw/jZf9UB7rVMU4ym+WHT792ZTP5Bo8LJ2xE/db4pO6zZXhjdRITbvJ+y +Admz0dTg1l6cZKpuzFQIgKd5ub6NEgr5gfx1C8kE/ttp46/C1tHbofZacxInnTLp9vmvU9Ya iUDrvWGdVY7oPUQBwkleigEfcY/dS3m5ahxSqcVZEd9iMd++fi/YSagqYz/wnGcYe6tFm2Uie TVEloU08OC3m5Q9laKzQ5ViEMimyjkQ130ds5pSFlgRozM0nxjKdLL23kIXVcMTvmz1zr/s10 DYYGr4VqHCatZPFcvWW4tVgwyWWjpbl54QJtFKevVbEOmyFsYyuK393fc6YQ1JIxcP7yHvj/4 z1N4bGPIgVbw4yiPz1YRoc/c08ETAeJ5N7HsCQqVib78gTOE6WVLONpGGAIyk0Fq06+BhpDYH PpJgdckSyJWFeh2UIgwe3i1TNDzWQ7VjuV4FX/Py9pw3Vm/Uas45fBwXjP7E4HznQoM8= Subject: Re: [Caml-list] exception Foo = Bar.Baz --=-mw3SCyeIB51SWpcWdDgP Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Am Dienstag, den 26.07.2016, 11:02 +0200 schrieb Matej Kosik: > On 07/25/2016 10:02 PM, Alain Frisch wrote: > > On 25/07/2016 16:34, Matej Kosik wrote: > >> That means that, at present, one can put something like: > >> > >> exception Foo =3D Bar.Baz > >> > >> inside a _module structure_. > >> > >> I am currently wondering why we are not allowed (also) to put this int= o a _module signature_ ? > >> Is this a deliberate decision (why?) or merely an omission? > >=20 > > What would be the use of putting that in a module signature instead of = just "exception Foo"? >=20 > AFAIK, if I put: >=20 > exception Foo >=20 > to some module signature, I am saying that: > - a given module defines a *new* exception > - a given module exports that new exception >=20 > That is not what I want to say, which is: > - a given module defines an alternative name for some *existing* exception > - a given module exports this new alternative name of an existing excepti= on. This is an interesting comment. I wonder from where this expectation comes. In OCaml, exceptions are only values, not types. For other values, we cannot assume that we get a new value, only because we find val foo : t in a signature. Does this expectation come from other languages where exceptions are usually classes (e.g. Java), and hence every exception defines a new subtype? I'm just wondering. Gerd > =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80 >=20 > The motivation is the same as in case of our ability to define alternativ= e names to existing > - sum-types > - record-types > where we can put something like >=20 > type a =3D B.c =3D C1 | C2 | ... | Cn > (* where C1, C2, C2, ..., Cn are all the constructors of sum-type B.c *) >=20 > or >=20 > type a =3D B.c =3D {f1:t1; f2:t2; ... ; fn:tn} > (* where f1,...,fn are all the fields of the record-type B.c *) >=20 > in module signature. Recently, I realized that this is actually useful bu= t I lack this kind of mechanism for exceptions. > There may be workarounds but I would like to understand why this kind of = mechanism is not available > (is this intentional or just nobody needed it so there was no motivation = to implement it). >=20 > =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80= =E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2= =94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94=80=E2=94= =80=E2=94=80=E2=94=80=E2=94=80 >=20 > Some more (although embarassing) details: >=20 > At present, individual files of Coq plugins are compiled with the followi= ng options passed to ocamlc >=20 > -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I ta= ctics -I pretyping -I interp -I stm -I toplevel -I parsing -I printing -I i= ntf -I engine -I ltac -I tools -I tools/coqdoc -I > plugins/omega -I plugins/romega -I plugins/micromega -I plugins/quote -I = plugins/setoid_ring -I plugins/extraction -I plugins/fourier -I plugins/cc = -I plugins/funind -I plugins/firstorder -I > plugins/derive -I plugins/rtauto -I plugins/nsatz -I plugins/syntax -I pl= ugins/decl_mode -I plugins/btauto -I plugins/ssrmatching -I "/home/me/.opam= /4.02.3/lib/camlp5" >=20 > and I am currently trying to whether it is possible to compile them inste= ad with just something like: >=20 > -I lib -I API -I $THE_PLUGIN_DIRECTORY >=20 > where API/API.mli is the thing I am trying to (1) identify >=20 > https://github.com/matej-kosik/coq/blob/API/API/API.mli > https://github.com/matej-kosik/coq/blob/API/API/API.ml >=20 > if I succeed, then (2) clean up, then (3) document. >=20 > Obviously, in the API, I do not want to define new exceptions, only alias= es to existing ones. > (so that plugins can catch the relevant exceptions not fake ones) >=20 > > (This could perhaps allow the compiler to report more pattern as being = useless, but this is of limit > > benefit.) >=20 --=20 ------------------------------------------------------------ Gerd Stolpmann, Darmstadt, Germany gerd@gerd-stolpmann.de My OCaml site: http://www.camlcity.org Contact details: http://www.camlcity.org/contact.html Company homepage: http://www.gerd-stolpmann.de ------------------------------------------------------------ --=-mw3SCyeIB51SWpcWdDgP Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iQEcBAABAgAGBQJXl1P1AAoJEAaM4b9ZLB5TIpsH/1uuvBm4flIstq3OMwZPBNOI jdpOtSLk2kvaldJEnpGxX4N39pWPjuRa6xwhLNSK5h/k5L9ho3klaTb3ivRqkiyQ AB1aMm3nwHmNGZ48uUWkMktvcRR2jly8+OXGRIRlNdSUk5CNWumTm3sW83XbcALd /fblx6zvAZZdM7GxSBUqm6Ur56H8CicJZps7ILo+F3yC3JTwA+p+O5vg/ObCHQ9O V0sMy9zKkJQ2LmXQhM1GFmRnTTpiQ/WsFmgV8iVLL148pbjhAi0i3Urx+yGA0hFy fVtT0NPH0GvjRGguK9qsYUVxS7hmQQYppWTit2YjllqhijmTwionViRbpBpYmWo= =KvJP -----END PGP SIGNATURE----- --=-mw3SCyeIB51SWpcWdDgP--