# How to explain/understand brackets of applicative functor [[f u1… un]]?

I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside applicative functors. These brackets are introduced and somehow explained in "Functional Pearl: Applicative programming with effects" http://strictlypositive.org/IdiomLite.pdf. I understand what applicative functor is and what what is functor generally (both in category theory and Haskell) but I still can not understand the meaning and value of these brackets. I understand the sentence idiomatic expression [[f x y]] means ηf * ηx * y, or, alternatively, map (f x) y - that means that [[F(tau)]] is sitting inside brackets, but I can not understand the difference between F(tau) and [[F(tau)]] in brackets (see page 4 of AACG article about context and notation). Also - brackets are not always used with 3 arguments, sometimes there are even on or none arguments!

Do those brackets have meaning, explanation and use in Haskell world? Any explanation - rigorous or not, associative and free-style of not is really appreciated.

pure (+) <*> Just 3 <*> Just 5


Its fine, but what benefit can we get by applying brackets [[]] around this expression, what additional meaning such application created?

In it's simplest, original form, $[\![f\ x \ y]\!]$ just means $\eta(f)\circledast x \circledast y$ where $\circledast$ is what Haskell calls <*> and $\eta$ is what Haskell calls pure. Of course, this is only type correct if $x$, and $y$ have types like $\mathcal{F}(\dots)$ where $\mathcal{F}$ is an applicative functor. If they don't, we can be a bit smarter and automatically use $\eta$/pure to "lift" them to that type. From there, the translation can simply be $[\![f\ x_1\dots x_n]\!]\leadsto [\![f]\!]_1\circledast [\![x_1]\!]_1\circledast\cdots\circledast [\![x_n]\!]_1$ where $[\![e]\!]_1$ is either $e$ or $\eta(e)$ depending on the type of $e$. More systematically, $[\![e\ x]\!]\leadsto [\![e]\!]\circledast [\![x]\!]_1$ where $[\![e]\!] = [\![e]\!]_1$ when $e$ is not an application. You can easily imagine a variation that recursively applies the transformation.
The idiom brackets are just for convenience. The example you show of an applicative expression would become [[3 + 5]] using idiom brackets which is quite a bit shorter and more readable than pure (+) <*> pure 3 <*> pure 5 (which is in this case just pure (3 + 5) and thus is a fairly trivial case).
I have no idea what you mean by [[F(tau)]]. Idiom brackets don't apply to types.