haskell - 索引到容器 : the mathematical underpinnings

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 的实例对于每个双仿函数构建 block 。

但到底发生了什么？仿函数与其索引之间的潜在关系是什么？它与仿函数的导数有何关系？是否需要了解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 实现 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)

请注意，例如在列表情况下，您不能构造指向 [] 的(非底部)索引。构造函数 - 同样适用于 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]