2014-07-01

Forcing rank

\(
\newcommand{\len}{\text{len}}
\newcommand{\r}{\rightarrow}
\newcommand{\d}{\mathbin{\cdot}}
\)By default, functions that act upon functors are not mapped at all. So, for instance, \(\len\ \{\{1,4,6,9\},\{2\},\{5,7\}\} = 3\). But what if what we actually wanted was \(\{1,2,4\}\)? (Notice that the set has been resorted. Notice also that if two of the inner sets had the same length, the result would have been shorter than the initial list, since duplicates are removed.)

This is where we use the prefixed subscript. This acts differently based on whether or not the number is negative (it must be an integer, by the way). For positive \(n\), \({}_nf\) is the function \(f\) applied to the parts of rank \(n\) with respect to the functor \(f\) handles. \({}_{n-0}f = {}^n\text{fmap}\ f\). \({}_0f\) is \(f\) applied as if \(f\) didn't handle the functor it does (the values it gets will be implicitly lifted).

But what is rank? I should have explained this before. The rank of a value, with respect to some functor, is how many times functors of that type can be “unwrapped” from the value. For example, a value of type \(\{\{\mathbb{N}\}\}\) (as in the first example) has rank 2, since it is wrapped twice in the Set functor. A value of type \((a\r b\r c)\r(a\r b)\r a\r c\) has rank 3, since it has been wrapped in the Function functors \(((a\r b\r c)\r)\), \(((a\r b)\r)\) and \((a\r)\). This is the type of the \(S\) combinator, \(S\ f\ g\ x = f\ x\ (g\ x)\), which, as you can see, takes 3 arguments.

So, to achieve the result of our first example, we can do either \({}_1\len\ A\) (applying to the rank-1 cells) or \({}_{1-0}\len\ A\) (applying to the cells 1 rank below the given value's rank). We can also distinguish between \({}^2D\left({}_\d^3\right)\) and \({}_1{}^2D\left({}_\d^3\right)\):
\[
 \begin{aligned}
{}^2D\left({}_\d^3\right) &{}= (DD)\left({}_\d^3\right) \quad & {}_1{}^2D\left({}_\d^3\right) &{}= \text{fmap}\ {}^2\ D\ {}_\d^3 \\
&{}= D\left(D\left({}_\d^3\right)\right) & &{}= {}^2\left(D\left({}_\d^3\right)\right) \\
&{}= D\left(3\d{}_\d^2\right) & &{}= {}^2\left(3\d{}_\d^2\right) \\
&{}= (6\d{}) & &{}= \left(3\d{}_\d^2\right)\left(3\d{}_\d^2\right) \\
&&&{}= 3\mathbin{\d}{}{}_\d^2\left(3\d{}_\d^2\right) \\
&&&{}= 27\d{}_\d^4
\end{aligned}
\]Okay, it's rare to use this explicitly. But it's there.

No comments:

Post a Comment