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

Question

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

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

我也相信智能编译器 [原文如此!] 可以利用它们来优化程序。
那么，是否可以写下不变量并让编译器检查它们？

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)

除了有证据之外，测试数字的方式很像通常的 bool 版本。 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

现在我们知道如何排列数字，让我们看看如何制作有序列表。该计划是描述松散界限之间的秩序。当然，我们不想排除任何可排序的元素，因此 bounds 的类型将元素类型扩展为底部和顶部元素。

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)

我们需要相信这个翻译给了我们 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))

并且什么都没有隐藏。]