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

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

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