11

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

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 传达例如+可交换和关联或零是身份，所以我遇到了很多问题，其中类型检查器 (可以理解）抱怨它无法确定 thata + b ~ b + a或 that a + Zero ~ a。

我是否需要添加某种证明对象（data Refl a b where Refl :: Refl a a等），或者有什么方法可以通过添加更明确的类型签名来完成这项工作？

4

1 回答 1

18

结盟

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

我是否需要添加某种证明对象（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，因为我们可以很容易地构造一些段错误的东西。问题只是我把约束放在了一个范围太广的地方。

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

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

返回索引意味着非Succ n空约束是局部的 a 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)

我们获得了一个拉链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 对齐。

于 2013-07-06T13:59:00.577 回答