MonadBaseControl法则

该MonadBaseControl课程提供的法律很少。为了得到我想要的东西，我还需要一个：

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

我极其模糊的直觉表明，这是自然的（从某种意义上来说），甚至可能是由Functor定律，参数化和成文法则的某种组合而产生的MonadBaseControl。是这样吗 如果不是，是否有任何违反法律的“合理”实例？

注意：我还问过这个问题的缩写形式是GitHub issue。

这是的自由定理的直接结果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，展开fmapfor 的定义ReaderT：

(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 Wadler撰写，以及另一个紧密相关的涉及定型构造器类的Free定理，由Janis Voigtlander撰写。