结盟
依赖类型编程就像做两个拼图,一些流氓粘在一起。不那么隐喻,我们在值级别和类型级别表示同时计算,我们必须确保它们的兼容性。当然,我们每个人都是自己的流氓,所以如果我们能把拼图粘成一条直线,我们就会过得更轻松。当您看到类型修复的证明义务时,您可能会想问
我是否需要添加某种证明对象(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 的约束求解器配备用于类型级数值推理的改进套件。但在此之前,值得将Cons
es 与Succ
s 对齐。