[TYPES] breaking abstraction with ML exceptions

[Sam Lindley]

Thanks Derek.

My subject line is deliberately provocative. Given that exceptions in ML are 
values that inhabit a single type, the behaviour does make sense, and is rather 
unsurprising if we rewrite M as:

   structure M :> sig val A : exn end =
   struct
     val A = C
   end

I did not have in mind an alternative semantics (I agree that introducing a 
"doppleganger" in the way you suggest would be unworkable). I was more 
interested in whether people abstract over exceptions in this way in practice. 
Gabriel's response suggests that perhaps they don't very often.

My motivation is understanding how this kind of pattern interacts with various 
designs for effect type systems that track exceptions - and whether one could 
perhaps get away with forbidding it.

Sam

On 28/03/18 13:17, Derek Dreyer wrote:
> Hi, Sam.
> 
> I would take issue with your characterization of this example as
> "breaking abstraction".  By way of analogy, when you opaquely seal a
> module with a signature containing a field
> 
> val v : T,
> 
> it does not mean that the client of the module sees a "fresh" value of
> type T (whatever that could mean) -- it means that the client can use
> the exported value at the type T.  In the case of an exception spec,
> you are exporting a value/constructor of type exn.  Values of type exn
> can have their tags dynamically inspected, and that's what's happening
> here, so I fail to see how any abstraction has been broken here.
> 
> Furthermore, I can't think of any other sensible semantics for
> signature matching with exceptions.  If the external M.A in your
> example were somehow made distinct from the internal A (= C), that
> would mean that the exception A had a different dynamic representation
> when referred to outside the module than it did inside the module.  In
> fact, they would be distinct values!  This would be particularly
> horrible, since the module's implementation would not even have a way
> of referring to the doppelganger exception M.A (and catching it) from
> within the module.  This is reminiscent of the "double vision problem"
> in recursive modules, except much much worse.  I would go so far as to
> say that such a semantics would be impossible to program against.
> 
> Do you have some alternative sensible semantics for exceptions and
> signature matching in mind?
> 
> Cheers,
> Derek
> 
> On Wed, Mar 28, 2018 at 11:49 AM, Sam Lindley <Sam.Lindley at ed.ac.uk> wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> The following SML program
>>
>>    exception C;
>>
>>    structure M :> sig exception A end =
>>    struct
>>      exception A = C
>>    end;
>>
>>    (raise M.A) handle C => 42
>>
>> returns the value 42 (according to SML/NJ and, I believe, the 1997
>> definition of Standard ML).
>>
>> The signature ascription appears to assert that exception A is abstract in
>> M, and yet we are able to raise the exception M.A and catch it as C outside
>> the scope of M. It makes no difference whether the signature ascription is
>> transparent or opaque. The equivalent OCaml program yields the same result.
>>
>> Does this kind of code occur in practice?
>>
>> Sam
>>
>> --
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.