是否可以在Haskell中编程和检查不变量？

Question

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

例如,一个函数可能返回一个有序列表,另一个函数则期望列出一个列表.
我知道定理证明存在,但我没有使用它们的经验.

我也相信智能编译器[sic!]可以利用它们来优化程序.
那么,是否有可能写下不变量并让编译器检查它们？

Answer 1

以下是特技,但这是一个非常安全的特技,所以在家尝试.它使用一些有趣的新玩具将订单不变量烘焙到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)

除了有证据之外,测试数字的方式与通常的布尔版本非常相似.步骤案例需要拆包和重新打包,因为类型会发生变化.实例推理有利于所涉及的逻辑.

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

现在我们知道如何按顺序放置数字,让我们看看如何制作有序列表.计划是描述松散边界之间的顺序.当然,我们不希望排除任何元素是可排序的,因此边界类型使用bottom和top元素扩展元素类型.

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

我们需要相信这个翻译为我们提供了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

我经常会惊讶于有多少对我们有意义的程序对于一个类型检查员来说同样有意义.

[这是我建立的一些备用工具包,看看发生了什么.

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 2

是.

您可以在Haskell类型系统中对不变量进行编码.然后编译器将强制执行(例如执行类型检查),以防止在不保持不变量的情况下编译程序.

对于有序列表,您可能会考虑实现智能构造函数的廉价方法,该构造函数在排序时更改列表的类型.

module Sorted (Sorted, sort) where

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

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

现在您可以编写假设Sorted保留的函数,编译器将阻止您将未排序的东西传递给这些函数.

您可以更进一步,将非常丰富的属性编码到类型系统中.例子:

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

通过练习,可以在编译时通过语言强制执行非常复杂的不变量.

但是有一些限制,因为类型系统的设计并不是为了证明程序的属性.对于重型样张,请考虑模型检查或定理证明语言,如Coq.Agda语言是一种类似Haskell的语言,其类型系统旨在证明丰富的属性.

Answer 3

嗯,答案是肯定的,不是.没有办法只从类型中写出一个不变的单独格式并检查它.在Haskell的一个名为ESC/Haskell的研究分支中有一个实现,但是:http://lambda-the-ultimate.org/node/1689

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

然后使用适当的标志,您可以关闭这些断言以进行生产.

更一般地,您可以对类型中的不变量进行编码.我打算在这里添加更多,但是dons打败了我.

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