<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Well, the answer is 'supposed' to be that Y is the identity monad. It might not quite work out that way due to bottoms, though. Lots of stuff doesn't work out in Haskell for that reason. In fact, it doesn't even form a category because of the lifted function space:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> id . _|_ = \x -> id (_|_ x) = (\x -> _|_) /= _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">This inequality is detectable by seq.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">In the identity case, it is actually not true that the Identity commonly used in Haskell is lifted, because it is defined with a newtype, and so:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> _|_ = Identity _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">holds. You can check this with seq as well. Both ((undefined :: Identity Int) `seq` ()) and ((Identity undefined :: Identity Int) `seq` ()) are undefined.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">However, I think (removing seq from the equation) Y is actually be equivalent to the lifted identity monad (or, it's probably not correct to call it the "identity monad," but whatever its proper name is). Presumably the isomorphism would go:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> data Z a = Z a<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ :: Y a -> Z a<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ (Y e) = e Z<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY :: Z a -> Y a<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY (Z x) = Y $ \k -> k x<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Note that Y is also defined with newtype, so there is no lifting involved except for the function space itself being lifted. And some equations to consider:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ _|_ = _|_ Z = _|_<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY _|_ = _|_ -- because of the pattern match<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY (toZ _|_) = _|_<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ (toY _|_) = _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY (Z _|_) = Y $ \k -> k _|_<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ (Y $ \k -> k _|_) = Z _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ (toY (Z _|_)) = Z _|_<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY (toZ (return _|_)) = return _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">So this looks promising. The monkey wrench comes in when we consider:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> Y $ \_ -> _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">because:<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toZ (Y $ \_ -> _|_) = (\_ -> _|_) Z = _|_<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"> toY (toZ (Y $ \_ -> _|_)) = _|_<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">And as mentioned before, seq can detect this difference. However, seq is the only way to detect this difference, as far as I know. So if seq on functions were given a semantics that didn't distinguish `undefined` from `const undefined` (which would make 'the category of Haskell types and functions' an actual category), then it seems quite likely that Y would be properly isomorphic to Z.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">This is a rather expected result, too, because Y is how we Church (or Boehm-Berarducci) encode things. And taking laziness and bottoms into account, it's not surprising that it is the encoding of the lifted definition Z instead of the unlifted definition Identity.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Hope that helps some.<br><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">-- Dan<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Feb 27, 2015 at 11:43 AM, Dr. Olaf Klinke <span dir="ltr"><<a href="mailto:o.klinke@dkfz-heidelberg.de" target="_blank">o.klinke@dkfz-heidelberg.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Dan,<br>
<br>
you posted an entry on the Comonad.Reader blog about free monoids in Haskell. I commented about FM being a monad, and meanwhile verified that indeed every monoid is an FM-algebra. The proofs are analogous to proving that the continuation (_ -> r) -> r for fixed r is a monad and that r is an algebra for it, respectively. Moreover, the FM-algebra stucture is a monoid homomorphism w.r.t. the monoid instance you gave for (FM a).<br>
<br>
I'd like to ask what happens when one omits the Monoid constraint. That is, what are the elements of<br>
<br>
newtype Y a = Y { runY :: forall b. (a -> b) -> b }<br>
<br>
(Y a) is like (Control.ForFree.Yoneda Identity a), that is, elements of (Y a) should be natural transformations from the reader functor ((->) a) to the identity functor. If that is true, then the Yoneda lemma tells us that (Y a) is isomorphic to (Identity a), but at least operationally that seems not to be the case:<br>
u = runY (return undefined)<br>
has different semantics than<br>
u' = runY (Y undefined) as can be seen by applying both to const (). So return does not map ⊥ to (Y ⊥). I wonder whether one can exhibit other elements not equal to any return(x). Of course (Identity a) is actually the lifted a, since<br>
⊥≠I dentiyt ⊥.<br>
Yet this does not serve as an explanation for u vs. u', as both u and u' are of the form (Y _), but one function evaluates its argument while the other does not.<span class="HOEnZb"><font color="#888888"><br>
<br>
Olaf</font></span></blockquote></div><br></div>