[TYPES] breaking abstraction with ML exceptions

[Sam Lindley]

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

Re: [TYPES] What algebra am I thinking of?

[Neel Krishnaswami]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi Phil,

I learned about this from Martin Escardo, and he told me the observation
about monoidal closure is in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".

One further observation I have not seen written down anywhere is that
the natural numbers also support a trace (ie, feedback) operator, since
it is also the case that x + y ≥ z + y if and only if x ≥ z.

This means that the Geometry of Interaction construction can be applied
to the natural numbers, which yields a preorder of pairs of natural
numbers (n,m). In this case, two objects have a map between them if
one object is greater than the other, viewing each object (n, m) as the
signed integer n - m.

As a result, I've sometimes wondered if the Int construction got its
name as a bit of a joke!

Best,
Neel


On 27/03/18 21:02, Philip Wadler wrote:

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]



Thanks to all for further replies, and especially to Neel for his
observation about monus and monoidal closure. Neel, is this written down
anywhere? Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 27 March 2018 at 13:39, Neel Krishnaswami  wrote:


On 27/03/18 15:27, Philip Wadler wrote:

Thank you for all the replies, and for reminding me of bags,

rigs/semirings, and modules.

In a rig, what corresponds to the notion of monus?
_∸_ : ℕ → ℕ → ℕ
m  ∸ zero  =  m
zero  ∸ (suc n)  =  zero
(suc m) ∸ (suc n)  =  m ∸ n
Is monus defined for every rig? (While zero and suc are defined in every
rig, it's not immediately obvious to me that definition by pattern
matching
as above makes sense in an arbitrary rig.) What are the algebraic
properties of monus?



The natural numbers Nat, ordered by , form a posetal symmetric
monoidal closed category. Here, the objects are the natural
numbers, and Hom(n, m) = { ∗ | n ≥ m }

The tensor product is given by:

   x ⊗ y ≜ x + y

The monoidal closed structure arises from saturating subtraction:

   y ⊸ z ≜ z - y

It's easy to show that Hom(x ⊗ y, z) = Hom(x, y ⊸ z) since
x + y ≥ z if and only if x ≥ z - y.

(This is all given in Lawvere's paper "Metric Spaces, Generalized
Logic, and Closed Categories".)

So it seems like the natural thing to do would be to say that a rig
has a monus when it is monoidal closed with respect to its addition,
defining x ≥ z to hold when there exists a y such that x = y + z.

Best,
Neel



--
Neel Krishnaswami
nk...@cl.cam.ac.uk




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

Re: [TYPES] breaking abstraction with ML exceptions

[Derek Dreyer]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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

Re: [TYPES] breaking abstraction with ML exceptions

[Sam Lindley]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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

Re: [TYPES] What algebra am I thinking of?

[Francesco Gavazzo]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I am not sure whether the following is the correct definition of a monus,
but following Neel (as well as the analogy with natural numbers) one could
look at monus in a monoid as right adjoint to monoid multiplication. In
particular, any quantale has monus, given by 'implication'.
This can indeed be found in Lawvere's 1973 paper, as well as in any
introduction/paper on quantales and/or generalised metric spaces. Another
relevant reference could be Chapter II of  Monoidal Topology, by Hofmann,
Seal, and Tholen. More generally, any paper dealing with V-categories (or
quantale-categories) provides relevant information on such algebraic
structures.

Best,
Francesco

2018-03-28 12:21 GMT+02:00 Neel Krishnaswami <
neelakantan.krishnasw...@gmail.com>:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi Phil,
>
> I learned about this from Martin Escardo, and he told me the observation
> about monoidal closure is in Lawvere's paper "Metric Spaces, Generalized
> Logic, and Closed Categories".
>
> One further observation I have not seen written down anywhere is that
> the natural numbers also support a trace (ie, feedback) operator, since
> it is also the case that x + y ≥ z + y if and only if x ≥ z.
>
> This means that the Geometry of Interaction construction can be applied
> to the natural numbers, which yields a preorder of pairs of natural
> numbers (n,m). In this case, two objects have a map between them if
> one object is greater than the other, viewing each object (n, m) as the
> signed integer n - m.
>
> As a result, I've sometimes wondered if the Int construction got its
> name as a bit of a joke!
>
> Best,
> Neel
>
>
> On 27/03/18 21:02, Philip Wadler wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/ma
>> ilman/listinfo/types-list ]
>>
>>
>>
>> Thanks to all for further replies, and especially to Neel for his
>> observation about monus and monoidal closure. Neel, is this written down
>> anywhere? Cheers, -- P
>>
>> .   \ Philip Wadler, Professor of Theoretical Computer Science,
>> .   /\ School of Informatics, University of Edinburgh
>> .  /  \ and Senior Research Fellow, IOHK
>> . http://homepages.inf.ed.ac.uk/wadler/
>>
>> On 27 March 2018 at 13:39, Neel Krishnaswami  wrote:
>>
>> On 27/03/18 15:27, Philip Wadler wrote:
>>>
>>> Thank you for all the replies, and for reminding me of bags,
>>>
 rigs/semirings, and modules.

 In a rig, what corresponds to the notion of monus?
 _∸_ : ℕ → ℕ → ℕ
 m  ∸ zero  =  m
 zero  ∸ (suc n)  =  zero
 (suc m) ∸ (suc n)  =  m ∸ n
 Is monus defined for every rig? (While zero and suc are defined in every
 rig, it's not immediately obvious to me that definition by pattern
 matching
 as above makes sense in an arbitrary rig.) What are the algebraic
 properties of monus?


