Applicative Functor (a.k.a. Strong Lax Monoidal Functor) [DRAFT]
Created at 2016-05-05T04:13:43.000Z

Summery

  • Motivation

  • Use case:

  • Theoretical exposition:

The most important line:

pure function applied to funny arguments

  • Compositionality of Applicative Functor comes from Compositionality of strong lax monoidal functor.

  • I don't know how to deal with usual functor for additional type constructor in language.

Notes

  • Original motivation for giving semantics to effectful computation by _Monad_ is:
    • equational reasoning
  • But, by removing monadic equation constraint, what _Applicative_ does is to give semantics to effectful computation which could bring:
    • faster effect resolution (e.g. reader, parallel computation, Traversable),
    • "practically interesting" effect resolution (e.g. matrix transposition).
  • I don't feel "more than one free variable" is not the point of strength required for applicative...

  • In Haskell (or in $Sets$), any Functor is strong. So, I think strong-ness shouldn't be emphasized in this discussion, it's confusing.

  • What kind of "formal language" are we talking about for _Applicative_ computation?
    • it will be "language without let (a.k.a binding)"
    • what's the crucial difference of "join" and "crushing effect (traverse effect along data structure)"?
    • traverse doesn't require "binding" ?
    • -

References