[Haskell-cafe] Applicative banana brackets

[martin]

Yes, I know, my sketch is like a swiss cheese. Also, I apologize for my
abuse of language. My excuse is that my training did not involve the
precise terms used in English proofs. (It's not my first language, after
all.) 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 ...

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:

# 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
>