ST with Efficient (simple nice semantics exceptions) was Re:

Carter Schonwald

2018-03-21 22:32:43 UTC

Thanks for the shout out Gershom!

I'd like to highlight that exceptions/effects as in the monad STE (aka ST
+ abort only semantics for exceptions) have a very very nice semantics: you
can only handle the exceptions at the runMonad (runSTE :: (forall s. STE
<https://hackage.haskell.org/package/monad-ste-0.1.0.0/docs/Control-Monad-STE.html#t:STE>
e s a) -> (Either
<https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Either.html#t:Either>
e a -> b) -> b ) and you are *guaranteed* that the exceptions thrown are
handled!

I've used it in certain interpreter style code dumps where i (private to
the ST style computation) want to use mutation, but also want to be able to
efficiently do a sort of "unsafeFreeze and export the entire heap" style
"core dump" for debugging/reproducible efforts when the program execution/
interpreter would other wise "crash"

Monad-STE <https://hackage.haskell.org/package/monad-ste-0.1.0.0> is
essentially STE s e a === ExceptT e (ST s) a, but where the throwError
isn't catchable, except ONLY by runSTE :: (forall s. STE
<https://hackage.haskell.org/package/monad-ste-0.1.0.0/docs/Control-Monad-STE.html#t:STE>
e s a) -> (Either
<https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Either.html#t:Either>
e a -> b) -> b

either way

1) it definitely hits a nice choice in mixing exceptions and state, because
by the time you're handling the exception, THERES NO STATE, so it becomes
radically simpler to handle errors because theres *NO* state to cleanup :)

2) to my knowledge, its the only monad that naturally has a Monad Throw
instance (in the IO ish flavored class) but no monad catch instance

3) likewise, to my knowledge its the only known PrimBaseMonad aside from
IO and the ST family

4) it'd be cool to have it in BASE, but i'm not sure whats the right way to
advocate it, though its certainly meaningfully distinct from IO and ST in
possible uses, though in a complimentary way that perhaps supports a
"haskell is a great imperative programming tool"

5) and at the very least it can be used for pure codes which also want to
have efficient abortive errors AND efficient binds (any error monad that
Uses either needs to case for Left's to do failure handling, this doesn't)

To be honest, you could probably do safe throwing and catching in ST by
wrapping a thrown SomeException in some hidden exception type (call it
STException), not exporting that type, and then having the catch command be
like the IO version except it only catches and unwraps STException.
Indeed, Carter has such a package here: https://hackage.haskell.
org/package/monad-ste-0.1.0.0
I wonder â could ST just be extended with some version of such
functionality directly?
-g

Just to add a couple cents, my informal intuition for âfailâ is that I
should be able to use it to âfilterâ things in do-notation or a monad
[x | Right x <- [Right "a", Right "b", Left 3]] :: [String]
Vector String
[x | Right x <- Just (Left 3)] :: Maybe String
The old âfailâ implementation for Data.Vector used to throw an exception,
and I nudged Bryan to accept a PR making it return an empty vector, so I
could use monad comprehensions for vectors with the same expectations as
list comprehensions. That does suggest MonadPlus as the ârealâ source of
the semantics I want.
But there just isnât always a well-defined thing you can do within a
given monad with only the type of âfailâ.
The fact that it raises an exception for IO is fine by me, because at
least it can be caught in IO. On the other hand, Iâd look at any code that
actually catches pattern-match failure exceptions as pretty smelly. Still,
in that context, to me the ideal solution is to also throw an exception in
ST, as long as some mechanism exists for safely throwing and catching
exceptions in ST. (I donât know how hard that would be to add.)

As one data point re: your lens, STM offers a meaningful retry.
-Edward

So this boils down to two concerns
1) should st support refutable pattern matches , and this in turn
touches on pure exceptions and totality concerns
2) is monad fail actually the monad zero or just support for refutable
patterns , which may sometimes use monad zero for implementation?
Iâm not sure one way or another.
One lens for this is: how do the arguments for monad fail differ
between ST and STM?

I also find your `Point` data type telling, but I think for the
opposite reason. I think most people would want to avoid letting a pattern
match silently turn into a bottom value in the `Point` data type.
IMO, what all of this comes down to is the fact that `MonadFail` is
1. By you to be the general purpose zero class
2. By (I think) everyone else to be the class that allows you to do
refutable pattern matches
Personally, I think `fail :: String -> m a` is a bad type for a
general purpose zero class; either MonadZero, or a type class using
`Exception` like `MonadThrow` in `exceptions, would be better. And
regardless, I don't think we should be encouraging further usage of bottom
values, even if the usage of a bottom is in fact law abiding.

If the concern is a lack of ability to have the properly sequenced
exception throwing, I would argue that the correct response is to provide a
monomorphic `failST :: String -> ST s a` function to be explicit about the
Exception e => e -> ST s a`.
I definitely agree here.
While it's true that `MonadFail (ST s)` obeys the laws, the point
here is about the extra functionality provided by `MonadFail`, namely
around pattern matching. I think the question can be boiled down to: do we
want to make it easy to call `fail` when writing code inside `ST`?
My point was more that this is rather distinct from the other cases
mentioned in that it is a true legal instance, enabling things like a
fail-based guard to actually protect against subsequent code in ST
executing.
I do find it telling that we can get into a similar situation
completely without effects with
data Point a = Point a
...
instance Monad Point where
return = Point
Point a >>= f = f a
instance MonadFail Point where
fail = error
the extra "point" added by using data rather than newtype and the
strict pattern match in >>= plumbs the error out in the same fashion as ST
here.
I find the ability to explicitly construct bottoms at the right time
to guard subsequent operations in those monads to be a piece of vocabulary
that would be otherwise missing if we retroactively tried to impose some
additional handling laws that aren't required by having a cancellative zero.

I'm a bit less convinced about the benefits removing the instance
for MonadFail (ST s).
Recall that throwIO is distinct from throw for a good reason, as it
ensures that the throwing occurs at the right step in the sequence of binds.
The `fail` instance for ST can similarly be viewed as a perfectly
reasonable monotone function affecting the result of runST :: (forall s. ST
s a) -> a, which produces an `a` that is the appropriate bottom at the
right time when you take a certain branch in the ST calculation. This is
rather different than Identity, as you can't just ape this behavior by
calling 'error' instead as you need the smarter call.
To achieve that functionality today _without_ fail, you need to
reach for unsafe operations `unsafeIOtoST . failIO` it to get the correct
semantics, which is a damn sight messier and scarier and importantly
removing the instance means this can't be something that is done by just
delegating to base monad transformer 'fail' as would be done through
something like `StateT s (ST s')`. This seems to create a false tension
between doing the most defined thing and doing the thing I want with a
stronger constraint, which I usually take as a sign that the building
blocks are wrong.
Removing this instance comes at a real cost in terms of generality
of code that uses `MonadFail`: It does pass the left zero law!
Overall, I'm -1, as I'm actually leaning against the removal of the
instance personally on the grounds above.
-Edward
On Wed, Mar 14, 2018 at 3:31 PM, Michael Snoyman <

One possible "well behaved" intuition could be "cannot result in an
exception thrown from pure code without usage of unsafe functions." By this
* Maybe's fail is well behaved: using `fail "foo"` results in a
total Nothing value
* List's: same thing, but with an empty list
* IO: runtime exception, but the exception is _not_ in pure code,
but rather from within IO, where exceptions are always to be expected
* ST: `runST (fail "foo")` results in a pure value which, when
evaluated, throws a runtime exception, breaking the well behaved definition
* Identity: `Identity (fail "foo")` can only be a pure value which
throws an exception, and is therefore not well behaved
Note that I added the requirement of "without usage of unsafe
functions," since `unsafePerformIO (fail "foo")` can result in a pure
bottom value.
On Wed, Mar 14, 2018 at 4:25 PM, Ryan Scott <

Thanks, that makes more sense. I'm inclined to agree that MonadFail
instances should fail in a "well-behaved" way. (I wish I knew how
to
make the phrase "well-behaved" more formal, but I don't.) It might
be
worth adding this intuition to the Haddocks for MonadFail.
That being said, one thing to consider before removing this
instance
is that there will be some breakage. Ben Gamari added this
instance in
[1] because apparently the regex-tdfa package needed it. Other than
that, though, I don't have any real objections to removing this
instance.
Ryan S.
-----
[1] https://phabricator.haskell.org/D3982
On Wed, Mar 14, 2018 at 9:58 AM, David Feuer <

I expect a MonadFail instance to have a well-behaved notion of

failure

within the monad. An exception from "pure" code (which is what ST
simulates) is not that. On the other hand, perhaps you're right

and

the instance should be removed for IO as well; I don't have as

strong

a sense of revulsion, but maybe users should be forced to be

explicit

with throwIO.
On Wed, Mar 14, 2018 at 9:46 AM, Ryan Scott <

OK. You used the phrase "utterly contrary to the purpose of
MonadFail", so I'm trying to figure out exactly what you mean

here.

Prima facie, the purpose of MonadFail (at least, as explained

in its

Haddocks) is to provide a type classâdirected way of desugaring
partial pattern matches in do-notation. With this in mind, the

current

MonadFail instance for ST doesn't seem too offensive.
However, I think you have some additional property in mind that

you

feel the MonadFail ST instance runs afoul of. Do you mind

explaining

in further detail what this is? (I'm not trying to be snarky

hereâI

genuinely don't know what you're getting at.)
Ryan S.
On Wed, Mar 14, 2018 at 9:41 AM, David Feuer <

I am not. I think that instance is fairly legitimate, as it

raises an

IO exception that can be caught in IO. IO's Alternative

instance is a

bit shadier, but that's not a topic for this proposal either.

ST is an

entirely different story, and I'm sorry I accidentally mixed

it in.

On Wed, Mar 14, 2018 at 9:05 AM, Ryan Scott <

It's worth noting that the MonadFail instance for IO [1] also

simply throws

an error (by way of failIO). Are you proposing we remove this

instance as

well?
Ryan S.
-----
[1]
http://git.haskell.org/ghc.git/blob/

cb6d8589c83247ec96d5faa82df3e93f419bbfe0:/libraries/base/
Control/Monad/Fail.hs#l80

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________

Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries