[Haskell-cafe] Applicative banana brackets

[Kim-Ee Yeoh]

On Mon, Dec 14, 2015 at 11:18 PM, martin <monkleyon at googlemail.com> wrote:

Yes, I know, my sketch is like a swiss cheese.


That's fine in many places. But extraordinary claims -- like applicative
and arrow brackets being the same -- demand extraordinary evidence.

Also, I apologize for my abuse of language.


(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.)


> My excuse is that my training did not involve the precise terms used in
> English proofs. (It's not my first language, after all.)


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.)

Indeed it did not even expand to proofs in this area at all. The
> only language I know how to express proofs in unambiguously is Haskell
> itself - but I haven't found a way to express the relationships here.
> Most importantly:
>
> instance (forall b.Applicative (a b)) => Arrow a where ...
>

You're referring to

http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html

?

Superclassing Applicative over Arrow appears off.


> That's not idiomatic, and I haven't found any idiomatic way to express
> that relationship yet.
> As a result (and to keep the sketch short), my goal was more on the
> level of transporting intuition.
>
> So, to quell your hunger for proofs, here's a proof that fmapA is indeed
> a suitable definition for fmap:
>

Or we could just cite "instance Arrow a => Applicative (WrappedArrow a b)"
in

https://hackage.haskell.org/package/base-4.8.1.0/docs/Control-Applicative.html

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.


-- Kim-Ee


> # Definition
> fmapA f = \a -> a >>> arr f -- equivalent through currying and the
> definition of (>>>)
>
> # fmap id == id
> fmapA id = \a -> a >>> arr id  -- definition of fmapA
>          = \a -> a >>> id      -- Arrow law
>          = \a -> id . a        -- definition of (>>>)
>          = \a -> a             -- definition of id
>          = id                  -- definition of id
>
> # fmap (f . g) == (fmap f) . (fmap g)
> fmapA (f . g) = \a -> a >>> arr (f . g)        -- definition of fmapA
>               = \a -> a >>> arr (g >>> f)      -- definition of (>>>)
>               = \a -> a >>> (arr g >>> arr f)  -- Arrow law
>               = \a -> (a >>> arr g) >>> arr f  -- Category law
>               = \a -> (fmapA g a) >>> arr f    -- definition of fmapA
>               = \a -> fmapA f (fmapA g a)       -- definition of fmapA
>               = \a -> (fmapA f) . (fmapA g) a   -- definition of (.)
>               = (fmapA f) . (fmapA g)           -- currying
>
> And here's the blog post that initially convinced me of the relationship
> between Arrows and Applicatives:
>
> http://just-bottom.blogspot.de/2010/04/programming-with-effects-story-so-far.html
>
> The alternative definition of Applicative as Monoidal can be found in
> the Typeclassopedia:
> https://wiki.haskell.org/Typeclassopedia#Alternative_formulation
>
> There are still holes to be filled, but these are more or less all the
> pieces of the puzzle I have so far.
>
> On 2015-12-14 16:41, Kim-Ee Yeoh wrote:
> > On Mon, Dec 14, 2015 at 10:10 PM, Erik Hesselink <hesselink at gmail.com>
> > wrote:
> >
> > Every Arrow is a Functor through:
> >>     fmapA :: Arrow arr => (a -> b) -> arr i a -> arr i b
> >>     fmapA f a = arr f . a
> >>
> >> Right?
> >>
> > That's one of the missing holes in Martin's claim.
> >
> > In cases like this, it would help to avoid any risk that the usual abuse
> of
> > language brings. So an arrow is not a functor but it does give rise to
> one.
> > More precisely, there would be an instance Arrow a => Functor (a b).
> >
> > -- Kim-Ee
> >
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151215/20008c6d/attachment.html>