[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> Date: 3/28/18 10:04 AM (GMT-05:00) To: [email protected] 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 [email protected] http://gallium.inria.fr/~fpottier/
