On 01/24/2012 10:56 PM, Edward Z. Yang wrote:
Excerpts from Mikhail Vorozhtsov's message of Tue Jan 24 07:26:35 -0500 2012:
Sure, but note that evaluate for IO is implemented with seq# under the hood,
so as long as you actually get ordering in your monad it's fairly
straightforward
to implement evaluate. (Remember that the ability to /catch/ an error
thrown by evaluate is separate from the ability to /evaluate/ a thunk which
might throw an error.)
Yes, of course. The purpose of MonadUnbottom is to guarantee that
`Control.Exception.throw e ∷ μ α = abort (toException e)`. The choice of
a class method is somewhat arbitrary here (one could go with 'α → μ
(Either SomeException α)` or with no methods at all).
I want to highlight the strangeness of "exception-like" monads that don't have
a MonadUnbottom instance (for concreteness, let's assume that there are no
methods associated with it. What would you expect this code to do?
catch (throw (UserError "Foo")) (putStrLn "caught")>> putStrLn "ignored
result"
If we don't have ordering, the monad is permitted to entirely ignore the thrown
exception. (In fact, you can see this with the lazy state monad, so long as you
don't force the state value.) Just like in lazy IO, exceptions can move around
to places you don't expect them.
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 = ⊥`.
[snip]
Stepping back for a moment, I think the conversation here would be helped if we
dropped loaded terms like "general" and "precise" and talked about concrete
properties:
- A typeclass has more/less laws (equivalently, the typeclass constrains
what else an object can do, outside of an instance),
- A typeclass requires an instance to support more/less operations,
- A typeclass can be implemented for more/less objects
One important point is that "general" is not necessarily "good". For example,
imagine I have a monad typeclass that has the "referential transparency" law
(why are you using a monad?! Well, never mind that for now.) Obviously, the IO
monad cannot be validly be an instance of this typeclass. But despite only
admitting instances for a subset of monads, being "less general", I think most
people who've bought into Haskell agree, referentially transparent code
is good code! This is the essential tension of generality and specificity:
if it's too general, "anything goes", but if it's too specific, it lacks
elegance.
So, there is a definitive and tangible difference between "all bottoms are
recoverable"
and "some bottoms are recoverable." The former corresponds to an extra law
along the lines of "I can always catch exceptions." This makes reduces the
number of objects the typeclass can be implemented for (or, if you may,
it reduces the number of admissible implementations for the typeclass), but
I would like to defend this as good, much like referential transparency
is a good restriction.
OK, what MonadUnrecoverableException exactly do you have in mind?
I don't know, I've never needed one! :^)
I was thinking about something like (no asynchronous exceptions for now):
-- ABORTS(μ) ⊆ RECOVERABLE_ZEROS(μ) ⊆ FINALIZABLE_ZEROS(μ) ⊆ ZEROS(μ)
Do you have a motivation behind this division? Are there non-finalizable
but recoverable zeros? Why can't I use aborts to throw non-recoverable
or non-finalizable zeros? Maybe there should be a hierarchy of recoverability,
since I might have a top-level controller which can "kill and spawn" processes?
Maybe we actually want a lattice structure?
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(μ)
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`.
Someone has put a term for this problem before: it is an "embarassment of
riches".
There is so much latitude of choice here that it's hard to know what the right
thing to do is.
-- RECOVERABLE_ZEROS = zeros recoverable /by `recover`/.
-- e.g. `mzero` may not be in RECOVERABLE_ZEROS, even though it is
-- recoverable by `mplus`.
class MonadAbort e μ ⇒ MonadRecover e μ | μ → e where
-- let eval m = recover (Right<$> m) (return . Left)
-- LAWS:
-- eval (return a) = return $ Right a
-- eval (abort e) = return $ Left e
-- eval (m>>= f) = eval m>>= either (return . Left) (eval . f)
recover ∷ μ α → (e → μ α) → μ α
-- RECOVERABLE_ZEROS(μ) = ZEROS(μ)
class MonadRecover e μ ⇒ MonadRecoverAll e μ | μ → e where
-- EXTRA LAW:
-- ∀ z ∷ μ α . (∀ f ∷ α → μ β . z>>= f = z)
-- => eval z = return $ Left ERROR(z)
-- No new methods.
finallyDefault ∷ MonadRecoverAll e μ ⇒ μ α → (Maybe α → μ β) → μ (α, β)
finallyDefault m f = do
a ← m `recover` \e → f Nothing>> abort e
(a, )<$> f (Just a)
I must admit, I have some difficulty seeing what is going on here. Does
the instance of a type class indicates there /exist/ zeros of some type
(zeros that would otherwise be untouchable?)
A MonadRecoverAll instance indicates that /all/ (can be relaxed to "all
finalizable") left zeros are recoverable by `recover`. The
implementation dependent meta-function `ERROR` maps zeros to the error
type `e` (but `ERROR (abort e) = e` always holds).
Well, in that case, recover/finally are being awfully nosy sticking their
laws into non-bottom zeros. :^)
`recover` should be tied to `abort` in the same manner as `mplus` is
tied to `mzero`. But I admit that MonadFinally is wacky, I can't even
give laws for it.
It would be cool if we could figure this out.
The "no error" and "recoverable error" scenarios are simple. But when an
unrecoverable error occurs, the finalizer may well be executed in a
different environment altogether (e.g. something like C `atexit`).
I want to squash all the typeclasses into one, staying as close to IO
exceptions as possible. This is because bottom is special, and I think
it's worth giving a typeclass for handling it specially. Let's call
this typeclass MonadException.
So I won't be able to use `catch` with `ErrorT SomeException` or
interpreters that do not handle bottoms?
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.
Some other points here:
- Why not use exceptions? I've always thought ErrorT was not such a good
idea, if you are in an IO based monad stack. If you're in a
left-associated stack of binds, exceptions are more efficient. (The
obvious answer is: you want the semantics to be different. But then...)
- 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.
MonadPlus is a fine typeclass and can be left as is. I don't think
MonadException should interact with MonadPlus zeros. In fact, I don't
even think IO should really be MonadPlus.
What about `MaybeT IO` and STM?
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 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`.
I make no claim about whether or not a modular API would make sense for
the unrecoverable/recoverable exception idea. Maybe it does, I haven't
thought hard enough about it. However, I definitely object to such an API
being used in a generic fashion, for ordinary IO as well.
Then we'll need two different APIs for error handling. One for "exactly
like IO" and one for "not exactly like IO". And all the common idioms
(starting with the contents of `Control.Exception`) will need to be
implemented twice. I just want to be able to write
-- Assuming the ConstraintKinds extension is enabled.
type MonadException μ = (MonadAbort SomeException μ, ...)
and get all the utilities for free.
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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
