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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
