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

Question

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.

http://learnyouahaskell.com/functors-applicative-functors-and-monoids contains example:

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?

Answer 1

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.

There's a quasi-quoter that implements a notation similar to idiom brackets. Idiom brackets are also implemented by the Strathclyde Haskell Enhancement (SHE) which is made by the person who originally introduced the notation and author of that Functional Pearl, Conor McBride.