索引到容器:数学基础 [英] Indexing into containers: the mathematical underpinnings

问题描述

要从数据结构中提取元素时，必须提供其索引.但是 index 的含义取决于数据结构本身.

When you want to pull an element out of a data structure, you have to give its index. But the meaning of index depends on the data structure itself.

class Indexed f where
    type Ix f
    (!) :: f a -> Ix f -> Maybe a  -- indices can be out of bounds

例如...

列表中的元素具有数字位置.

Elements in a list have numeric positions.

data Nat = Z | S Nat
instance Indexed [] where
    type Ix [] = Nat
    [] ! _ = Nothing
    (x:_) ! Z = Just x
    (_:xs) ! (S n) = xs ! n

二叉树中的元素由一系列方向标识.

Elements in a binary tree are identified by a sequence of directions.

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

在玫瑰树中寻找某种东西需要通过从每个级别的森林中选择一棵树来一次降低一个级别.

Looking for something in a rose tree entails stepping down the levels one at a time by selecting a tree from the forest at each level.

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.

It seems that the index of a product type is a sum (telling you which arm of the product to look at), the index of an element is the unit type, and the index of a nested type is a product (telling you where to look in the nested type). Sums seem to be the only one which aren't somehow linked to the derivative. The index of a sum is also a sum - it tells you which part of the sum the user is hoping to find, and if that expectation is violated you're left with a handful of Nothing.

实际上，我对于将定义为多项式bifunctor的不动点的函子普遍实现!取得了一些成功.我不会详细介绍，但是当f是Indexed2的实例时，可以将Fix f做成Indexed的实例...

In fact I had some success implementing ! generically for functors defined as the fixed point of a polynomial bifunctor. I won't go into detail, but Fix f can be made an instance of Indexed when f is an instance of 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

...事实证明，您可以为每个bifunctor构建块定义Indexed2的实例.

... and it turns out you can define an instance of Indexed2 for each of the bifunctor building blocks.

但是到底是怎么回事?函子及其索引之间的潜在关系是什么?它与函子的导数有什么关系?是否需要了解容器理论(我实际上不是， )回答这个问题?

But what's really going on? What is the underlying relationship between a functor and its index? How does it relate to the functor's derivative? Does one need to understand the theory of containers (which I don't, really) to answer this question?

推荐答案

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

It seems like the index into the type is an index into the set of constructors, following by an index into the product representing that constructor. This can be implemented quite naturally with e.g. generics-sop.

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

First you need a datatype to represent possible indices into a single element of the product. This could be an index pointing to an element of type a, or an index pointing to something of type g b - which requires an index pointing into g and an index pointing to an element of type a in b. This is encoded with the following type:

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元和).

The index itself is just a sum (implemented by NS for n-ary sum) of sums over the generic representation of the type (choice of constructor, choice of constructor element):

newtype Ix f = MkIx (forall x . NS (NS (ArgIx f x)) (Code (f x)))

您可以为各种索引编写智能的构造函数:

You can write smart constructors for various indices:

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.

Note that e.g. in the list case, you cannot construct an (non-bottom) index pointing to the [] constructor - likewise for Tree and Empty, or constructors containing values whose type is not a or something containing some values of type a. The quantification in MkIx prevents the construction bad things like an index pointing to the first Int in data X x = X Int x where x is instantiated to Int.

即使类型很可怕，索引函数的实现也非常简单:

The implementation of the index function is fairly straightforward, even if the types are scary:

(!) :: (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的情况下这是微不足道的，并且在某些子结构的情况下，两个索引编制操作都必须一个接一个地接续，这由>>=处理.

The go function compares the constructor pointed to by the index and the actual constructor used by the type. If the constructors don't match, the indexing returns Nothing. If they do, the actual indexing is done - which is trivial in the case that the index points exactly Here, and in the case of some substructure, both indexing operations must succeed one after the other, which is handled by >>=.

一个简单的测试:

>map (("hello" !) . listIx) [0..5]
[Just 'h',Just 'e',Just 'l',Just 'l',Just 'o',Nothing]

这篇关于索引到容器:数学基础的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！