Indexação em contêineres: os fundamentos matemáticos

Quando você deseja extrair um elemento de uma estrutura de dados, é necessário fornecer seu índice. Mas o significado deíndice depende da própria estrutura de dados.

class Indexed f where
    type Ix f
    (!) :: f a -> Ix f -> Maybe a  -- indices can be out of bounds

Por exemplo...

Os elementos de uma lista têm posições numéricas.

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

Os elementos em uma árvore binária são identificados por uma sequência de direções.

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

Procurar algo em uma roseira implica descer os níveis, um de cada vez, selecionando uma árvore da floresta em cada nível.

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 >>= (! j)

Parece que o índice de um tipo de produto é uma soma (informando em qual ramo do produto examinar), o índice de um elemento é o tipo de unidade e o índice de um tipo aninhado é um produto (informando onde procure no tipo aninhado). As somas parecem ser as únicas que não estão de alguma forma ligadas aoderivado. O índice de uma soma também é uma soma - indica qual parte da soma o usuário espera encontrar e, se essa expectativa for violada, você terá um punhado deNothing.

Na verdade, eu tive algum sucesso implementando! genericamente para functores definidos como o ponto fixo de um bifuncor polinomial. Não vou entrar em detalhes, masFix f pode ser feita uma instância deIndexed quandof é uma instância deIndexed2...

class Indexed2 f where
    type IxA f
    type IxB f
    ixA :: f a b -> IxA f -> Maybe a
    ixB :: f a b -> IxB f -> Maybe b

... e você pode definir uma instância deIndexed2 para cada um dos blocos de construção do bifunctor.

Mas o que realmente está acontecendo? Qual é a relação subjacente entre um functor e seu índice? Como isso se relaciona com a derivada do functor? É necessário entender oteoria dos recipientes (o que realmente não faço) para responder a essa pergunta?

questionAnswers(1)

yourAnswerToTheQuestion