haskell - functors - Indexación en contenedores: los fundamentos matemáticos.

fmap haskell

Question

Cuando quiere sacar un elemento de una estructura de datos, tiene que dar su índice. Pero el significado del índice depende de la propia estructura de datos.

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

Por ejemplo...

Los elementos en una lista tienen posiciones numéricas.

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

Los elementos en un árbol binario se identifican por una secuencia de direcciones.

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

Buscar algo en un rosal implica bajar los niveles uno por uno seleccionando un árbol del bosque en cada nivel.

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 el índice de un tipo de producto es una suma (que le indica qué brazo del producto debe mirar), que el índice de un elemento es el tipo de unidad y que el índice de un tipo anidado es un producto (que le indica dónde debe buscar en el tipo anidado). Las sumas parecen ser las únicas que no están vinculadas de alguna manera al derivative . El índice de una suma también es una suma: te dice qué parte de la suma que el usuario espera encontrar, y si se viola esa expectativa, te quedas con un puñado de Nothing .

De hecho, tuve algo de éxito implementando ! genéricamente para funtores definidos como el punto fijo de un bifunctor polinomial. No entraré en detalles, pero Fix f se puede convertir en una instancia de Indexed cuando f es una instancia de Indexed2 ...

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

... y resulta que puede definir una instancia de Indexed2 para cada uno de los bloques de construcción bifunctor.

Pero, ¿qué está pasando realmente? ¿Cuál es la relación subyacente entre un funtor y su índice? ¿Cómo se relaciona con la derivada del funtor? ¿Es necesario comprender la teoría de los contenedores (que yo no, realmente) para responder esta pregunta?

Answer 1

Parece que el índice en el tipo es un índice en el conjunto de constructores, seguido por un índice en el producto que representa ese constructor. Esto se puede implementar de forma bastante natural, por ejemplo, con generics-sop .

Primero necesita un tipo de datos para representar índices posibles en un solo elemento del producto. Esto podría ser un índice que apunta a un elemento de tipo a , o un índice que apunta a algo de tipo gb , que requiere un índice que apunta a g un índice que apunta a un elemento de tipo a en b . Esto está codificado con el siguiente tipo:

import Generics.SOP

data ArgIx f x x'' where 
  Here :: ArgIx f x x 
  There :: (Generic (g x'')) => Ix g -> ArgIx f x x'' -> ArgIx f x (g x'') 

newtype Ix f = ...

El índice en sí es solo una suma (implementada por NS para la suma n-aria) de sumas sobre la representación genérica del tipo (elección del constructor, elección del elemento constructor):

newtype Ix f = MkIx (forall x . NS (NS (ArgIx f x)) (Code (f x)))

Puedes escribir constructores inteligentes para varios índices:

listIx :: Natural -> Ix [] 
listIx 0 = MkIx $ S $ Z $ Z Here 
listIx k = MkIx $ S $ Z $ S $ Z $ There (listIx (k-1)) Here  

treeIx :: [Bool] -> Ix Tree 
treeIx [] = MkIx $ S $ Z $ S $ Z Here 
treeIx (b:bs) = 
  case b of 
    True -> MkIx $ S $ Z $ Z $ There (treeIx bs) Here 
    False -> MkIx $ S $ Z $ S $ S $ Z $ There (treeIx bs) Here 

roseIx :: [Natural] -> Ix Rose 
roseIx [] = MkIx $ Z $ Z Here  
roseIx (k:ks) = MkIx $ Z $ S $ Z $ There (listIx k) (There (roseIx ks) Here)

Tenga en cuenta que, por ejemplo, en el caso de la lista, no puede construir un índice (no inferior) que apunte al constructor [] , del mismo modo para Tree y Empty , o constructores que contengan valores cuyo tipo no sea a o algo que contenga algunos valores de tipo a . La cuantificación en MkIx evita que las cosas malas de la construcción, como un índice que apunta al primer Int en los data X x = X Int x donde x se ejemplifica a Int .

La implementación de la función de índice es bastante sencilla, incluso si los tipos dan miedo:

(!) :: (Generic (f x)) => f x -> Ix f -> Maybe x 
(!) arg (MkIx ix) = go (unSOP $ from arg) ix where 

  atIx :: a -> ArgIx f x a -> Maybe x 
  atIx a Here = Just a 
  atIx a (There ix0 ix1) = a ! ix0 >>= flip atIx ix1 

  go :: (All SListI xss) => NS (NP I) xss -> NS (NS (ArgIx f x)) xss -> Maybe x 
  go (Z a) (Z b) = hcollapse $ hzipWith (/(I x) -> K . atIx x) a b 
  go (S x) (S x'') = go x x'' 
  go Z{} S{} = Nothing 
  go S{} Z{} = Nothing 

La función go compara el constructor al que apunta el índice y el constructor real utilizado por el tipo. Si los constructores no coinciden, la indexación devuelve Nothing . Si lo hacen, se realiza la indexación real, lo cual es trivial en el caso de que el índice apunte exactamente Here , y en el caso de alguna subestructura, ambas operaciones de indexación deben suceder una después de la otra, que es manejada por >>= .

Y una prueba sencilla:

>map (("hello" !) . listIx) [0..5]
[Just ''h'',Just ''e'',Just ''l'',Just ''l'',Just ''o'',Nothing]