在Haskell中编写和检查不变量是否可行？

Question

在Haskell中编写和检查不变量是否可行？

haskelltypesinvariantstheorem-proving

30

当我编写算法时，我通常会在注释中写下不变量。

例如，一个函数可能返回一个有序列表，而另一个函数期望列表是有序的。
我知道存在定理证明器，但我没有使用它们的经验。

我还相信聪明的编译器可以利用它们来优化程序。
因此，是否可以编写不变量并让编译器检查它们？

- Andrew

5

关于"扩展静态检查"，已经有一些相关工作，例如http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm。此外，Ralf Hinze和其他人对合同进行了研究。目前的实践似乎是通过类型系统来强制执行不变式，即为有序列表创建一个不透明的新类型，并仅导出正确构建它的构造函数。 - stephen tetley

4个回答

26

是的。

你可以在Haskell类型系统中编码你的不变量。编译器将执行类型检查等操作，以防止程序编译时不满足不变量。

对于有序列表，你可以考虑实现一个智能构造函数，在排序时改变列表的类型。

module Sorted (Sorted, sort) where

newtype Sorted a = Sorted { list :: [a] }

sort :: [a] -> Sorted a
sort = Sorted . List.sort

现在，你可以编写假定{Sorted}被保持的函数，编译器将防止你将未排序的内容传递给这些函数。

你可以进一步将极其丰富的属性编码到类型系统中。例如：

通过实践，语言可以在编译时强制执行相当复杂的不变量。

然而，由于类型系统并非旨在证明程序属性，因此存在限制。对于重型证明，请考虑模型检查或定理证明语言，如Coq。Agda是一种类似于Haskell的语言，其类型系统旨在证明丰富的属性。

- Don Stewart

16

答案是肯定的和否定的。没有办法仅仅写一个与类型无关的不变量并对其进行检查。然而，在名为ESC/Haskell的Haskell研究分支中有一种实现方式: http://lambda-the-ultimate.org/node/1689 你还有其他各种选项。首先，你可以使用asserts: http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html 然后，通过适当的标志，你可以在生产环境中关闭这些asserts。

更一般地说，你可以将不变量编码到你的类型中。我本来想在这里添加更多内容，但dons已经抢先了。

另一个例子是这个非常好的红黑树编码: http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

- sclv

1

我正在寻找GADTs树示例。很好的发现。 - Don Stewart

看起来类型和断言的组合已经足够好了。但我希望能够在编译时检查这些断言是否成立。例如，在 (!!) :: [a] -> b -> a 中，检查 b < length a 是否为真。 - Andrew

Andrew：看一下Don的帖子中的“静态检查数组访问”示例。此外，还可以在Hackage上查看blas和hmatrix-static库，它们使用类型来确保矩阵和向量操作中的大小匹配。 - sclv

@Andrew: 在极限情况下，您需要一个依赖类型系统来验证这样的事情，而这不是编译器可以在您没有额外工作的情况下为您完成的；作为程序员，您必须_证明_您在使用 （！！）的任何地方时，都传递了一个索引，该索引在范围内。 Haskell代表了在静态和自动验证方面可以验证的相当甜蜜的点。 - Tom Crockett

4

这里的其他答案都很棒，但是尽管您的问题特别提到了编译器检查，我觉得如果不至少提一下 QuickCheck，这个页面就会显得不完整。QuickCheck在运行时完成工作，而不是在编译时的类型系统中完成工作，但它是一个非常好的工具，用于测试可能在类型系统中静态表达过于困难或不方便的属性。

- mightybyte

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- pigworker · Accepted Answer

以下是一种技巧，但它非常安全，你可以尝试在家里实践。它使用了一些有趣的新玩具来将顺序不变量嵌入到归并排序中。

