是否有可能程序，检查不变量在Haskell？(Is it possible to program a

当我写一个算法我通常写在意见不变量。

例如，一个功能可能会返回一个有序列表，而另一个期望清单将被订购。
我知道，定理证明存在，但我一直在使用他们没有经验。

我也相信，聪明的编译器[原文如此]可以利用它们来优化程序。
那么，是不是可以写下来的不变量，使编译器检查他们？

Answer 1:

那么，答案是yes和no。有没有办法只写从类型不变单独进行检查。有这个在Haskell的研究叉的实现称为ESC /哈斯克尔，但是： http://lambda-the-ultimate.org/node/1689

你有各种其他的选择。首先，你可以使用断言： http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html

然后用相应的标志，你可以关闭这些断言进行生产。

更一般地，你可以在你的类型编码不变。我要添加更多的在这里，但穿上打我的punchlines。

还有一个例子是这样的非常漂亮的红黑树编码： http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

Answer 2:

下面是一个噱头，但它是一个相当安全的绝技所以不要尝试在家里。它使用了一些有趣的新玩具烤顺序不变成归并。

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

我要的自然数，只是为了让事情变得简单。

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

但我会定义<=式类Prolog的，所以typechecker可以揣摩出顺序含蓄。

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)

测试围绕数字方式都是一样的平常布尔版本颇多，除了与证据。步骤情况下需要拆包和重新包装，因为类型而改变。实例推理有利于参与的逻辑。

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)

我延伸的概念<=相应地，因此，可以typechecker做边界检查。

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 lu是一个序列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)

我们要相信，这个翻译为我们提供了NATTY对应于Nat我们要排序。这种相互关系Nat ， Natty和NATTY是有点沮丧，但是这就是它需要在Haskell刚才。一旦我们得到了，我们可以建立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

我经常看多少程序，是有意义的我们可以让同样多的意义，一个typechecker惊讶。

[下面是一些备用套件我建的，看看发生了什么事。

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))

而没有被隐藏。]

Answer 3:

是。

您编码您不变量在Haskell的类型系统。然后，编译器将强制执行（例如进行类型检查），以防止你的程序编译，如果不变量没有举行。

对于有序列表，你可能会考虑实施的廉价方法智能构造，其在分拣更改的列表类型。

module Sorted (Sorted, sort) where

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

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

现在，您可以编写承担的功能Sorted举行，编译器会阻止你通过无序的东西这些功能。

你可以去很多很多进一步和编码极为丰富的特性入式系统。例子：

静态检查数组访问
检查数据库访问
检查物理尺寸

通过练习，相当复杂的不变量可以用语言来实施，在编译时。

有限制，虽然，作为类型系统没有设计这么多的证明程序的性能。对于重型证明，考虑模型检验或定理证明的语言，如勒柯克。语言阿格达是一个Haskell般的语言，其类型系统的目的是证明丰富的特性。

Answer 4:

这里的其他答案都是美妙的，但即使你的问题特别提到编译器检查，我觉得这个页面是不完整至少帽子的顶端快速检查。快速检查不工作在运行时，而不是在编译时的类型系统，但它是用于测试可能过于困难或不便在类型系统静态特性表达一个伟大的工具。

文章来源: Is it possible to program and check invariants in Haskell?