How to explain/understand brackets of applicative functor [[f u1... un]]?
In it's simplest, original form, $[\![f\ x \ y]\!]$ just means $\eta(f)\circledast x \circledast y$ where $\circledast$ is what Haskell calls &lt;*&gt; 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 (+) &lt;*&gt; pure 3 &lt;*&gt; 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.