我怎样才能表达'takeWhile for vectors'的类型？

Question

Haskell初学者在这里.我已经定义了以下类型:

data Nat = Z | S Nat
data Vector a n where
    Nil :: Vector a Z
    (:-) :: a -> Vector a n -> Vector a (S n)
infixl 5 :-

我正在尝试编写函数takeWhileVector,其行为与takeWhile在列表上的行为相同,但在Vectors上.

我的实现如下:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
takeWhileVector f Nil = Nil
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil

这不会编译并产生以下错误:

Could not deduce (m ~ 'S n0)
from the context (n ~ 'S n1)
  bound by a pattern with constructor
             :- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n),
           in an equation for ‘takeWhileVector’
  at takeWhileVector.hs:69:20-26
  ‘m’ is a rigid type variable bound by
      the type signature for
        takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
      at takeWhileVector.hs:67:20
Expected type: Vector a m
  Actual type: Vector a ('S n0)
Relevant bindings include
  takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
    (bound at takeWhileVector.hs:69:1)
In the expression: (x :- takeWhileVector f xs)
In an equation for ‘takeWhileVector’:
    takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)

我原以为takeWhileVector的类型定义如下:

对于所有类型'a'和'n'类型的Nat,此函数返回'Vector a m',其中'm'是类型Nat.

我是否需要更改takeWhileVector的类型签名以使其更具体,以便显示结果为Vector a(m :: Nat)？否则,如何更改它以使其编译？

Answer 1

你建议的类型无法实现,即它没有人居住:

takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m

请记住,调用者选择类型变量a,n,m.这意味着调用者可以使用您的函数,例如

takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z)

这是胡说八道,因为a如果你一开始没有,你就不能产生一些.更实际的是,这个函数的调用者并不意味着能够选择有多少结果并传递一个完全不相关的函数 - 这将不同于预期的语义takeWhile.

我猜你真正的意思是什么

takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m

除了那exists是无效的Haskell语法.相反,你需要类似的东西

data SomeVector a where
   S :: Vector a m -> SomeVector a

takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a

Answer 2

没有办法静态地知道Vec返回的长度takeWhileVec:它取决于Vec您使用的函数和函数中包含的值.但是,我能做的就是给你一个你可以模式匹配的值来学习它的长度Vec.输入单例值.

data Natty n where
    Zy :: Natty Z  -- pronounced 'zeddy', because I'm a limey
    Sy :: Natty n -> Natty (S n)  -- pronounced 'essy'

对于给定n的类型Nat,只有一个(非undefined)类型的值Natty n.因此,如果你对a有所了解Natty,你也会对它的相关类型级别有所了解Nat.*

为什么我们不能只Nat为此目的使用？Haskell维持值和类型之间的分离.Nat除了结构相似性之外,类型级别Nat与值级别没有任何关系:值S Z具有类型Nat,而不是S' Z'- 因此我们必须使用Natty第二个副本Nat来手动将值和类型绑定在一起.(像Agda这样的真正依赖类型的系统允许您Nat在值级和类型级计算中重复使用它们.)

_{*您也可以使用类型类以其他方式传播知识.}

计划是将输出向量及其长度作为a返回Natty,其中类型的排列方式使GHC理解Natty确实代表其长度.您可以先在问题中考虑此示例的变体:

-- takeWhile :: (a -> Bool) -> Vec a n -> (Natty m, Vec a m)

但这并不是说正确的事情:我们说takeWhile可以回复任何m来电者的选择,这不是真的!它只能返回m由函数和输入向量确定的唯一值.正如我所提到的,这在编译时是不可知的,所以我们必须保持编码器的长度.

data AVec a = forall n. AVec (Natty n) (Vec a n)

AVec是一种存在主义类型:n出现在右侧而不是左侧.此技术允许您模拟依赖对类型:类型Vec取决于的值Natty.只要数据的静态属性依赖于编译时不可用的动态信息,从属对就很有用.

我们takeWhile现在可以直截了当地写:

takeWhile :: (a -> Bool) -> Vec a n -> AVec a
takeWhile f Nil = AVec Zy Nil
takeWhile f (x :- xs) = case takeWhile f xs of
                             AVec n ys -> if f x
                                          then AVec (Sy n) (x :- ys)
                                          else AVec Zy Nil

我们不得不抛弃Vector长度的静态知识,那么如何使用AVec带有静态要求的函数呢？由于AVec构造方式,我们知道Natty左侧插槽中的向量表示右侧插槽中向量的长度:它们都具有相同(存在隐藏)类型参数n.所以,通过模式匹配Natty,我们可以了解它的长度Vec.

head :: Vec a (S n) -> a
head (x :- xs) = x

head' :: AVec a -> Maybe a
head' (AVec Zy Nil) = Nothing
head' (AVec (Sy n) xs) = Just (head xs)

