索引到容器:数学基础

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)

似乎产品类型的索引是一个总和(告诉你要看产品的哪一部分),元素的索引是单元类型,嵌套类型的索引是一个产品(告诉你在哪里看看嵌套类型).总和似乎是唯一一个与衍生物没有联系的人.和的索引也是一个总和 - 它告诉你用户希望找到的总和的哪一部分,如果这个期望被违反,你只剩下少数Nothing.

事实上,我已经成功地实现!了定义为多项式bifunctor的固定点的仿函数.我不会详细介绍,但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为每个bifunctor构建块定义一个实例.

但究竟发生了什么？仿函数与其索引之间的基本关系是什么？它与仿函数的衍生物有什么关系？是否需要理解容器理论(我不是,真的)才能回答这个问题？

Answer 1

似乎类型的索引是构造函数集的索引，后跟代表该构造函数的产品的索引。这可以很自然地用例如generics-sop实现。

首先，您需要一个数据类型来表示产品单个元素中的可能索引。这可以是指向类型的元素的索引，也可以是指向类型的a东西g b的索引-这需要指向in g的索引和指向ain中的元素的索引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)

请注意，例如在列表的情况下，您不能构造指向构造函数的（非底部）索引[]-像for Tree和Empty，或者构造函数包含类型不是的a值或某些包含类型type的值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]