Lập chỉ mục vào vùng chứa: nền tảng toán học

Question

Khi bạn muốn lấy phần tử ra khỏi cấu trúc dữ liệu, bạn phải cung cấp chỉ mục của nó. Nhưng ý nghĩa của chỉ số phụ thuộc vào cấu trúc dữ liệu.

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

Ví dụ ...

yếu tố trong một danh sách có vị trí số.

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

Các phần tử trong cây nhị phân được xác định theo trình tự chỉ đường.

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 

Tìm kiếm thứ gì đó trong cây hồng đòi hỏi phải giảm từng cấp một bằng cách chọn cây từ rừng ở mỗi cấp.

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) 

Dường như chỉ số của một loại sản phẩm là một sum (nói cho bạn mà cánh tay của sản phẩm để nhìn vào), chỉ số của một phần tử là loại đơn vị, và chỉ số của một loại lồng nhau là một sản phẩm (cho bạn biết nơi để tìm trong loại lồng nhau). Số tiền có vẻ là người duy nhất không được liên kết với số điện thoại derivative. Chỉ mục của tổng cũng là một tổng - nó cho bạn biết phần nào của tổng số người dùng hy vọng sẽ tìm thấy, và nếu kỳ vọng đó bị vi phạm, bạn còn lại với một số ít là Nothing.

Trong thực tế, tôi đã thực hiện một số thành công khi thực hiện ! chung cho các functors được định nghĩa là điểm cố định của một bifunctor đa thức. Tôi sẽ không đi sâu vào chi tiết, nhưng Fix f thể được thực hiện một thể hiện của Indexed khi f là một thể hiện của 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 

... và nó quay ra bạn có thể xác định một thể hiện của Indexed2 cho mỗi của các khối xây dựng bifunctor.

Nhưng điều gì đang thực sự xảy ra? Mối quan hệ cơ bản giữa functor và chỉ mục của nó là gì? Làm thế nào nó liên quan đến đạo hàm của functor? Có cần phải hiểu theory of containers (mà tôi không, thực sự) để trả lời câu hỏi này?

Answer 1

Dường như chỉ mục vào loại là một chỉ mục trong tập hợp các nhà xây dựng, tiếp theo là chỉ mục vào sản phẩm đại diện cho hàm tạo đó. Điều này có thể được triển khai hoàn toàn tự nhiên, ví dụ: generics-sop.

Trước tiên, bạn cần một kiểu dữ liệu để thể hiện các chỉ mục có thể có thành một phần tử duy nhất của sản phẩm. Đây có thể là chỉ mục trỏ đến một phần tử thuộc loại a, hoặc chỉ mục trỏ đến một loại nào đó g b - yêu cầu chỉ mục trỏ đến g và chỉ mục trỏ đến một phần tử thuộc loại a trong b.Đây được mã hóa với các loại sau đây:

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 = ... 

Chỉ số bản thân chỉ là một khoản tiền (thực hiện bởi NS để tổng hợp n-ary) của khoản tiền so với đại diện chung của các loại (Lựa chọn hàm tạo, sự lựa chọn của nguyên tố constructor):

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

Bạn có thể viết constructors thông minh cho các chỉ số khác nhau:

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) 

Lưu ý rằng ví dụ trong trường hợp danh sách, bạn không thể xây dựng một chỉ mục (không phải dưới cùng) trỏ đến hàm tạo [] - tương tự như vậy cho Tree và Empty hoặc các nhà xây dựng chứa các giá trị có loại không a hoặc cái gì đó chứa một số giá trị loại a. Định lượng trong MkIx ngăn các công trình xây dựng xấu như chỉ mục trỏ đến số Int đầu tiên trong data X x = X Int x trong đó x được khởi tạo đến Int.

Việc thực hiện chức năng chỉ số này khá đơn giản, ngay cả khi các loại rất đáng sợ:

(!) :: (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 

Chức năng go so sánh các nhà xây dựng được trỏ đến bởi chỉ số và các nhà xây dựng thực tế được sử dụng bởi các loại. Nếu các nhà thầu không khớp, chỉ mục trả về Nothing. Nếu chúng thực hiện, việc lập chỉ mục thực tế được thực hiện - đó là tầm thường trong trường hợp chỉ mục chính xác là Here và trong trường hợp của một số cấu trúc con, cả hai hoạt động lập chỉ mục phải thành công sau khi được xử lý bởi >>=.

Và một thử nghiệm đơn giản:

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