<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote">On Mon, Dec 14, 2015 at 11:18 PM, martin <span dir="ltr"><<a href="mailto:monkleyon@googlemail.com" target="_blank">monkleyon@googlemail.com</a>></span> wrote:<br><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, I know, my sketch is like a swiss cheese.</blockquote><div><br></div><div>That's fine in many places. But extraordinary claims -- like applicative and arrow brackets being the same -- demand extraordinary evidence.<br><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Also, I apologize for my abuse of language. </blockquote><div><br></div><div>(Actually that wasn't directed at anyone in particular. I'd really like to get to the bottom of this, and abuse of language is like drilling with a blunt bit.)<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">My excuse is that my training did not involve the precise terms used in English proofs. (It's not my first language, after all.) </blockquote><div><br></div><div>A smart man once wrote that Fate has imposed upon my writing the yoke of a foreign tongue that was not sung at my cradle. That makes two of us. (See what I wrote about "missing holes"? There was a hole. Erik filled it. No-one misses it.)<br><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Indeed it did not even expand to proofs in this area at all. The<br>
only language I know how to express proofs in unambiguously is Haskell<br>
itself - but I haven't found a way to express the relationships here.<br>
Most importantly:<br>
<br>
instance (forall b.Applicative (a b)) => Arrow a where ...<br></blockquote><div><br></div><div>You're referring to <br><br>
<a href="http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html" rel="noreferrer" target="_blank">http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html</a><br><br>?<br><br></div>Superclassing Applicative over Arrow appears off.<br></div><div class="gmail_quote"> <br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
That's not idiomatic, and I haven't found any idiomatic way to express<br>
that relationship yet.<br>
As a result (and to keep the sketch short), my goal was more on the<br>
level of transporting intuition.<br>
<br>
So, to quell your hunger for proofs, here's a proof that fmapA is indeed<br>
a suitable definition for fmap:<br></blockquote><div><br></div><div>Or we could just cite "instance Arrow a => Applicative (WrappedArrow a b)" in<br><br><a href="https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Applicative.html">https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Applicative.html</a><br></div><div><br></div><div>Make no mistake: The goal here isn't pedantry. We retrace the steps (1) to (4) with a fine-toothed comb to understand the claimed equivalence of brackets.<br></div><div><br><br></div><div>-- Kim-Ee<br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
# Definition<br>
fmapA f = \a -> a >>> arr f -- equivalent through currying and the<br>
definition of (>>>)<br>
<br>
# fmap id == id<br>
fmapA id = \a -> a >>> arr id -- definition of fmapA<br>
= \a -> a >>> id -- Arrow law<br>
= \a -> id . a -- definition of (>>>)<br>
= \a -> a -- definition of id<br>
= id -- definition of id<br>
<br>
# fmap (f . g) == (fmap f) . (fmap g)<br>
fmapA (f . g) = \a -> a >>> arr (f . g) -- definition of fmapA<br>
= \a -> a >>> arr (g >>> f) -- definition of (>>>)<br>
= \a -> a >>> (arr g >>> arr f) -- Arrow law<br>
= \a -> (a >>> arr g) >>> arr f -- Category law<br>
= \a -> (fmapA g a) >>> arr f -- definition of fmapA<br>
= \a -> fmapA f (fmapA g a) -- definition of fmapA<br>
= \a -> (fmapA f) . (fmapA g) a -- definition of (.)<br>
= (fmapA f) . (fmapA g) -- currying<br>
<br>
And here's the blog post that initially convinced me of the relationship<br>
between Arrows and Applicatives:<br>
<a href="http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html" rel="noreferrer" target="_blank">http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html</a><br>
<br>
The alternative definition of Applicative as Monoidal can be found in<br>
the Typeclassopedia:<br>
<a href="https://wiki.haskell.org/Typeclassopedia#Alternative_formulation" rel="noreferrer" target="_blank">https://wiki.haskell.org/Typeclassopedia#Alternative_formulation</a><br>
<br>
There are still holes to be filled, but these are more or less all the<br>
pieces of the puzzle I have so far.<br>
<div class="HOEnZb"><div class="h5"><br>
On 2015-12-14 16:41, Kim-Ee Yeoh wrote:<br>
> On Mon, Dec 14, 2015 at 10:10 PM, Erik Hesselink <<a href="mailto:hesselink@gmail.com">hesselink@gmail.com</a>><br>
> wrote:<br>
><br>
> Every Arrow is a Functor through:<br>
>> fmapA :: Arrow arr => (a -> b) -> arr i a -> arr i b<br>
>> fmapA f a = arr f . a<br>
>><br>
>> Right?<br>
>><br>
> That's one of the missing holes in Martin's claim.<br>
><br>
> In cases like this, it would help to avoid any risk that the usual abuse of<br>
> language brings. So an arrow is not a functor but it does give rise to one.<br>
> More precisely, there would be an instance Arrow a => Functor (a b).<br>
><br>
> -- Kim-Ee<br>
><br>
<br>
</div></div><div class="HOEnZb"><div class="h5">_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div></div>