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

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

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)

Кажется, что индекс типа продукта представляет собой сумму (указывающую, какой рычаг продукта следует посмотреть), индекс элемента является типом единицы, а индекс вложенного типа - это продукт (рассказывающий вы, где искать в вложенном типе). Суммы, кажется, единственные, которые никак не связаны с производным . Индекс суммы также является суммой - он сообщает вам, какая часть суммы, которую пользователь надеется найти, и если это ожидание нарушено, вы останетесь с горсткой 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 для каждого из бифуркационных строительных блоков.

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

Ответы

Ответ 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 для n-арной суммы) сумм по общему представлению типа (выбор конструктора, выбор элемента конструктора):

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]