haskell - 为长度索引列表实现 zipper

Question

我正在尝试为长度索引列表实现一种 zipper ，它将返回列表的每个项目与删除该元素的列表配对。例如。对于普通列表:

zipper :: [a] -> [(a, [a])]
zipper = go [] where
    go _    []     = []
    go prev (x:xs) = (x, prev ++ xs) : go (prev ++ [x]) xs

以便

> zipper [1..5]
[(1,[2,3,4,5]), (2,[1,3,4,5]), (3,[1,2,4,5]), (4,[1,2,3,5]), (5,[1,2,3,4])]

我目前尝试为长度索引列表实现相同的功能:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Zero | Succ Nat
type One = Succ Zero

type family (+) (a :: Nat) (b :: Nat) :: Nat
type instance (+) Zero n = n
type instance (+) (Succ n) m = Succ (n + m)


data List :: Nat -> * -> * where
    Nil  :: List Zero a
    Cons :: a -> List size a -> List (Succ size) a

single :: a -> List One a
single a = Cons a Nil

cat :: List a i -> List b i -> List (a + b) i
cat Nil ys = ys
cat (Cons x xs) ys = Cons x (xs `cat` ys)

zipper :: List (Succ n) a -> List (Succ n) (a, List n a)
zipper = go Nil where

    go :: (p + Zero) ~ p
        => List p a -> List (Succ q) a -> List (Succ q) (a, List (p + q) a)
    go prev (Cons x Nil) = single (x, prev)
    go prev (Cons x xs) = (x, prev `cat` xs) `Cons` go (prev `cat` single x) xs

这感觉应该相当简单，但似乎没有任何方法可以传达给 GHC，例如 +是可交换和关联的，或者零是身份，我遇到了很多问题，类型检查器(可以理解)提示它无法确定 a + b ~ b + a或者那个 a + Zero ~ a .

我是否需要添加某种证明对象( data Refl a b where Refl :: Refl a a 等)，或者有什么方法可以通过添加更明确的类型签名来实现这一目标？

Answer 1

结盟
依赖类型编程就像是做两个被某些流氓粘在一起的拼图。不那么隐喻，我们在值级别和类型级别表示同时计算，我们必须确保它们的兼容性。当然，我们每个人都是自己的流氓，所以如果我们能把拼图粘在一起，我们会更轻松。当您看到类型修复的证明义务时，您可能会问

Do I need to add some sort of proof objects (data Refl a b where Refl :: Refl a a et al.) or is there some way to make this work with just adding more explicit type signatures?

但是您可能首先考虑值级和类型级计算在哪些方面不一致，以及是否有希望使它们更接近。
一个办法
这里的问题是如何从向量中计算选择的向量(长度索引列表)。所以我们想要一些带有类型的东西

List (Succ n) a -> List (Succ n) (a, List n a)

其中每个输入位置的元素被其兄弟元素的一个较短的向量修饰。建议的方法是从左到右扫描，在右侧增长的列表中累积大 sibling ，然后在每个位置与小 sibling 连接。右边越来越多的列表总是令人担忧，尤其是当 Succ因为长度与 Cons 对齐在左边。连接的需要需要类型级加法，但右端事件产生的算术与加法的计算规则不一致。稍后我会回到这种风格，但让我们再考虑一下。
在我们进入任何基于累加器的解决方案之前，让我们先尝试一下沼泽标准结构递归。我们有“一个”案例和“更多”案例。

picks (Cons x xs@Nil)         = Cons (x, xs) Nil
picks (Cons x xs@(Cons _ _))  = Cons (x, xs) (undefined (picks xs))

在这两种情况下，我们都将第一个分解放在前面。在第二种情况下，我们已经检查过尾部是非空的，所以我们可以询问它的选择。我们有

x         :: a
xs        :: List (Succ n) a
picks xs  :: List (Succ n) (a, List n a)

我们想要

Cons (x, xs) (undefined (picks xs))  :: List (Succ (Succ n)) (a, List (Succ n) a)
              undefined (picks xs)   :: List (Succ n) (a, List (Succ n) a)

所以 undefined需要是通过重新附加 x 来增加所有兄弟列表的函数在左端(左端很好)。所以，我定义了 Functor List n 的实例

instance Functor (List n) where
  fmap f Nil          = Nil
  fmap f (Cons x xs)  = Cons (f x) (fmap f xs)

