Excerpts from Mikhail Vorozhtsov's message of Sun Jan 29 05:34:17 -0500 2012: > You are trying to make bottoms a new null pointers. Sometimes it just > doesn't worth the effort (or depends on the interpreter you use). I want > to have the option to say: sorry, in this particular case (monad) I > don't distinguish `error` from non-termination, so `catch ⊥ h = ⊥`.
This is a longstanding complaint that Robert Harper has with lazy languages (the "paucity of types" complaint.) http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/ There's not much I can say here, except that: - There really is no difference: GHC can sometimes detect nontermination and will throw an exception (for example, the deadlocked exception), and - The user will sometimes act as a termination checker, and ^C a program that is taking too long. > I think it is one of the simplest layouts one can some up with. I'll try > to explain the motivation behind each inclusion. > > ABORTS(μ) ⊆ RECOVERABLE_ZEROS(μ) I'm sorry, I cannot understand the discussion below because you haven't defined precisely what ABORTS means. (See also below; I think it's time to write something up.) > Why are they not equal? After all we can always write `recover weird $ > \e → abort e`, right? But zeros from `RECOVERABLE_ZEROES \ ABORTS` may > have additional effects. For example, recoverable interruptions could > permanently disable blocking operations (you can close a socket but you > can't read/write from it). Why the inclusion is not the other way > around? Well, I find the possibility of `abort e1` and `abort e2` having > different semantics (vs `recover` or `finally`) terrifying. If you can > throw unrecoverable exceptions, you should have a different function for > that. > > RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ) > > If a zero is recoverable, we can always "finalize" it (by > catch-and-rethrow). > > FINALIZABLE_ZEROS(μ) ⊆ ZEROS(μ) > > This one is pretty obvious. One example of non-finalizable zeros is > bottoms in a non-MonadUnbottom monad (e.g. my X monad). Another would be > `System.Posix.Process.exitImmediately`. Ugh, don't talk to me about the exit() syscall ;-) > > If we can unify the semantics in a sensible way, I have no objection > > (the choice of exceptions or pure values is merely an implementation > > detail.) But it's not obvious that this is the case, especially when > > you want to vary the semantics in interesting ways. > That's why I'm trying to make things like MonadUnbottom optional. Well, I haven't actually checked if this works or not! > > - If the semantics are different, OK, now you need to write two catch > > functions, but you are handling each type of exception separately > > already, right? > You have to handle IO exceptions only if you "leak" them from your > implementation. For transformer stacks it is always so, for some > interpreters it is not. The `ErrorT e IO` problem is related to another > can of worms: operation lifting through transformers. OK. > > IO has effects, so if I have mplus (effect>> mzero) a, this equals > > effect>> a, not a. Same applies for MaybeT IO. I have to be very > > careful to preserve the monoid property. STM, on the other hand, > > by definition has the ability to rollback. This is what makes it so nice! > Should STM/`MaybeT IO` have MonadException instances? How `catch` and > `finally` will interact with `retry`/`MaybeT (return Nothing)`? I don't see why not, as long as they obey the semantics. But someone should do the legwork here. > >>> I also think that unrecoverable/recoverable exceptions is a legitimate > >>> idea. I > >>> think it could get its own typeclass, let's call it > >>> MonadUnrecoverableException. I don't think any MonadException is > >>> automatically > >>> a MonadUnrecoverableException, by appealing to the laws of MonadException. > >> I'm confused. What methods/laws would MonadUnrecoverableException contain? > > > > They'd be very simple! Unrecoverable exceptions always cause program > > execution > > to "get stuck." There are no contexts (like catch) which affect them. > So you are suggesting something like > > class MonadUnrecoverableException μ where > throwUnrecoverable ∷ Exception e ⇒ e → μ α > > But I'm not interested in throwing such exceptions! It may not even be > possible (allowed) to do that from within the monad itself (e.g. > external interruptions in my X monad). All I care about is that > unrecoverable zeros (not necessarily tied with Exception) exist, which > means that I cannot implement `finally` on top of `catch`. Yes, but in that case, your semantics would have to change to add a case for finally; you'd need to unwind the stack, etc etc. You're talking about finalizable, but unrecoverable exceptions. > > Yes, I think for some this is the crux of the issue. Indeed, it is why > > monad-control is so appealing, it dangles in front of us the hope that > > we do, in fact, only need one API. > > > > But, if some functions in fact do need to be different between the two > > cases, there's not much we can do, is there? > Yes, but on the other hand I don't want to reimplement ones that are the > same. I want to have a modular solution precisely because it allows both > sharing and extensibility. The cardinal sin of object oriented programming is building abstractions in deference of code reuse, not the other way around. Stepping back a moment, I think the most useful step for you is to write up a description of your system, incorporating the information from this discussion, and once we have the actual article in hand we can iterate from there. Edward _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe