<div dir="auto"><div>There should be at least some laws for callCC.<div dir="auto"><br></div><div dir="auto">Obvious ones:</div><div dir="auto"><br></div><div dir="auto">* callCC (const m) = m</div><div dir="auto"><br></div><div dir="auto">This one says callCC itself has no side effects other than passing the continuation to the provided function.</div><div dir="auto"><br></div><div dir="auto">* callCC f = callCC (f . fmap absurd)</div><div dir="auto"><br></div><div dir="auto">This says that the return type of the continuation is effectively m Void, so it will never actually "return".</div><div dir="auto"><br></div><div dir="auto">* callCC ($ a) = pure a</div><div dir="auto"><br></div><div dir="auto">The continuation given returns the value passed to it, and not a different one. It could also probably be expanded to:</div><div dir="auto"><br></div><div dir="auto">* callCC ((>>=) m) = m</div><div dir="auto"><br></div><div dir="auto">One I'm not as sure about:</div><div dir="auto"><br></div><div dir="auto">* callCC (\k -> f k >>= (\a -> k a >>= g)) = callCC (\k -> f (fmap absurd . k) >>= (fmap absurd . k))</div><div dir="auto"><br></div><div dir="auto">A more precise and probably more checkable way of saying that the continuation given doesn't actually return (in other words, it's a left zero for (>>=)), but I'm not sure if it always holds. I'm pretty sure it does, though, because if f uses k at any point, then it would have already returned, by induction on f and the ((>>=) m), ($ a), and (const m) base cases.</div><div dir="auto"><br></div><div dir="auto">Incidentally, if you have the MonadCont, MonadReader, MonadState, or MonadWriter operations with a type that only is a Bind (from semigroupoids), then you can prove it's an Applicative and Monad as well:</div><div dir="auto"><br></div><div dir="auto">* callCC ($ a) = pure a</div><div dir="auto">* a <$ ask = pure a</div><div dir="auto">* a <$ get = pure a</div><div dir="auto">* a <$ tell mempty = pure a</div><div dir="auto"><br></div><div dir="auto">But I don't see how you can with MonadError, though.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Oct 20, 2019, 14:27 Li-yao Xia <<a href="mailto:lysxia@gmail.com" target="_blank" rel="noreferrer">lysxia@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">And I forgot to link to the Coq development for the curious ones: <br>
<a href="https://github.com/Lysxia/coq-mtl" rel="noreferrer noreferrer noreferrer" target="_blank">https://github.com/Lysxia/coq-mtl</a><br>
<br>
On 10/20/19 3:25 PM, Li-yao Xia wrote:<br>
> Hello Libraries,<br>
> <br>
> Some time ago I proposed some laws for the most common mtl classes <br>
> (State, Reader, Error): <br>
> <a href="https://mail.haskell.org/pipermail/libraries/2019-April/029549.html" rel="noreferrer noreferrer noreferrer" target="_blank">https://mail.haskell.org/pipermail/libraries/2019-April/029549.html</a><br>
> <br>
> To address some concerns about completeness I reorganized the laws into <br>
> groups describing more high-level properties, and formalized them in Coq <br>
> to ensure the laws are strong enough to lift themselves through common <br>
> transformers (StateT, ExceptT, ContT; ReaderT and WriterT are similar to <br>
> StateT, but formalizing that relationship also makes the laws interact <br>
> in interesting ways).<br>
> <br>
> I'm open to suggestions for better ways to verify the "completeness" of <br>
> the laws. However, as long there aren't any objections to the existing <br>
> laws themselves, it still seems worth having some documentation earlier <br>
> rather than never.<br>
> <br>
> In the end the actual changes to the initial proposal were quite minor. <br>
> Feel free to weigh in on the following pull requests:<br>
> <br>
> <a href="https://github.com/haskell/mtl/pull/61" rel="noreferrer noreferrer noreferrer" target="_blank">https://github.com/haskell/mtl/pull/61</a> (MonadReader, MonadState)<br>
> <a href="https://github.com/haskell/mtl/pull/62" rel="noreferrer noreferrer noreferrer" target="_blank">https://github.com/haskell/mtl/pull/62</a> (MonadError)<br>
> <br>
> ---<br>
> <br>
> # Changes<br>
> <br>
> 1. Three laws were added,<br>
> <br>
> In MonadReader,<br>
> <br>
> > local id = id<br>
> <br>
> to complete the property that local is a monoid homomorphism (rather <br>
> than only semigroup); thanks to Andreas Abel for pointing out its <br>
> absence in the initial proposal.<br>
> <br>
> <br>
> > local f u = ask >>= \s -> local (\_ -> f s) u<br>
> <br>
> This law was necessary to verify ContT's MonadReader instance. ContT is <br>
> not actually lawful, but a certain subset of it seems to be (the <br>
> elements of ContT that satisfy the commutativity of ask).<br>
> <br>
> I did not manage to find out whether it's implied by the other laws.<br>
> <br>
> <br>
> In MonadError, a naturality law<br>
> <br>
> > fmap f (catchError u h) = catchError (fmap f u) (fmap f . h)<br>
> <br>
> whose need arose when describing the relationship between StateT's and <br>
> ReaderT's instances.<br>
> <br>
> <br>
> 2. Another finding is the fact that, much like the laws of MonadState <br>
> are equivalent to saying that 'state' is a monad morphism, the 'ask' <br>
> fragment of MonadReader (which to many *is* MonadReader) can also be <br>
> characterized by a monad morphism, which cannot be 'reader', as it only <br>
> yields two of the 'ask' laws.<br>
> <br>
> <br>
> 3. There were two mistakes in the original proposal.<br>
> <br>
> One MonadError law was too strong:<br>
> <br>
> > catchError (m >>= k) h = tryError m >>= either h k -- broken by StateT<br>
> <br>
> And local should flip the order of composition<br>
> <br>
> > local g . local f = local (g . f) -- wrong<br>
> > local g . local f = local (f . g) -- right<br>
> <br>
> ---<br>
> <br>
> # Updated proposal<br>
> <br>
> ## MonadState<br>
> <br>
> > get >>= put = pure ()<br>
> > put s >> get = put s >> pure s<br>
> > put s1 >> put s2 = put s2<br>
> <br>
> Those three laws imply the following equations expressing that get has <br>
> no side effects:<br>
> <br>
> > get >> m = m<br>
> > get >>= \s1 -> get >>= \s2 -> k s1 s2 = get >>= \s -> k s s<br>
> <br>
> state must be equivalent to its default definition in terms of get and <br>
> put, and conversely. Under that last condition, a property which is <br>
> equivalent to the laws above is that state must be a monad morphism, <br>
> from State s to m.<br>
> <br>
> ---<br>
> <br>
> ## MonadReader<br>
> <br>
> ask has no side effects, and produces the same result at any time.<br>
> <br>
> > ask >> m = m<br>
> > ask >>= \s1 -> ask >>= \s2 -> k s1 s2 = ask >>= \s -> k s s<br>
> ><br>
> > m <*> ask = ask <**> m<br>
> <br>
> local f applies f to the environment produced by ask.<br>
> <br>
> > local f ask = f <$> ask<br>
> > local f u = ask >>= \s -> local (\_ -> f s) u<br>
> <br>
> local is a monoid morphism from (r -> r) to (reversed) (m a -> m a) <br>
> (i.e., (Endo r -> Dual (Endo (m a)))).<br>
> <br>
> > local id = id<br>
> > local g . local f = local (f . g)<br>
> <br>
> local is a monad morphism from m to m.<br>
> <br>
> > local f (pure x) = pure x<br>
> > local f (a >>= k) = local f a >>= \x -> local f (k x)<br>
> <br>
> reader must be equivalent to its default definition in terms of ask, and <br>
> conversely.<br>
> <br>
> Under that last condition, a property which is equivalent to the first <br>
> two laws is that reader must be a monad morphism from Reader r to m.<br>
> <br>
> Another property equivalent to the first three laws is that there is a <br>
> monad morphism phi :: forall a. ReaderT r m a -> m a such that phi ask = <br>
> ask and phi . lift = id.<br>
> <br>
> ---<br>
> <br>
> ## MonadError<br>
> <br>
> See also Exceptionally Monadic Error Handling, by Jan Malakhovski: <br>
> <a href="https://arxiv.org/abs/1810.13430" rel="noreferrer noreferrer noreferrer" target="_blank">https://arxiv.org/abs/1810.13430</a><br>
> <br>
> catchError and throwError form a monad, with (>>=) interpreted as <br>
> catchError and pure as throwError.<br>
> <br>
> > catchError (throwError e) h = h e<br>
> > catchError m throwError = m<br>
> > catchError (catchError m k) h = catchError m (\e -> catchError (k e) h)<br>
> <br>
> pure and throwError are left zeros for catchError and (>>=) respectively.<br>
> <br>
> > catchError (pure a) h = pure a<br>
> > throwError e >>= k = throwError e<br>
> <br>
> catchError commutes with fmap (it is a natual transformation).<br>
> <br>
> > fmap f (catchError u h) = catchError (fmap f u) (fmap f . h)<br>
> <br>
> <br>
> ---<br>
> <br>
> Li-yao Xia<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>
</div></div>