在Haskell中強制執行monad法律嗎？

從Haskell的維基：在Haskell中強制執行monad法律嗎？

單子可以被看作是一個標準的編程接口的各種數據或控制結構，它是由單子類捕獲。所有常見的單子是它的成員：
class Monad m where 
    (>>=) :: m a -> (a -> m b) -> m b 
    (>>) :: m a -> m b -> m b 
    return :: a -> m a 
    fail :: String -> m a 
除了實現類功能，單子的所有實例應符合下列公式，或單子法律：
return a >>= k = k a 
m >>= return = m 
m >>= (\x -> k x >>= h) = (m >>= k) >>= h 

問題：底部的三條單子法實際上是以這種語言來執行的嗎？還是他們額外的公理你必須強制執行，以便您的「Monad」的語言結構匹配「Monad」的數學概念？

來源

2016-05-09 George

它們不是由語言強制執行或編譯器。程序員負責確保法律的執行。 – ErikR

由於Haskell是* Turing完全*語言，因此您無法對其功能實施任何法律。 –

@WillemVanOnsem這真是讓人誤解。轉向完整的語言仍然可以有一個證明系統，並提供有關操作的保證。例如，Haskell之上的許多擴展（通常是基於SMT）可以證明單子法 - 這些新的擴展語言是否突然變成非圖靈完成的？ –

您負責強制執行一個Monad實例服從單子法。這裏有一個簡單的例子，不是。

即使其類型與Monad方法兼容，計數的時間綁定運營商，已經使用的數量不是一個單子，因爲它違反法律m >>= return = m

{-# Language DeriveFunctor #-} 

import Control.Monad 

data Count a = Count Int a 
    deriving (Functor, Show) 

instance Applicative Count where 
    pure = return 
    (<*>) = ap 

instance Monad Count where 
    return = Count 0 
    (Count c0 a) >>= k = 
     case k a of 
      Count c1 b -> Count (c0 + c1 + 1) b

來源

2016-05-09 20:15:14 Cirdec

不，單子法不是由語言強制執行的。但是如果你不遵守它們，你的代碼在某些情況下可能不一定像你所期望的那樣。它肯定會讓你的代碼用戶感到困惑。

來源

2016-05-09 20:15:06

在Haskell中強制執行monad法律嗎？

回答

相關問題