容器索引：数学基础答案

【问题标题】：Indexing into containers: the mathematical underpinnings容器索引：数学基础
【发布时间】：2016-04-16 17:44:36
【问题描述】：

当你想从数据结构中拉出一个元素时，你必须给出它的索引。但是index的含义取决于数据结构本身。

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。

事实上，对于定义为多项式双函子的不动点的函子，我已经成功地实现了!。我不会详细介绍，但是当f 是Indexed2 的实例时，Fix f 可以成为Indexed 的实例...

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（我真的不需要）才能回答这个问题？

【问题讨论】：

我真的不认为列表是按数字索引的（这个Nothing 相当难看）。对我来说，xs 的列表由Fin (length xs) 或this 之类的东西索引。那么索引只是相应容器中的位置。对于列表Shape = ℕ 和Position = Fin，即您得到的正是Fin (length xs)，因为列表的形状就是它的长度。

标签： haskell functor generic-programming

【解决方案1】：

似乎类型的索引是构造函数集的索引，然后是表示该构造函数的乘积的索引。这可以很自然地实现，例如generics-sop.

首先，您需要一种数据类型来将可能的索引表示为产品的单个元素。这可能是指向a 类型元素的索引，或指向g b 类型的索引 - 这需要指向g 的索引和指向b 中a 类型元素的索引。这是用以下类型编码的：

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 中的量化可防止构造坏事，例如指向data X x = X Int x 中的第一个Int 的索引，其中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]

【讨论】：