当我编写算法时，我通常会在注释中写下不变量。
例如，一个函数可能返回一个有序列表，而另一个函数期望一个列表是有序的。
我知道定理证明存在，但我没有使用它们的经验。
我也相信智能编译器 [原文如此！] 可以利用它们来优化程序。
那么，是否可以写下不变量并让编译器检查它们？
问问题
3868 次
4 回答
58
以下是一个特技，但它是一个相当安全的特技，所以请在家里尝试一下。它使用一些有趣的新玩具将顺序不变量烘焙到 mergeSort 中。
{-# 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
我们想知道每两个数字确实是可排序的，只要我们有它们的运行时表示。这些天来，我们通过为Nat. Natty n是 的运行时副本的类型n。
data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
除了有证据之外，测试数字的方式很像通常的布尔版本。step case 需要解包和重新打包，因为类型会发生变化。实例推理有利于所涉及的逻辑。
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
这里是有序的数字列表： anOList l u是一个序列x1 :< x2 :< ... :< xn :< ONil，使得l <= x1 <= x2 <= ... <= xn <= u. 高于下限的x :<检查，然后作为下限强加在尾部。xx
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)
我们需要相信这个翻译给了我们与我们想要排序的NATTY内容相对应的内容。和之间的Nat这种相互作用有点令人沮丧，但这就是刚才在 Haskell 中所需要的。一旦我们有了这些，我们就可以按照通常的分而治之的方式进行构建。NatNattyNATTYsort
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))
并且什么都没有隐藏。]
于 2012-05-18T20:42:18.190 回答
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 的语言，其类型系统旨在证明丰富的属性。
于 2012-05-18T16:41:56.727 回答
16
嗯，答案是肯定的和否定的。没有办法只写一个与类型分开的不变量并检查它。在 Haskell 的一个名为 ESC/Haskell 的研究分支中有一个实现，但是： http: //lambda-the-ultimate.org/node/1689
您确实有各种其他选择。一方面，您可以使用断言：http ://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html
然后使用适当的标志，您可以关闭这些断言以进行生产。
更一般地，您可以对类型中的不变量进行编码。我打算在这里添加更多，但不要击败我的妙语。
另一个例子是这种非常好的红黑树编码：http ://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/
于 2012-05-18T16:39:55.540 回答
4
这里的其他答案都很棒，但即使你的问题特别提到了编译器检查，我觉得如果没有至少对QuickCheck的提示，这个页面将是不完整的。QuickCheck 在运行时而不是在编译时在类型系统中完成它的工作，但它是一个很好的工具，用于测试在类型系统中静态表达可能过于困难或不方便的属性。
于 2012-05-24T04:37:07.233 回答