[TYPES] breaking abstraction with ML exceptions
Andrew Myers
andru at cs.cornell.edu
Wed Mar 28 12:50:17 EDT 2018
Yizhou Zhang and I made similar observations about unchecked exceptions violating abstraction in our PLDI'16 paper. We also proposed and implemented a new exception semantics that addresses the problem, tunneled exceptions.
Andrew
-------- Original message --------From: François Pottier <francois.pottier at inria.fr> Date: 3/28/18 10:04 AM (GMT-05:00) To: types-list at LISTS.SEAS.UPENN.EDU Subject: Re: [TYPES] breaking abstraction with ML exceptions
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi Sam,
Le 28/03/2018 à 15:20, Sam Lindley a écrit :
> 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.
In OCaml, it might seem tempting to forbid the exception-aliasing
declaration, "exception A = B". But I believe that that still would not
be sufficient
to eliminate exception aliasing, by which I mean the possibility that
a single (dynamic) exception is known under two distinct (static) names.
This is due to other language features that introduce aliasing, such
as module aliasing declarations ("module A = B") and first-class
modules (a function that expects two first-class modules as arguments
can be applied twice to the same module).
--
François Pottier
francois.pottier at inria.fr
http://gallium.inria.fr/~fpottier/
More information about the Types-list
mailing list