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 = Bar.Baz
> >>
> >> inside a _module structure_.
> >>
> >> I am currently wondering why we are not allowed (also) to put this into a _module signature_ ?
> >> Is this a deliberate decision (why?) or merely an omission?
> > 
> > What would be the use of putting that in a module signature instead of just "exception Foo"?
> 
> AFAIK, if I put:
> 
>   exception Foo
> 
> to some module signature, I am saying that:
> - a given module defines a *new* exception
> - a given module exports that new exception
> 
> 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 exception.

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


> ──────────────────────────────────────────────────────────────────────────────
> 
> The motivation is the same as in case of our ability to define alternative names to existing
> - sum-types
> - record-types
> where we can put something like
> 
>   type a = B.c = C1 | C2 | ... | Cn
>   (* where C1, C2, C2, ..., Cn are all the constructors of sum-type B.c *)
> 
> or
> 
>   type a = B.c = {f1:t1; f2:t2; ... ; fn:tn}
>   (* where f1,...,fn are all the fields of the record-type B.c *)
> 
> in module signature. Recently, I realized that this is actually useful but 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).
> 
> ──────────────────────────────────────────────────────────────────────────────
> 
> Some more (although embarassing) details:
> 
> At present, individual files of Coq plugins are compiled with the following options passed to ocamlc
> 
>   -I config -I lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I interp -I stm -I toplevel -I parsing -I printing -I intf -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 plugins/decl_mode -I plugins/btauto -I plugins/ssrmatching -I "/home/me/.opam/4.02.3/lib/camlp5"
> 
> and I am currently trying to whether it is possible to compile them instead with just something like:
> 
>   -I lib -I API -I $THE_PLUGIN_DIRECTORY
> 
> where API/API.mli is the thing I am trying to (1) identify
> 
>   https://github.com/matej-kosik/coq/blob/API/API/API.mli
>   https://github.com/matej-kosik/coq/blob/API/API/API.ml
> 
> if I succeed, then (2) clean up, then (3) document.
> 
> Obviously, in the API, I do not want to define new exceptions, only aliases to existing ones.
> (so that plugins can catch the relevant exceptions not fake ones)
> 
> > (This could perhaps allow the compiler to report more pattern as being useless, but this is of limit
> > benefit.)
> 

-- 
------------------------------------------------------------
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
------------------------------------------------------------