Got it eventually. Thanks to
huzhepidarasa and "Applicative programming with effects" by McBride and Paterson.
So, let's see.
In Haskell, in Scala, and I don't know... in PHP? every monad is an applicative functor, with the help of lift2. But I could not figure out where does it come from?
Say we have a category C that has products a × b and power objects, b
a; an endofunctor T is called applicative if it is supplied with two natural transformations,
pure: a → T(a)
and
(*): T(ba) → T(b)T(a)
that have obvious properties.
The statement is that every monad is an applicative functor.
Turned out not every monad, but a strong one.
A strong monad is a monad that has a natural transformation
ta,b: a × T(b) → T(a×b)
with a bunch of good properties that could be found on wikipedia (are they called coherence? something like that - MacLane studied them eons ago).
Anyway, a strong monad is an applicative functor.
We already have
pure
; have to define
(*)
.
The trick is this.
Given a binary operation
f: a×b → c
then we will lift this binary operation (since we deal with a function of two parameters, the operation is called
lift2
) to
T(a)×T(b) → T(c)
Namely, we have
tT(a),b: T(a)×T(b) → T(T(a)×b)
T(flipT(a),b): T(T(a)×b) → T(b×T(a))
T(tb,T(a)): T(b×T(a)) → T(T(b×a))
T(T(flipb,a)): T(T(b×a)) → T(T(a×b))
T(T(f)):T(T(a×b)) → T(T(c))
mc: T(T(c)) → T(c)
Composing them, we will have the
lift2
we were looking for.
Now take
evala,b: a × ba → b
, and apply
lift2
We will have
T(a) × T(ba) → T(b)
; currying it, we get
(*): T(ba) → T(b)T(a)
This may be obvious from the fp point of view, but I am a categorist, not a functional programmer (although you should have seen the rich loops I've been writing lately in Scala), so I needed a sound proof, not just a sound of a proof.
Thank you.
Questions and remarks greatly welcome.