Haskell 单子证明答案

【问题标题】：Haskell monadic proofHaskell 单子证明
【发布时间】：2018-12-06 06:57:06
【问题描述】：

对于数学专家（我不是，也不是 Haskell 专家）：

m >> k = m >>= \_ -> k

这个“monad”类型检查和编译。这是为了在数学上证明m >> k（省略返回值）和m >>= \_ -> k（有返回的单子，但没有返回的lambda）是相同的，还是我可以实际输入值？只是好奇。不是阻塞问题。

【问题讨论】：

在数学上，>> 是根据上面的等式中的>>= 定义的，所以这里没有什么可以证明的。此外，即使等式的两边具有相同的类型，我们也不能得出它们相等的结论。例如。 True = False -- 它们具有相同的类型Bool，但它们不相等。
如果你把实际值放进去，它变成>>=，不再是>>。

【解决方案1】：

这是函数>>的中缀形式的定义。

相当于更常见的(>>) m k = ...。

这里的括号是为了说明Haskell我们使用前缀形式的操作符。

【讨论】：

【解决方案2】：

这不是证据。这更类似于 OOP 接口中方法的定义。

在class Monad的定义中有（Haskell中的类更像是一个接口）；它定义了一个运算符>> 应该被定义。并提供了默认定义。默认定义为m >>= \_ -> k。

【讨论】：