9

想象一下，我有一个在 monad 上通用的值：

m :: (Monad m) => m A  -- 'A' is some concrete type

现在假设我以两种不同的方式将此值专门用于具体的 monad 转换器堆栈：

m1 :: T M A
m1 = m

m2 :: T M A
m2 = lift m

...其中M和T M是单子，并且T是单子转换器：

instance Monad M where ...
instance (Monad m) => Monad (T m) where ...
instance MonadTrans T where ...

...并且这些实例遵守单子定律和单子变换器定律。

我们可以推断出：

m1 = m2

m...除了它的类型之外一无所知？

这只是一个冗长的询问是否lift m是 的有效替换的方式m，假设两者都进行了类型检查。表述这个问题有点困难，因为它需要m在替换之前和之后将类型检查作为两个单独的 monad。据我所知，这种替换类型检查的唯一方法是 ifm对 monad 是通用的。

我模糊的直觉是替换应该总是正确的，但我不确定我的直觉是否正确，或者如果它是正确的，如何证明它。

4

2 回答 2

9

If m :: Monad m => m A, thenm必须等价于return xfor some x :: A，因为获得任何东西的唯一方法:: m x是returnand (>>=)。但是为了使用(>>=)，您必须能够生成一些m y，您可以return使用(>>=). 无论哪种方式，您最终都必须使用return，并且单子定律保证整个表达式将等效于return x.

（如果m在 monad 上完全多态，那么您必须能够在 处使用它m ~ Identity，因此它不能使用任何花哨的 monad 技巧，除非您将参数传递给它。这种技巧在此处和此处使用。）

鉴于此m = return x，我们通过 monad 转换器法则 ( lift . return = return) 知道lift m = m。

当然，这只适用于这种特定类型。如果你有，比如说，m :: MonadState S m => m A那么m很容易不同于lift m——例如，有一个类似的类型StateT A (State A) A，get并且lift get会不同。

（当然，所有这些都忽略了⊥。再说一次，如果你不这样做，大多数 monad 无论如何都不遵守法律。）

于 2013-02-18T03:33:39.970 回答
2

我相信这是一个草率的归纳证明，你m的等价于lift m.

我认为我们必须尝试证明m（或者更确切地说，关于 type 的所有可能值(Monad m) => m A）。如果我们认为Monad只包含绑定和返回，而忽略底部，fail那么您m必须在顶层是以下之一：

mA = return (x)
mB = (mX >>= f)

因为通过单子变换定律，mA的两种形式是等价的：m

lift (return (x)) = return (x)

这是基本情况。然后我们剩下第二个变压器定律来推理mB：

lift (mX >>= f) = lift mX >>= (lift . f)

并且我们想证明 ourmB等于那个扩展：

mX >>= f = lift mX >>= (lift . f)

我们假设 bind 的左边是等价的（mX = lift mX），因为这是我们的归纳假设（对吗？）。

因此，我们需要f = lift . f通过弄清楚f必须是什么样子来证明：

f :: a -> m b
f = \a -> (one of our forms mA or mB)

看起来lift . f像：

f = \a -> lift (one of our forms mA or mB)

这让我们回到了我们的假设：

m = lift m
于 2013-02-18T03:35:17.750 回答