[Caml-list] exception Foo = Bar.Baz

[Caml-list] exception Foo = Bar.Baz

[Matej Kosik]

Hi,

Here:

  http://caml.inria.fr/pub/docs/manual-ocaml/typedecl.html#sec156

in Section 8.6.2 (Exception definitions) I read that one can define an alternate name for some existing exception.

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?

Re: [Caml-list] exception Foo = Bar.Baz

[Alain Frisch]

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"?  (This could perhaps allow the compiler to report 
more pattern as being useless, but this is of limit benefit.)

-- Alain

Re: [Caml-list] exception Foo = Bar.Baz

[Gabriel Scherer]

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.

On Mon, Jul 25, 2016 at 4:02 PM, Alain Frisch <alain.frisch@lexifi.com> 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"?  (This could perhaps allow the compiler to report more
> pattern as being useless, but this is of limit benefit.)
>
> -- Alain
>
>
> --
> 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

Re: [Caml-list] exception Foo = Bar.Baz

[Leo White]

> 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

Re: [Caml-list] exception Foo = Bar.Baz

[Gabriel Scherer]

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 <leo@lpw25.net> 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

Re: [Caml-list] exception Foo = Bar.Baz

[Alain Frisch]

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 <leo@lpw25.net> 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
>

Re: [Caml-list] exception Foo = Bar.Baz

[Gabriel Scherer]

I would see some use in being able to rename variant constructors, see

  MPR#7102: Ability to re-export a variant definition with renamed constructors?
  http://caml.inria.fr/mantis/view.php?id=7102

On Tue, Jul 26, 2016 at 12:27 PM, Alain Frisch <alain.frisch@lexifi.com> wrote:
> 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 <leo@lpw25.net> 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
>>
>>
>

Re: [Caml-list] exception Foo = Bar.Baz

[Alain Frisch]

On 26/07/2016 18:32, Gabriel Scherer wrote:
> I would see some use in being able to rename variant constructors, see
>
>   MPR#7102: Ability to re-export a variant definition with renamed constructors?
>   http://caml.inria.fr/mantis/view.php?id=7102

The fact that an expression "A = B" can evaluate to true can be 
confusing and really change the interpretation of constructors as atoms. 
  It's already the case for exceptions/extension constructors, but I'd 
prefer to have less of it than more.

Thinking more about it, even for exceptions, not allowing different name 
for the same constructor could be useful to optimize cases such as:


   try

     try
      ....
      raise A
      ...
     with B -> ...

   with A -> ....


If the compiler could assume that A and B were different constructors, 
it could compile the "raise" to a static jump to the handler for A, 
removing two dynamic comparisons with exception slots (and their 
associated memory accesses).


Alain

Re: [Caml-list] exception Foo = Bar.Baz

[Gabriel Scherer]

You can already eliminate one of the two comparisons if both A are
statically known to be the same. Moreover, cross-module optimization
information is likely to give you the actual definition of both A and
B -- if they are just defined with either "exception Foo" or
"exception Bar = Baz" as a structure item of the compilation unit
level, their identity will be known. In the complex cases where it is
not (functor parameters, inclusion of a first-class module, etc.), the
cost corresponds to some extra expressiveness for the user that I
think is worth it.

On Wed, Jul 27, 2016 at 4:07 AM, Alain Frisch <alain.frisch@lexifi.com> wrote:
> On 26/07/2016 18:32, Gabriel Scherer wrote:
>>
>> I would see some use in being able to rename variant constructors, see
>>
>>   MPR#7102: Ability to re-export a variant definition with renamed
>> constructors?
>>   http://caml.inria.fr/mantis/view.php?id=7102
>
>
> The fact that an expression "A = B" can evaluate to true can be confusing
> and really change the interpretation of constructors as atoms.  It's already
> the case for exceptions/extension constructors, but I'd prefer to have less
> of it than more.
>
> Thinking more about it, even for exceptions, not allowing different name for
> the same constructor could be useful to optimize cases such as:
>
>
>   try
>
>     try
>      ....
>      raise A
>      ...
>     with B -> ...
>
>   with A -> ....
>
>
> If the compiler could assume that A and B were different constructors, it
> could compile the "raise" to a static jump to the handler for A, removing
> two dynamic comparisons with exception slots (and their associated memory
> accesses).
>
>
> Alain

Re: [Caml-list] exception Foo = Bar.Baz

[Alain Frisch]

On 27/07/2016 10:27, Gabriel Scherer wrote:
> You can already eliminate one of the two comparisons if both A are
> statically known to be the same.

You could check if A is equal B on the raise site and jump to the 
correct handler depending on the result, but this approach could in 
general produce much bigger code (you need to check equality with all 
intermediate exception constructors with the same arity on each such raise).

> Moreover, cross-module optimization
> information is likely to give you the actual definition of both A and
> B -- if they are just defined with either "exception Foo" or
> "exception Bar = Baz" as a structure item of the compilation unit
> level, their identity will be known.

Indeed, good point.

Thanks also to Leo for providing a good use case (renaming on functor 
boundaries).

Alain

Re: [Caml-list] exception Foo = Bar.Baz

[Leo White]

> 
> So: do people see some use in being able to rename extension constructors?
> 

Renaming extension constructors can definitely be useful. Essentially, it is required
if you want to have an extension constructor as the parameter or result of some
function.

The testsuite contains such an example:

  https://github.com/ocaml/ocaml/blob/trunk/testsuite/tests/typing-extensions/msg.ml

In that example, the function is a functor which returns fresh constructors. The name of
this constructor is just `C` since the functor does not know what the constructor
represents, but it can then be renamed to something more suitable.

Regards,

Leo

Re: [Caml-list] exception Foo = Bar.Baz

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

──────────────────────────────────────────────────────────────────────────────

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

Re: [Caml-list] exception Foo = Bar.Baz

[Gerd Stolpmann]

[-- Attachment #1: Type: text/plain, Size: 4419 bytes --]

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


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]