haskell - MonadBaseControl 法律

Question

MonadBaseControl class提供很少的法律。获取something I want ，我还需要一个:

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

我极其模糊的直觉表明这是自然的(在某种意义上)，它甚至可能来自 Functor 的某种组合。法律、参数化和记录在案的 MonadBaseControl法律。是这样吗？如果没有，是否有任何“合理”的不遵守法律的情况？

注意:我也问过这个问题的缩写版本 as a GitHub issue .

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 ，展开 fmap的定义对于 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 theorems involving type constructor classes由贾尼斯福伦达。