Re: [Haskell-cafe] Applicative banana brackets

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