Anders Kaseorg wrote:
Isaac Dupree wrote:
Do you see the difference? The effects are sequenced in different places. The return/join pair moves all the effects *outside* the operations such as catch... thus defeating the entire purpose of morphIO.
Yes; my question is more whether Wren has a more clever way to get an isomorphism (forall b. (m a -> IO b) -> IO b) <-> IO (m a) that would make the simpler interface work out. (Or maybe I misunderstood what he was getting at.)
Yeah no, that's what I was getting at. Since it doesn't quite work out, I should probably rethink my appeal to parametricity re Kleisli arrows.[1] That is, when we take the monad to be the identity monad or equivalently to be "no monad", then parametricity yields: (forall b. (m a -> b) -> b) <-> (m a). Apparently this makes some sort of appeal to special properties about the identity monad (e.g., being both pointed and copointed) since it doesn't generalize to every monad in the way I suggested. <musing> Perhaps the correct version is this? forall a n. Monad n => (forall b. (m a -> n b) -> n b) <-> n (m (n a)) Of course that may not solve your H98 concerns. Not all monads m provide a universal law (forall n, n.m.n -> n.m) so to define the law you'd need MPTCs to relate m and n. But if we monomorphize to just n=IO that would simplify things; but then we'd need (Traversable m) in order to collapse the two layers of IO... </musing> [1] Oleg discusses a similar need to be careful about appeals to parametricity when dealing with monads: http://okmij.org/ftp/Computation/lem.html -- Live well, ~wren