Вопрос по haskell, types – Можно ли программировать и проверять инварианты в Haskell?

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

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

Для того, чтобы отсортировать номера, мне нужно знать, что любые два номера можно заказатьone way or the other, Скажем, что означает, что два числа должны быть настолько упорядоченными.

data OWOTO :: Nat -> Nat -> * where
  LE :: LeN x y => OWOTO x y
  GE :: LeN y x => OWOTO x y

Нам бы хотелось знать, что каждые два числа действительно можно заказать, если у нас есть их представление во время выполнения. В наши дни мы получаем это, строяsingleton family за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

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

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

Да.

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

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

module Sorted (Sorted, sort) where

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

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

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

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

• statically checked array access
• checked data base access
• checked physical dimensions

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

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

Ну, ответ да и нет. Нет способа просто написать инвариант, отдельный от типа, и проверить его. Однако это было реализовано в исследовательской ветке 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/