我诅咒 Prelude和

import Control.Arrow((***))

这样我就可以写

picks (Cons x xs@Nil)         = Cons (x, xs) Nil
picks (Cons x xs@(Cons _ _))  = Cons (x, xs) (fmap (id *** Cons x) (picks xs))

它可以在没有任何添加的情况下完成工作，更不用说证明了。
变化
我对在两行中做同样的事情感到恼火，所以我试图摆脱它:

picks :: m ~ Succ n => List m a -> List m (a, List n a)  -- DOESN'T TYPECHECK
picks Nil          = Nil
picks (Cons x xs)  = Cons (x, xs) (fmap (id *** (Cons x)) (picks xs))

但是GHC积极解决约束，拒绝让 Nil作为一种模式。这样做是正确的:我们真的不应该在我们静态知道 Zero ~ Succ n 的情况下进行计算。 ，因为我们可以轻松构建一些段错误。问题是我把我的约束放在一个范围太广的地方。
相反，我可以为结果类型声明一个包装器。

data Pick :: Nat -> * -> * where
  Pick :: {unpick :: (a, List n a)} -> Pick (Succ n) a

Succ n返回索引意味着非空约束是本地的 Pick .辅助函数进行左端扩展，

pCons :: a -> Pick n a -> Pick (Succ n) a
pCons b (Pick (a, as)) = Pick (a, Cons b as)

留给我们

picks' :: List m a -> List m (Pick m a)
picks' Nil          = Nil
picks' (Cons x xs)  = Cons (Pick (x, xs)) (fmap (pCons x) (picks' xs))

如果我们想要

picks = fmap unpick . picks'

这可能有点矫枉过正，但如果我们想将 sibling 和 sibling 分开，将列表分成三份，这可能是值得的，如下所示:

data Pick3 :: Nat -> * -> * where
  Pick3 :: List m a -> a -> List n a -> Pick3 (Succ (m + n)) a

pCons3 :: a -> Pick3 n a -> Pick3 (Succ n) a
pCons3 b (Pick3 bs x as) = Pick3 (Cons b bs) x as

picks3 :: List m a -> List m (Pick3 m a)
picks3 Nil          = Nil
picks3 (Cons x xs)  = Cons (Pick3 Nil x xs) (fmap (pCons3 x) (picks3 xs))

同样，所有的 Action 都是左端的，所以我们很好地适应了 + 的计算行为。 .
积累
如果我们想保持最初尝试的风格，一边走一边积累哥哥姐姐，我们可以做的比保持 zipper 式更糟糕，将最接近的元素存储在最容易接近的地方。也就是说，我们可以以相反的顺序存储大兄弟，这样在每一步我们只需要 Cons ，而不是串联。当我们想要在每个地方构建完整的兄弟列表时，我们需要使用反向串联(实际上，将子列表插入列表 zipper )。您可以输入 revCat如果您部署算盘样式的添加，则很容易用于向量:

type family (+/) (a :: Nat) (b :: Nat) :: Nat
type instance (+/) Zero     n  =  n
type instance (+/) (Succ m) n  =  m +/ Succ n

这是与 revCat 中的值级计算一致的加法。 ，定义如下:

revCat :: List m a -> List n a -> List (m +/ n) a
revCat Nil         ys  =  ys
revCat (Cons x xs) ys  =  revCat xs (Cons x ys)

我们购买了一个带 zipper 的 go版本

picksr :: List (Succ n) a -> List (Succ n) (a, List n a)
picksr = go Nil where
  go :: List p a -> List (Succ q) a -> List (Succ q) (a, List (p +/ q) a)
  go p (Cons x xs@Nil)         =  Cons (x, revCat p xs) Nil
  go p (Cons x xs@(Cons _ _))  =  Cons (x, revCat p xs) (go (Cons x p) xs)

没有人证明任何事情。
结论
Leopold Kronecker 应该说

God made the natural numbers to perplex us: all the rest is the work of man.

一 Succ看起来很像另一个，所以很容易写下表达事物大小的表达式，这与它们的结构不一致。当然，我们可以并且应该(并​​且即将)为 GHC 的约束求解器配备用于类型级数值推理的改进套件。但在此之前，值得密谋调整 Cons es 与 Succ s。