Haskell: Как доказать (проверить), соответствует ли самоопределенный экземпляр монады законам монады?

Question

Не используя формальный вывод, как я могу проверить, соответствует ли самоопределенный экземпляр Monad законам Монады?

Answer 1

FWIW, вот набор свойств QuickCheck, которые я недавно написал, чтобы проверить законы Монады для реализации Maybe, полученной из ее F-алгебры:

testProperty "Monad left identity law" $ do
  a :: String <- arbitrary
  k :: String -> MaybeFix Integer <- (fromMaybe .) <$> arbitrary

  let left = return a >>= k
  let right = k a

  return $ left == right
,
testProperty "Monad right identity law" $ do
  m :: MaybeFix Integer <- fromMaybe <$> arbitrary

  let left = m >>= return
  let right = m

  return $ left == right
,
testProperty "Monad associativity law" $ do
  m :: MaybeFix String <- fromMaybe <$> arbitrary
  k :: String -> MaybeFix Integer <- (fromMaybe .) <$> arbitrary
  h :: Integer -> MaybeFix Ordering <- (fromMaybe .) <$> arbitrary

  let left = m >>= (\x -> k x >>= h)
  let right = (m >>= k) >>= h

  return $ left == right

Answer 2

Это может быть немного чрезмерно, но вы можете попробовать hs-to-coq , который может быть в состоянии преобразовать ваш код hs в код Coq, который затем вы можете доказать с помощью Coq (помощник по проверке) .

Пример доказательства законов монады с использованием Coq (хотя при этом не использовался hs-to-coq) см. https://github.com/jwiegley/coq-pipes#laws-proven

Answer 3

Полагаю, вы знаете, что такое законы Монады, но я свяжу их для полноты.

Поскольку вы прямо упомянули тестирование, а не формальное доказательство, вы можете использоватьодна из автоматизированных сред тестирования для Haskell, например, QuickCheck или Hspec .