19

我正在尝试构建一个类型的函数：

liftSumthing :: ((a -> m b) -> m b) -> (a -> t m b) -> t m b

t单子变压器在哪里。具体来说，我有兴趣这样做：

liftSumthingIO :: MonadIO m => ((a -> IO b) -> IO b) -> (a -> m b) -> m b

我摆弄了一些 Haskell 魔法库，但无济于事。我怎样才能做到正确，或者在我没有找到的地方有现成的解决方案？

4

1 回答 1

25

由于类型处于负数位置，因此一般无法在所有MonadIO实例上完成此操作。IO有一些关于 hackage 的库可以针对特定实例（monad-control，monad-peel）执行此操作，但是对于它们在语义上是否合理存在一些争论，尤其是关于它们如何处理异常和类似的怪异IO事物。

编辑：有些人似乎对正/负位置的区别感兴趣。实际上，没什么好说的（你可能已经听说过，只是用了不同的名字）。该术语来自子类型的世界。

子类型化背后的直觉是“当 an可以在任何预期使用 a 的地方使用时，它是（我将写的）a的子类型”。在很多情况下，确定子类型很简单。例如，对于产品，无论何时和，这是一个非常简单的规则。但是有一些棘手的情况；例如，我们应该什么时候决定？ba <= bab(a1, a2) <= (b1, b2)a1 <= b1a2 <= b2a1 -> a2 <= b1 -> b2

好吧，我们有一个函数f :: a1 -> a2和一个期望 type 函数的上下文b1 -> b2。所以上下文将使用f' 的返回值，就好像它是 a 一样b2，因此我们必须要求它a2 <= b2。棘手的事情是上下文将提供f一个b1，即使f它会像使用它一样使用它a1。因此，我们必须要求b1 <= a1- 从您可能猜到的情况向后看！我们说a2andb2是“协变的”，或者出现在“正位”， a1andb1是“逆变”，或者出现在“负位”。

（顺便说一句：为什么是“正”和“负”？它的动机是乘法。考虑这两种类型：

f1 :: ((a1 -> b1) -> c1) -> (d1 -> e1)
f2 :: ((a2 -> b2) -> c2) -> (d2 -> e2)

什么时候f1' 类型应该是 ' 类型的子f2类型？我陈述了这些事实（练习：使用上述规则检查）：

  • 我们应该有e1 <= e2。
  • 我们应该有d2 <= d1。
  • 我们应该有c2 <= c1。
  • 我们应该有b1 <= b2。
  • 我们应该有a2 <= a1。

e1在 中处于正位d1 -> e1，而在 的类型中又处于正位f1；此外，在整体e1类型中处于积极位置f1（因为它是协变的，根据上述事实）。它在整个术语中的位置是它在每个子术语中的位置的乘积：正 * 正 = 正。同样，d1在 中处于负数位置d1 -> e1，在整个类型中处于正数位置。负*正=负，d变量确实是逆变的。b1在类型中处于正位置，在类型a1 -> b1中处于(a1 -> b1) -> c1负位置，在整个类型中处于负位置。正 * 负 * 负 = 正，它是协变的。你明白了。）

现在，让我们看一下这个MonadIO类：

class Monad m => MonadIO m where
    liftIO :: IO a -> m a

我们可以将其视为子类型的显式声明：我们正在提供一种方法，使其成为某些具体IO a的子类型。我们马上就知道我们可以在构造函数处于正数位置时获取任何值并将它们转换为s。但仅此而已：我们无法将负构造函数转换为s——我们需要一个更有趣的类。m amIOmIOm

于 2012-02-11T20:53:59.427 回答