为长度索引列表实现拉链

Question

我正在尝试为长度索引列表实现一种拉链,它将返回列表中的每个项目以及删除该元素的列表.例如普通列表:

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

对准

依赖类型编程就像做两个拼图,一些流氓粘在一起.不那么隐喻,我们在价值级别和类型级别表达同时计算,我们必须确保它们的兼容性.当然,我们每个人都是我们自己的流氓,所以如果我们可以安排将拼图粘在一起,我们就会有更轻松的时间.当您看到类型修复的证明义务时,您可能会想要问

我是否需要添加某种证明对象(data Refl a b where Refl :: Refl a a等等)或者是否有某种方法可以通过添加更多显式类型签名来实现此功能？

但是您可能首先考虑价值和类型级别计算以何种方式不一致,以及是否有任何希望使它们更接近.

一个办法

这里的问题是如何计算向量中的选择向量(长度索引列表).所以我们想要类型的东西

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

其中每个输入位置的元素用其兄弟姐妹的一个较短的向量进行装饰.所提出的方法是从左向右扫描,将年长的兄弟姐妹聚集在右侧生长的列表中,然后在每个位置与较年轻的兄弟姐妹连接.右侧的增长列表总是令人担心,尤其是当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,因为我们可以很容易地构建一些segfaulting的东西.问题在于我将约束放在一个范围太广的地方.

相反,我可以为结果类型声明一个包装器.

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'

这可能是矫枉过正的,但如果我们想要将年龄较小的兄弟姐妹分开,将三个名单分成三部分,这可能是值得的,如下所示:

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))

同样,所有动作都是左端的,所以我们很好地适应了计算行为+.

累积

如果我们想要保持原始尝试的风格,在我们去的时候积累年长的兄弟姐妹,我们可能做得更糟,而不是保持拉链式,将最接近的元素存放在最容易接近的地方.也就是说,我们可以以相反的顺序存储年长的兄弟姐妹,这样我们只需要每一步Cons,而不是连接.当我们想在每个地方构建完整的兄弟列表时,我们需要使用反向连接(实际上,将子列表插入到列表拉链中).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)

我们获得了一个zipperized 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应该说

上帝使自然数字困扰我们:其余的都是人的工作.

一个Succ看起来非常像另一个,因此很容易写下表达式,这些表达式以与其结构不一致的方式给出事物的大小.当然,我们可以而且应该(并​​且即将)为GHC的约束求解器配备改进的类型级数值推理套件.但在开始之前,值得密谋将Conses与Succs 对齐.