Haskell平臺獲得的Applicative類型類的所有Haskell實例都被證明滿足所有適用法律？ 如果是，我們在哪裏找到這些證明？用於haskell實例的應用法律證明
Control.Applicative的源代碼似乎沒有包含任何證據證明各種實例的適用法律確實成立。 它只是提到
-- | A functor with application.
--
--Instances should satisfy the following laws:
它然後就指出在意見的法律。
我發現了一個類似的情況下，其他類型實例（Alternative和Monad）。
這些庫的用戶是否應該自行驗證這些規則？
但是我想知道這些法律的嚴格證據是否已經由開發者在別處給出了？
同樣，我知道IO Monad的Applicate（或Monad）法律的一個嚴格證明，涉及到與外界的交談，一般而言，可能非常複雜。
謝謝。
是的，舉證責任完全在圖書館作家身上。有一些實施違反這些法律的例子。違反法律的典型例子是ListT，它不遵守大多數基本monad的單子法（參見examples）。這給出了非常錯誤的行爲，因此沒有人真的使用ListT。
我敢肯定，大多數這些類型的證明沒有在標準的地方刻在石頭上。大多數證據只是被各種好奇的社區成員重複和檢查而死，所以過了一段時間，我們知道哪些實施是否滿足其法律。
舉一個具體的例子，當我寫我pipes庫，我要證明我的pipes滿足Category法律，但我只是保持在一個文本文件，這些證明或hpaste爲將來的記錄，如果有人要求他們。將它們包括在源代碼中並不可行，因爲它們可能會變得很長，特別是對於關聯性法則。
但是，我認爲一個好的做法可能是在可能的情況下在原始存儲庫中包含機器檢查證明，以便用戶可以根據需要引用它們。
有優秀的圖書館checkers它提供QuickCheck屬性來檢查法律。
實驗庫ghc-proofs允許您使用編譯器來驗證這些法律對您：
app_law_2 a b (c :: Succs a) = pure (.) <*> a <*> b <*> c
=== a <*> (b <*> c)
它只能在少數情況下，如一個描述in my blog post，並且最好被看成是一個實驗，而不是一個現成的工具。
我想也有可能在Agda或Coq這樣的系統中編寫代碼，然後從中提取Haskell源代碼。說實話，我還沒有嘗試過，但結果將是對所需屬性的完全正式證明。 –
@加布裏埃爾謝謝。像ListT一樣，有多少其他實現已經注意到會出錯？是否有哪個實例實現哪個是錯誤的列表？另外，如果包含整個證明由於長度而不可行，那麼可以在源代碼中加入證明超鏈接，並將證明文本放在Haskell.org上作爲文檔的一部分。 – user1308560
@ user1308560 ListT是我知道的標準庫中唯一一個不在我頭頂的人。鏈接的想法是有道理的。 –