Indeksowanie w kontenerach: podstawy matematyczne

Question

Jeśli chcesz wyciągnąć element ze struktury danych, musisz podać jego indeks. Ale znaczenie tego parametru zależy od samej struktury danych.

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

Na przykład ...

Elementy na liście mają pozycji numerycznych.

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

Elementy w drzewie binarnym są identyfikowane za pomocą sekwencji wskazówek.

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 

Szukasz czegoś w drzewa różanego wiąże ustąpię poziomy jeden na raz wybierając drzewo z lasu na każdym poziomie.

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) 

Wydaje się, że indeks danego typu produktu to suma (z informacją, której ramię produktu patrzeć), indeks elementu jest typ jednostki, a indeks typu zagnieżdżonego jest produkt (informujący, gdzie szukać w typie zagnieżdżonym). Kwoty wydają się być jedynymi, które nie są w jakiś sposób powiązane z derivative. Indeks sumy jest również sumą - informuje, która część sumy, którą użytkownik ma nadzieję znaleźć, i jeśli to oczekiwanie zostanie naruszone, pozostanie ci garstka z Nothing.

Rzeczywiście, odniosłem pewien sukces, wprowadzając generalnie ! dla funktorów zdefiniowanych jako stały punkt wielomianu dwufunkcyjnego. Nie będę wchodzić w szczegóły, ale Fix f można instancję Indexed gdy f jest instancją 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 

... i okazuje się, można zdefiniować instancję Indexed2 dla każdego bloków konstrukcyjnych bifunctor.

Ale co się naprawdę dzieje? Jaki jest podstawowy związek między funktorem a jego indeksem? Jak to się ma do pochodnej funktora? Czy konieczne jest zrozumienie theory of containers (której tak naprawdę nie mam), aby odpowiedzieć na to pytanie?

Answer 1

Wygląda na to, że indeks w typie jest indeksem do zestawu konstruktorów, po indeksie do produktu reprezentującego ten konstruktor. To może być zrealizowane całkiem naturalnie z np. generics-sop.

Najpierw potrzebujesz typu danych do przedstawienia możliwych wskaźników w jednym elemencie produktu. Może to być indeks wskazujący na element typu a, lub indeks wskazujący na coś typu g b - który wymaga wskaźnika wskazującego na g i indeksu wskazującego na element typu a w przypadku elementu typu a.To jest kodowany z następujących typów:

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 = ... 

Sam wskaźnik jest tylko suma (realizowane przez NS dla n-ary sumy) kwot nad ogólnym reprezentacji typu (wybór konstruktora, wybór elementu konstruktora):

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

można pisać inteligentne konstruktorów dla różnych indeksach:

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) 

pamiętać, że np w przypadku listy nie można skonstruować indeksu (poza dnem) wskazującego na konstruktor [] - podobnie dla Tree i Empty lub konstruktorów zawierających wartości, których typem nie jest a lub coś zawierającego pewne wartości typu a. Kwantyfikacja pod numerem MkIx zapobiega błędom konstrukcyjnym, takim jak indeks wskazujący na pierwsze Int w data X x = X Int x, gdzie x jest tworzone na Int.

Realizacja funkcji indeksu jest dość proste, nawet jeśli typy są przerażające:

(!) :: (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 

Funkcja go porównuje konstruktor wskazywanego przez indeks i rzeczywistą konstruktora używanych przez typ. Jeśli konstruktory nie są zgodne, indeksowanie zwraca Nothing. Jeśli tak, faktyczne indeksowanie jest wykonywane - co jest trywialne w przypadku, gdy indeks wskazuje dokładnie Here, a w przypadku jakiejś podstruktury, obie operacje indeksowania muszą odnieść sukces jeden po drugim, który jest obsługiwany przez >>=.

I prosty test:

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