Когда я пишу алгоритм, я обычно записываю инварианты в комментариях.
Например, одна функция может возвращать упорядоченный список, а другая ожидает, что список будет заказан.
Я знаю, что существуют теоретические прокси, но у меня нет опыта их использования.
Я также считаю, что интеллектуальный компилятор [sic!] может использовать их для оптимизации программы.
Итак, можно ли записать инварианты и заставить компилятор проверить их?
Ответ 2
Следующим является трюк, но это довольно безопасный трюк, поэтому попробуйте его дома. Он использует некоторые из развлекательных новых игрушек для извлечения инвариантов порядка в mergeSort.
{-# 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
И вот упорядоченные списки чисел: a 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
Я часто удивляюсь тому, сколько программ, которые имеют для нас смысл, могут иметь такой же смысл для 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))
И ничего не было скрыто.]
Ответ 3
Да.
Вы кодируете свои инварианты в системе типа Haskell. Затем компилятор будет принудительно выполнять (например, выполнять проверку типов), чтобы предотвратить компиляцию вашей программы, если инварианты не удерживаются.
Для упорядоченных списков вы можете рассмотреть дешевый подход к реализации интеллектуального конструктора, который изменяет тип списка при сортировке.
module Sorted (Sorted, sort) where
newtype Sorted a = Sorted { list :: [a] }
sort :: [a] -> Sorted a
sort = Sorted . List.sort
Теперь вы можете записывать функции, предполагающие, что Sorted хранится, и компилятор помешает вам передавать несохраненные вещи этим функциям.
Вы можете пойти гораздо дальше и кодировать чрезвычайно богатые свойства в систему типов. Примеры:
С практикой в процессе компиляции язык может быть применен довольно сложными инвариантами.
Существуют ограничения, поскольку система типов не рассчитана на доказательство свойств программ. Для сверхпрочных доказательств рассмотрим проверку модели или теоретические доказательства, такие как Coq. Язык Agda - это язык, похожий на Haskell, тип которого предназначен для доказательства богатых свойств.
