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

[Alain Frisch <alain.frisch@lexifi.com>]

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
>