Индексирование в контейнеры: математические основы

Question

Если вы хотите вытащить элемент из структуры данных, вы должны указать его индекс. Но значение индекса зависит от самой структуры данных.

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

Например ...

Элементы в списке имеют числовые позиции.

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

Элементы в двоичном дереве идентифицируются последовательностью направлений.

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 

Ищет что-то в розовом дереве влечет за собой уйдя уровни один за один раз, выбрав дерево из леса на каждом уровне.

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) 

Кажется, что индекс типа продукта является сумма (говорят вам, который рука продукта смотреть), индекс элемента является типом блока, а индекс вложенного типа продукт (рассказывающий, где искать вложенный тип). Суммы, кажется, единственные, которые никак не связаны с derivative. Индекс суммы также является суммой - он сообщает вам, какая часть суммы, которую пользователь надеется найти, и если это ожидание нарушено, вы останетесь с горсткой Nothing.

Фактически у меня был некоторый успех, реализующий ! в общем случае для функторов, определяемых как неподвижная точка полиномиального бифунтера. Я не буду вдаваться в подробности, но Fix f можно сделать экземпляр Indexed когда f является экземпляром 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 

... и оказывается, можно определить экземпляр Indexed2 для каждого бифункциональных строительных блоков.

Но что же происходит? Какова основная взаимосвязь между функтором и его индексом? Как это связано с производной функтора? Нужно ли понимать theory of containers (чего я не знаю), чтобы ответить на этот вопрос?

Answer 1

Похоже, что индекс в тип является индексом в набор конструкторов, следующий индексом в произведение, представляющее этот конструктор. Это может быть осуществлено вполне естественно, например, generics-sop.

Для начала вам нужен тип данных для представления возможных индексов в один элемент продукта. Это может быть индекс, указывающий на элемент типа a, или индекс, указывающий на что-то типа g b - для которого требуется указатель, указывающий на g и индекс, указывающий на элемент типа a в b.Это кодируется с использованием следующего вида:

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

Сам индекс является только сумма (осуществляется NS для п-арной суммы) сумм по родовым представления типа (выбор конструктора, выбор конструктора элемента):

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

Вы можете написать умные конструкторы для различных индексов:

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) 

Обратите внимание, что, например, в случае списка вы не можете построить индекс (non-bottom), указывающий на конструктор [] - также для Tree и Empty, или конструкторы, содержащие значения, тип которых не равен a, или что-то, содержащее некоторые значения типа a. Количественная оценка в MkIx предотвращает создание плохих вещей, таких как индекс, указывающий на первый Int в data X x = X Int x, где x был создан в Int.

Реализация функции индекса довольно проста, даже если типы страшно:

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

go функция сравнивает конструктор указывает индекс и фактического конструктора, используемого типа. Если конструкторы не совпадают, индексирование возвращает Nothing. Если это так, выполняется фактическое индексирование - что тривиально в том случае, если индекс указывает точно Here, а в случае какой-либо подструктуры обе операции индексирования должны выполняться один за другим, который обрабатывается >>=.

И простой тест:

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