Можно ли программировать и проверять инварианты в Haskell?

Все остальные ответы здесь просто невероятны, но даже несмотря на то, что в вашем вопросе конкретно упоминается проверка компилятора, я чувствую, что эта страница была бы неполной без хотя бы подсказки QuickCheck . QuickCheck выполняет свою работу во время выполнения, а не в системе типов во время компиляции, но это отличный инструмент для тестирования свойств, которые могут быть слишком сложными или неудобными для статического выражения в системе типов.

Да.

Вы кодируете свои инварианты в системе типов Haskell. Затем компилятор принудительно выполнит (например, выполнит проверку типа), чтобы предотвратить компиляцию вашей программы, если инварианты не удерживаются.

Для упорядоченных списков вы могли бы рассмотреть дешевый подход к реализации умного конструктора , который изменяет тип списка при сортировке.

module Sorted (Sorted, sort) where

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

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

Теперь вы можете написать функции, которые предполагают, что Sorted удерживается, и компилятор предотвратит передачу несортированных вещей этим функциям.

Вы можете пойти намного дальше и закодировать чрезвычайно богатые свойства в систему типов. Примеры:

• статически проверенный доступ к массиву
• проверенный доступ к базе данных
• проверенные физические размеры

С практикой, довольно сложные инварианты могут быть применены языком во время компиляции.

Однако существуют ограничения, так как система типов не предназначена для проверки свойств программ. Для тяжелых доказательств рассмотрите проверку моделей или теоремы, доказывающие языки, такие как Coq. Язык Agda - это язык, похожий на Haskell, система типов которого предназначена для доказательства богатых свойств.

1136 Следующее - это трюк, но это довольно безопасный трюк, поэтому попробуйте его дома. Он использует некоторые из новых интересных игрушек, чтобы испечь инварианты порядка порядка в 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

Теперь мы знаем, как упорядочить числа, давайте посмотрим, как составлять упорядоченные списки. План состоит в том, чтобы описать, что это должно быть в порядке между свободными границами . Конечно, мы не хотим исключать какие-либо элементы из сортируемых, поэтому тип 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

Ветви анализа случая расширяют то, что уже известно из входных данных, с помощью информации о заказе, достаточной для удовлетворения требований к результатам. Вывод экземпляра действует как основной доказатель теоремы: к счастью (или, скорее, с небольшой практикой) обязательства по доказательству достаточно легки.

1147 Давайте заключим сделку. Нам нужно построить свидетелей времени выполнения для чисел, чтобы отсортировать их таким образом.

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

И ничего не было спрятано.]