>>> The natural numbers Nat, ordered by , form a posetal symmetric
>>> monoidal closed category. Here, the objects are the natural
>>> numbers, and Hom(n, m) = { ∗ | n ≥ m }
>>>
>>> The tensor product is given by:
>>>
>>>x ⊗ y ≜ x + y
>>>
>>> The monoidal closed structure arises from saturating subtraction:
>>>
>>>y ⊸ z ≜ z - y
>>>
>>> It's easy to show that Hom(x ⊗ y, z) = Hom(x, y ⊸ z) since
>>> x + y ≥ z if and only if x ≥ z - y.
>>>
>>> (This is all given in Lawvere's paper "Metric Spaces, Generalized
>>> Logic, and Closed Categories".)
>>>
>>> So it seems like the natural thing to do would be to say that a rig
>>> has a monus when it is monoidal closed with respect to its addition,
>>> defining x ≥ z to hold when there exists a y such that x = y + z.
>>>
>>> Best,
>>> Neel
>>>
>>>
>>>
>>> --
>>> Neel Krishnaswami
>>> nk...@cl.cam.ac.uk
>>>
>>>
>>>
>>>
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>>>
>>

Re: [TYPES] breaking abstraction with ML exceptions

[Gabriel Scherer]

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

While I cannot comment on how often this occurs in practice, I'd like to
point out that this ability to hide equalities between exceptions has
delicate implications for the compilation of pattern-matching (in
exception-handling clauses, or when matching on exceptions as values¹), and
we (Luc Maranget, Thomas Refis and myself) somewhat recently found and
fixed bugs in the OCaml pattern-matching compilation coming from them. (The
bug went unreported for a long time, suggesting that indeed these cases do
not occur terribly often in practice.)

The problem is that it is wrong to assume that two constructors with
distinct names are distinct, because one may be redefined to be equal to
the other in a way that is not visible from your type environment (so a
canonicalization strategy does not suffice). Remark that if you decide to
conservatively assume that all constructors of exception type may be equal,
and  you use a classic "matrix-based" algorithm for pattern-matching, you
can end up with ill-typed columns of patterns (containing patterns of
incompatible types), coming from "potentially-equal" constructors of
different argument types, so your pattern-matching processing has to be
robust against this. (Two types may be equal for reasons unknown to the
current typing environment, but you should also be ready to deal with
incompatible head constructors or take steps to prevent that in the check
of whether two constructors are surely equal, surely distinct, or may be
equal.)

¹: OCaml 4.02 (August 2014) introduced extensible algebraic datatypes
(variants), contributed by Leo White, which generalize the extensible-type
model of exceptions to arbitrary datatypes (including GADTs). It is more
natural to match on the value on those than on exceptions.

On Wed, Mar 28, 2018 at 11:49 AM, Sam Lindley  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.
>
>