{-# LANGUAGE GADTs, PolyKinds, KindSignatures, MultiParamTypeClasses,
    FlexibleInstances, RankNTypes, FlexibleContexts #-}

为了保持简单，我将使用自然数。

data Nat = Z | S Nat deriving (Show, Eq, Ord)

但是我将在Prolog类型类中定义<=，这样类型检查器可以尝试隐式地确定顺序。

class LeN (m :: Nat) (n :: Nat) where
instance             LeN Z n where
instance LeN m n =>  LeN (S m) (S n) where

为了对数字进行排序，我需要知道任何两个数字可以以一种或另一种方式排序。假设这意味着两个数字可以按照某种顺序排列。

data OWOTO :: Nat -> Nat -> * where
  LE :: LeN x y => OWOTO x y
  GE :: LeN y x => OWOTO x y

我们希望知道每两个数字是否可以排序，只要我们有它们的运行时表示。现在，我们通过构建 "singleton family" 来实现这一点，其中 Nat 是该 family 的类型。 Natty n 是 n 的运行时复制的类型。

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

测试数字的顺序与通常的布尔版本非常相似，只是需要证据。在步骤案例中，需要进行拆包和重新打包，因为类型会发生变化。实例推断对所涉及的逻辑很有帮助。

owoto :: forall m n. Natty m -> Natty n -> OWOTO m n
owoto Zy      n       = LE
owoto (Sy m)  Zy      = GE
owoto (Sy m)  (Sy n)  = case owoto m n of
  LE -> LE
  GE -> GE

现在我们知道如何将数字排序，让我们看看如何创建有序列表。计划是描述处于松散边界之间的顺序。当然，我们不想排除任何元素的可排序性，因此限制类型扩展了元素类型，包括底部和顶部元素。

data Bound x = Bot | Val x | Top deriving (Show, Eq, Ord)

我相应地扩展了“<=”的概念，这样类型检查器就可以进行边界检查。

class LeB (a :: Bound Nat)(b :: Bound Nat) where
instance             LeB Bot     b        where
instance LeN x y =>  LeB (Val x) (Val y)  where
instance             LeB (Val x) Top      where
instance             LeB Top     Top      where

这里是数字有序列表：一个OList l u是一个序列x1 :< x2 :< ... :< xn :< ONil，满足l <= x1 <= x2 <= ... <= xn <= u。 x :<检查x是否在下限之上，然后将x作为尾部的下限。

data OList :: Bound Nat -> Bound Nat -> * where
  ONil :: LeB l u => OList l u
  (:<) :: forall l x u. LeB l (Val x) =>
          Natty x -> OList (Val x) u -> OList l u

我们可以像处理普通有序列表一样编写merge函数。关键是如果两个列表共享相同的范围，则它们的合并也将共享该范围。

merge :: OList l u -> OList l u -> OList l u
merge ONil      lu         = lu
merge lu        ONil       = lu
merge (x :< xu) (y :< yu)  = case owoto x y of
  LE  -> x :< merge xu (y :< yu)
  GE  -> y :< merge (x :< xu) yu

案例分析的分支扩展了输入内容已知的部分，提供了足够的排序信息以满足结果的要求。实例推理作为基本定理证明器：幸运的是（或者说，通过一些练习），证明义务是足够简单的。

让我们达成协议。我们需要构建运行时证明来对数字进行排序。

data NATTY :: * where
  Nat :: Natty n -> NATTY

natty :: Nat -> NATTY
natty Z      =                           Nat Zy
natty (S n)  = case natty n of Nat n ->  Nat (Sy n)

我们需要相信这个翻译可以给我们对应于我们想要排序的 Nat 的 NATTY。在Haskell中，Nat、Natty和NATTY之间的相互作用有些令人沮丧，但现在就是这样。一旦我们得到了这个，我们就可以按照通常的分治方式构建 sort。

deal :: [x] -> ([x], [x])
deal []        = ([], [])
deal (x : xs)  = (x : zs, ys) where (ys, zs) = deal xs

sort :: [Nat] -> OList Bot Top
sort []   = ONil
sort [n]  = case natty n of Nat n -> n :< ONil
sort xs   = merge (sort ys) (sort zs) where (ys, zs) = deal xs

我经常感到惊讶的是，对我们有意义的许多程序也可以让类型检查器感到同样有意义。

[这是我建造的一些备用工具，用于观察发生了什么。

instance Show (Natty n) where
  show Zy = "Zy"
  show (Sy n) = "(Sy " ++ show n ++ ")"
instance Show (OList l u) where
  show ONil = "ONil"
  show (x :< xs) = show x ++ " :< " ++ show xs
ni :: Int -> Nat
ni 0 = Z
ni x = S (ni (x - 1))

并且没有任何内容被隐藏。