Доказательства применимого законодательства для экземпляров haskell

Доказано ли, что все экземпляры Haskell класса Applicative, которые мы получаем с платформой Haskell, удовлетворяют всем законам Applicative? Если да, то где мы можем найти эти доказательства?

Исходный код Control.Applicative, похоже, не содержит никаких доказательств того, что применимые законы для различных случаев действительно соблюдаются. Он просто упоминает, что

-- | A functor with application.
--
--Instances should satisfy the following laws:

Затем он просто указывает законы в комментариях.

Я нашел аналогичный случай и для экземпляров других классов типов (Альтернатива и Монада).

Должны ли пользователи этих библиотек сами проверять эти законы?

Но мне было интересно, были ли предоставлены разработчики где-то в другом месте строгие доказательства этих законов?

Опять же, я осознаю, что строгое доказательство законов Applicate (или Monad) для IO Monad, которое включает в себя общение с внешним миром в целом, может быть очень сложным.

Спасибо.


haskell applicative proof
person user1308560    schedule 26.09.2012    source источник

Ответы (3)


arrow_upward
11
arrow_downward

Да, бремя доказывания полностью ложится на писателей библиотеки. Есть несколько примеров реализации, нарушающих эти законы. Каноническим примером нарушения закона является ListT, который не подчиняется законам монад для большинства базовых монад (см. примеры). Это дает очень ошибочное поведение, и в результате никто не использует ListT.

Я почти уверен, что большинство подобных доказательств не высечено на камне в стандартном месте. Большинство доказательств просто повторяли и проверяли до смерти различными любопытными членами сообщества, поэтому через некоторое время мы узнаем, какие реализации удовлетворяют, а какие не удовлетворяют их законам.

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

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

person Gabriel Gonzalez    schedule 26.09.2012
comment
Я полагаю, есть также возможность написать код в такой системе, как Agda или Coq, а затем извлечь из него исходный код Haskell. Честно говоря, я этого не пробовал, но результат будет полностью формальным доказательством требуемых свойств. - person Petr; 26.09.2012
comment
@Gabriel Спасибо. Как и в случае со ListT, сколько других реализаций были замечены в сбоях? Есть ли список неправильных реализаций экземпляров? кроме того, если включение всего доказательства невозможно из-за длины, то можно поместить гиперссылку на доказательство в исходный код и разместить текст доказательства на Haskell.org как часть документации. - person user1308560; 27.09.2012
comment
@ user1308560 ListT - единственная из стандартных библиотек, о которой я знаю совершенно случайно. Идея ссылки имеет смысл. - person Gabriel Gonzalez; 27.09.2012

arrow_upward
1
arrow_downward

Существует отличная библиотека checkers, которая предоставляет свойства QuickCheck для проверки законов.

person s9gf4ult    schedule 01.05.2015

arrow_upward
1
arrow_downward

Экспериментальная библиотека ghc-proofs позволяет вам использовать компилятор для проверки следующих законов:

app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c
                           === a <*> (b <*> c)

Это работает только в нескольких случаях, например, описанный в моем сообщении в блоге , и это лучше всего рассматривать как эксперимент, а не как готовый инструмент.

person Joachim Breitner    schedule 24.04.2017