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

[Gabriel Scherer <gabriel.scherer@gmail.com>]

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