MonadBaseControl定律

Question

班级提供的法律很少。要想得到我想要的东西，我还需要一个：

forall f q. f <$> liftBaseWith q
  = liftBaseWith $ \runInBase -> fmap f (q runInBase)

我极其模糊的直觉表明，这是自然的(在某种意义上)，它甚至可能来自Functor定律、参数性和文档化的MonadBaseControl定律的某些组合。是这样吗？如果没有，是否有任何违反法律的“合理”事例？

注意:我还问了这个问题的简写版本作为一个GitHub问题。

Answer 1

这是liftBaseWith型自由定理的直接结果。

“自由定理”的一个简化版本足以产生这样一个自由定理的版本：

任何函数f :: forall a. F a -> G a，其中F和G是函子，对于任何类型的a、b和任何函数phi :: a -> b，都满足，

fmap phi . f = f . fmap phi  -- simplified "free theorem" for f

(换句话说，这个公式在任何时候都适用。)

我没有现成的证据，但如果有反例，我会感到非常惊讶的。

应用程序

在本例中，f是liftBaseWith，其中函子是

F a = RunInBase m b -> b a  -- F = ReaderT (RunInBase m b) b
G a = m a

将上述“自由定理”的两面应用于q，给出了ReaderT的fmap定义。

(fmap phi . liftBaseWith) q = (liftBaseWith . fmap phi) q
fmap phi (liftBaseWith q) = liftBaseWith (fmap phi q)
fmap phi (liftBaseWith q) = liftBaseWith \run -> fmap phi (q run)

相关文献

作为阅读这个话题的起点，当然还有免费的论文“定理”！作者菲利普·瓦德勒( Philip )，另一位与詹尼斯·沃格兰德( Janis )密切相关的人( https://www.janis-voigtlaender.eu/papers/FreeTheoremsInvolvingTypeConstructorClasses.pdf )。