Indexing into containers: the mathematical underpinnings
<p>When you want to pull an element out of a data structure, you have to give its index. But the meaning of <em>index</em> depends on the data structure itself.</p>

<pre><code>class Indexed f where
    type Ix f
    (!) :: f a -&gt; Ix f -&gt; Maybe a  -- indices can be out of bounds
</code></pre>

<p>For example...</p>

<p>Elements in a list have numeric positions.</p>

<pre><code>data Nat = Z | S Nat
instance Indexed [] where
    type Ix [] = Nat
    [] ! _ = Nothing
    (x:_) ! Z = Just x
    (_:xs) ! (S n) = xs ! n
</code></pre>

<p>Elements in a binary tree are identified by a sequence of directions.</p>

<pre><code>data Tree a = Leaf | Node (Tree a) a (Tree a)
data TreeIx = Stop | GoL TreeIx | GoR TreeIx  -- equivalently [Bool]
instance Indexed Tree where
    type Ix Tree = TreeIx
    Leaf ! _ = Nothing
    Node l x r ! Stop = Just x
    Node l x r ! GoL i = l ! i
    Node l x r ! GoR j = r ! j
</code></pre>

<p>Looking for something in a rose tree entails stepping down the levels one at a time by selecting a tree from the forest at each level.</p>

<pre><code>data Rose a = Rose a [Rose a]  -- I don't even like rosé
data RoseIx = Top | Down Nat RoseIx  -- equivalently [Nat]
instance Indexed Rose where
    type Ix Rose = RoseIx
    Rose x ts ! Top = Just x
    Rose x ts ! Down i j = ts ! i &gt;&gt;= (! j)
</code></pre>

<p>It seems that the index of a product type is a sum (telling you which arm of the product to look at), the index of an element is the unit type, and the index of a nested type is a product (telling you where to look in the nested type). Sums seem to be the only one which aren't somehow linked to the <a href="https://stackoverflow.com/questions/25554062/zipper-comonads-generically">derivative</a>. The index of a sum is also a sum - it tells you which part of the sum the user is hoping to find, and if that expectation is violated you're left with a handful of <code>Nothing</code>.</p>

<p>In fact I had some success implementing <code>!</code> generically for functors defined as the fixed point of a polynomial bifunctor. I won't go into detail, but <code>Fix f</code> can be made an instance of <code>Indexed</code> when <code>f</code> is an instance of <code>Indexed2</code>...</p>

<pre><code>class Indexed2 f where
    type IxA f
    type IxB f
    ixA :: f a b -&gt; IxA f -&gt; Maybe a
    ixB :: f a b -&gt; IxB f -&gt; Maybe b
</code></pre>

<p>... and it turns out you can define an instance of <code>Indexed2</code> for each of the bifunctor building blocks.</p>

<p>But what's really going on? What is the underlying relationship between a functor and its index? How does it relate to the functor's derivative? Does one need to understand the <a href="https://en.wikipedia.org/wiki/Container_(type_theory)" rel="nofollow noreferrer">theory of containers</a> (which I don't, really) to answer this question?</p>