隐含提升的正确性

Question

想象一下,我有一个比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是monad,并且T是monad变换器:

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

......这些实例遵守monad法律和monad变压器法则.

我们可以推断出:

m1 = m2

...... m除了它的类型之外什么都不知道？

这只是一个冗长的方式,询问是否lift m是一个有效的替代m,假设两种类型检查.这个问题有点难以理解,因为它需要m在替换之前和之后将类型检查作为两个单独的monad.据我所知,这种替换进行类型检查的唯一方法m是在monad上是否通用.

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

Answer 1

如果m :: Monad m => m A,那么m必须等同return x于某些人x :: A,因为你必须获得任何东西的唯一方法:: m x是return和(>>=).但是为了使用(>>=)你必须能够生产一些m y,你可以做return或与另一个应用程序(>>=).无论哪种方式,你必须return最终使用,monad法律保证整个表达式将等同于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会有所不同.

(当然所有这一切都忽略了⊥.然后,如果你不这样做,大多数单子都不遵守法律.)