Ответ 1
Вы можете переносить "доказательство", которое имеет ваш инвариант, создавая newtype
.
newtype Sorted a = Sorted { fromSorted :: [a] }
sorted :: Ord a => [a] -> Sorted a
sorted = Sorted . sort
foo :: Sorted Integer -> Bool
foo (Sorted as) -> some_recursive_stuff_here
Если вы спрячете конструктор Sorted
в отдельном модуле, тогда пользователи вашего кода не смогут использовать foo
, не создавая сначала подтверждение сортировки. Они также не смогут sort
a Sorted
, поэтому вы можете быть уверены, что это произошло только один раз.
Вы можете даже поддерживать операции подтверждения, если хотите.
instance Monoid (Sorted a) where
mempty = Sorted mempty
mappend (Sorted as) (Sorted bs) = Sorted (go as bs) where
-- lazy stable sort
go :: Ord a => [a] -> [a] -> [a]
go [] xs = xs
go xs [] = xs
go (x:xs) (y:ys) | x == y = x : y : go xs ys
| x < y = x : go xs (y:ys)
| x > y = y : go (x:xs) ys
(Этот код теперь доступен для Hackage: http://hackage.haskell.org/package/sorted)