分度容器:数学基础

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)

产品类型的索引似乎是一个和(告诉您要查看产品的哪个分支)，元素的索引是单元类型，嵌套类型的索引是产品(告诉您在嵌套类型中的位置)。数字似乎是唯一一个与导数没有某种联系的。一个sum的索引也是一个sum -它告诉您用户希望找到的和的哪一部分，如果这个期望被违反了，那么剩下的是少量的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实例。

但到底是怎么回事？函子和它的索引之间的基本关系是什么？它与函子的导数有什么关系？你是否需要理解容器理论 (我真的不理解)才能回答这个问题？

Answer 1

似乎对类型的索引是对构造函数集的索引，后面是对表示该构造函数的产品的索引。这可以很自然地通过例如仿制药-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)

注意，例如，在list情况下，您不能构造指向[]构造函数的(非底部的)索引--对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]