在这个例子中,我们只关心向量是否长于1,因此模式匹配Sy足以向GHC证明我们应该被允许使用head.(参见我的相关答案,了解更多涉及证明AVecs 事实的例子.)

@chi提到了一个诱人的想法:您可能希望显示返回的向量takeWhile不长于输入向量.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n

AShorterVec向量的类型在哪里不超过n.我们的挑战是写下定义AShorterVec.

给出两个自然数,你如何确定第一个与第二个相差不是或等于？这种关系是归纳的.如果左操作数为零,则它自动小于或等于任何自然数.否则,如果一个数字的前身小于或等于另一个的前任,则该数字小于或等于另一个数字.我们可以使用GADT将其编码为建设性证据.

data LTE n m where
    ZLte :: LTE Z m
    SLte :: LTE n m -> LTE (S n) (S m)

如果n小于m,你将能够得到一个值LTE n m.如果不是,你就做不到.这就是库里 - 霍华德同构的全部意义所在.

现在我们已经准备好定义AShorterVec:为了构建一个值,AShorterVec a n你需要能够证明它比n提供一个值更短LTE m n.在AShorterVec构造函数上进行模式匹配时,它会为您提供校对,以便您可以使用它进行计算.

data AShorterVec a n = forall m. AShorterVec (LTE m n) (Vec a m)

takeWhile 编译只有一个小的改变:我们必须操纵这个证明对象.

takeWhile :: (a -> Bool) -> Vec a n -> AShorterVec a n
takeWhile f Nil = AShorterVec ZLte Nil
takeWhile f (x :- xs) = case takeWhile f xs of
                             AShorterVec prf ys -> if f x
                                                   then AShorterVec (SLte prf) (x :- ys)
                                                   else AShorterVec ZLte Nil

给出类型的另一种方法takeWhile是将长度的上限推入返回类型本身,而不是将其作为数据携带.这种方法不需要任何争论Natty,证明术语LTE和存在量化.

data ShorterVec a n where
    SNil :: ShorterVec a n
    SCons :: a -> ShorterVec a n -> ShorterVec a (S n)

再一次,ShorterVec a n表示不超过的向量集n.结构ShorterVec让人联想到有限集,但是从自然世界转化为向量世界.空矢量比您想要命名的任何长度都短; cons单元将最小有效上限增加1.请注意,值的值n永远不会完全由type的值确定ShorterVec,因此您可以为a赋予任何有效的上限ShorterVec.这两个表达式都是很好的类型:

ok1 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S (S Z)))
ok2 = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S (S Z))

但这个不是:

-- notOk = SCons 1 (SCons 3 SNil) :: ShorterVec Int (S Z)  -- the vector is longer than our stated upper bound.

使用此数据类型,您可以编写一个非常简单的版本,takeWhile其外观与原始列表版本完全相同:

takeWhile :: (a -> Bool) -> Vec a n -> ShorterVec a n
takeWhile f Nil = SNil
takeWhile f (x :- xs) = if f x
                        then SCons x (takeWhile f xs)
                        else SNil

放宽我们对类型的假设使得函数更容易实现,但是您需要支付另外一种需要转换的类型的成本.您可以ShorterVec通过测量长度从后面转换为使用从属对的版本.

toAVec :: ShorterVec a n -> AVec a
toAVec SNil = AVec Zy Nil
toAVec (SCons x xs) = case toAVec xs of
                           AVec n ys -> AVec (Sy n) (x :- ys)

我们开始使用单例将类型和值绑定在一起,并使用存在类型将数据本身的运行时信息包含在内.然后,遵循@ chi的想法,我们使用证明项将(正文的一部分)编码takeWhile到类型签名中.然后我们想出了一种方法来直接将长度不变量烘焙到返回类型中,从而无需证明任何定理.

一旦你在舌头上获得了依赖类型编程的味道,就很难回到旧的方式.富有表现力的类型系统至少为您提供三个优势:您可以编写其他语言不允许的有效程序(或强制您复制代码); 你可以为相同的函数编写更有意义的类型,做出更有力的承诺; 并且您可以以机器可检查的方式证明程序的正确性.

不过Haskell并没有为它做好准备.一个问题是单例使得绑定类型和值不必要地复杂化:Nat- Natty区别导致样板代码爆炸,其中大部分是我免除的,在类型和值之间进行混洗.(许多这样的样板可以自动化-这就是在singletons图书馆给你).如果我们想要指定的正确性的另一个方面takeWhile-事实上,所有的输出列表的元素满足谓词-我们不得不用专门工作单例列表和类型级谓词函数.每次我想要量化存在的东西时,我也发现声明一个新的顶级类型是很繁琐的(你可以编写库来帮助解决这个问题,尽管它们经常导致其他的样板) - 我们缺少类型级lambda到谢天谢地 另一个主要难点是可以提升到类型级别的限制使用DataKinds:GADT和存在类型无法提升,因此例如你不能有一个多维数组,其形状静态表示为a Vec Nat n.没有真正依赖类型的系统使得依赖类型难以使用!