证明一个新的单子实例的单子定律（可能的列表）答案

【问题标题】：proving monad laws of a new monad instance (list of maybe)证明一个新的单子实例的单子定律（可能的列表）
【发布时间】：2020-11-23 13:19:20
【问题描述】：

我创建了一个新的 Maybe Monad 实例列表并试图证明实现确实满足 Monad 定律，我做得对还是实现不正确？任何指针表示赞赏。谢谢！

newtype Test a = Test { getTest :: [Maybe a] }
  deriving Functor

instance Applicative Test where
  pure = return
  (<*>) = liftM2 ($)

instance Monad Test where
  return :: a -> Test a
  return a = Test $ [Just a]
  
  (>>=) :: Test a -> (a -> Test b) -> Test b
  Test [Nothing] >>= f = Test [Nothing]
  Test [Just x] >>= f = f x

{-
1. return x >>= f = f x
     return x >>= f = [Just x] >>= f = f x   
 
2. m >>= return = m
     [Nothing] >>= return = [Nothing]
     [Just x] >>= return = return x = [Just x] 

3. (m >>= f) >>= g    ==    m >>= (\x -> (f x >>= g))

   m = [Nothing]
   L.H.S. = ([Nothing] >>= f ) >>= g = Nothing >>= g = Nothing
   R.H.S. = [Nothing] >>= (\x -> (f x >>= g)) = Nothing
   m = [Just x]
   L.H.S. = ([Just x] >>= f) >>= g = f x >>= g
   R.H.S. = [Just x] >>= (\v -> (f v >>= g)) = (\v -> (f v >>= g)) x
          = f x >>= g
-}

【问题讨论】：

看起来你还没有完成定义。 Test [] >>= f 或 Test [Just x, Just y] >>= f 是什么？
启用警告，它们会报告您的模式匹配不完整。我没有检查你的证明，因为你之前需要修复你的>>=。
我阅读了 List Monad 的 Monad law proofs 并注意到它使用了 concat 和 map 等函数，但似乎我不能在这里使用它们。在这种情况下，这是否会使实施变得更加困难？
如果您直接定义pure，return 的默认定义为return = pure，因为Applicative 现在是Monad 的超类。（相同的工作量，但符合现代 Functor-Applicative-Monad 层次结构，而不是在编写 Applicative 实例时已经存在类型的 Monad 实例的旧假设。）
你会发现用单子 composition ((>=>) :: (a -> m b) -> (b -> m c) -> a -> m c / (<=<) = flip (>=>)) 而不是应用程序 (>>= / =<<) 来证明单子定律更容易)，从那时起，它们的措辞更加对称： 1. 左身份 return >=> x = x; 2. 正确的身份 x >=> return = x;和 3. 关联性 (x >=> y) >=> z = x >=> (y >=> z)。这也更清楚地显示了它们与Monoid、Alternative 和Category 法律的关系。

标签： haskell monads

【解决方案1】：

你所写的证明部分只是在不重要的方面是不正确的。具体来说，在这两行中：

([Nothing] >>= f ) >>= g = Nothing >>= g = Nothing
[Nothing] >>= (\x -> (f x >>= g)) = Nothing

三个裸露的Nothings 应该是[Nothing]s。

但是，证明不完整，因为Test a 类型的值既不是[Just (x :: a)] 也不是[Nothing]。这使得整个证明在一个重要方面是不正确的。

【讨论】：