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

[Leo White <leo@lpw25.net>]

> 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