Indizierung in Container: die mathematischen Grundlagen

Question

Wenn Sie ein Element aus einer Datenstruktur ziehen möchten, müssen Sie seinen Index angeben. Aber die Bedeutung von Index hängt von der Datenstruktur selbst ab.

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

Zum Beispiel ...

Elemente in einer Liste finden numerische Positionen.

Elemente in einem binären Baum werden durch eine Abfolge von Richtungen identifiziert.

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 

die Suche nach etwas in einem Rosenbaum bringt auf jeder Ebene, indem Sie einen Baum aus dem Wald zu einer Zeit, die Ebenen einen Rücktritt.

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) 

Es scheint, dass der Index eines Produkttyps ist eine Summe (sagen Ihnen, welche Arm des Produkts zu sehen), der Index eines Elements ist die Art der Einheit und der Index eines verschachtelten Typs ein Produkt (sagt Ihnen, wo Sie im verschachtelten Typ suchen). Summen scheinen die einzigen zu sein, die nicht irgendwie mit dem derivative verknüpft sind. Der Index einer Summe ist auch eine Summe - er sagt Ihnen, welcher Teil der Summe der Benutzer zu finden hofft, und wenn diese Erwartung verletzt wird, bleiben Sie mit einer Handvoll Nothing.

In der Tat hatte ich einige Erfolge bei der Implementierung ! generisch für Funktoren definiert als der Fixpunkt eines Polynoms Bifunctor. Ich werde nicht ins Detail gehen, aber Fix f kann eine Instanz von Indexed gemacht werden, wenn f eine Instanz von Indexed2 ist ...

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 

... und es stellt sich heraus, Sie eine Instanz von Indexed2 für jede definieren der Bifunktorfelder.

Aber was ist wirklich los? Was ist die zugrunde liegende Beziehung zwischen einem Funktor und seinem Index? Wie verhält es sich mit dem Derivat des Funktors? Muss man die theory of containers (die ich nicht wirklich verstehe) verstehen, um diese Frage zu beantworten?

Answer 1

Es scheint, als wäre der Index in den Typ ein Index in die Menge der Konstruktoren, gefolgt von einem Index in das Produkt, das diesen Konstruktor darstellt. Dies kann ganz natürlich mit z.B. generics-sop.

Zuerst benötigen Sie einen Datentyp, um mögliche Indizes in einem einzelnen Element des Produkts darzustellen. Dies könnte ein Index sein, der auf ein Element des Typs a, oder einen Index verweist, der auf etwas vom Typ g b verweist. Dies erfordert einen Index, der auf g zeigt, und einen Index, der auf ein Element des Typs a in b verweist.Dies wird mit dem folgenden Typ codiert:

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

Der Index selbst ist nur eine Summe (implementiert durch NS für n-ary sum) der Summen über die generische Darstellung des Typs (Wahl der Konstruktor Wahl des Konstruktors Elements):

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

Sie intelligente Konstrukteure für verschiedene Indizes schreiben:

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) 

Beachten Sie, dass zB Im Listenfall können Sie keinen (nicht unteren) Index erstellen, der auf den []-Konstruktor verweist - ebenfalls für Tree und Empty oder Konstruktoren, die Werte enthalten, deren Typ nicht a oder etwas ist, das Werte vom Typ a enthält. Die Quantifizierung in MkIx verhindert die Konstruktion schlechter Dinge wie ein Index, der auf die erste Int in data X x = X Int x zeigt, wo x in Int instanziiert wird.

Die Umsetzung der Index-Funktion ist recht einfach, auch wenn die Typen sind beängstigend:

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

Die go Funktion vergleicht der Konstruktor auf dem durch den Index und der tatsächlichen Konstruktor vom Typ verwendet. Wenn die Konstruktoren nicht übereinstimmen, gibt die Indizierung Nothing zurück. Ist dies der Fall, wird die eigentliche Indizierung durchgeführt - was für den Fall, dass der Index exakt auf Here zeigt, trivial ist, und im Fall einer Unterstruktur müssen beide Indizierungsoperationen nacheinander ausgeführt werden, was von >>= gehandhabt wird.

Und ein einfacher Test:

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