在 Haskell 中提升高阶函数 [英] Lifting a higher order function in Haskell

问题描述

我正在尝试构造一个类型的函数:

I'm trying to construct a function of type:

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

其中 t 是一个 monad 转换器.具体来说，我有兴趣这样做:

where t is a monad transformer. Specifically, I'm interested in doing this:

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

我摆弄了一些 Haskell 巫术库，但无济于事.我如何得到它是的，或者我没有找到某个现成的解决方案?

I fiddled with some Haskell wizardry libs and but to no avail. How do I get it right, or maybe there is a ready solution somewhere which I did not find?

推荐答案

这不能在所有 MonadIO 实例上通用，因为 IO 类型为否定位置.hackage 上有一些库可以针对特定实例执行此操作(monad-control、monad-peel)，但是对于它们在语义上是否合理存在一些争论，尤其是关于他们如何处理异常和类似的奇怪的IOy 事情.

This can't be done generically over all MonadIO instances because of the IO type in a negative position. There are some libraries on hackage that do this for specific instances (monad-control, monad-peel), but there's been some debate over whether they are semantically sound, especially with regards to how they handle exceptions and similar weird IOy things.

有些人似乎对正/负位置区别感兴趣.实际上，没什么好说的(您可能已经听说过，但名称不同).该术语来自子类型的世界.

Some people seem interested in the positive/negative position distinction. Actually, there's not much to say (and you've probably already heard it, but by a different name). The terminology comes from the world of subtyping.

子类型背后的直觉是a 是 b 的子类型(我将写成 a <= b)，当a 可以用在任何需要 b 的地方".在很多情况下，决定子类型很简单.对于产品，(a1, a2) <= (b1, b2) 每当 a1 <= b1 和 a2 <= b2，例如，这是一个非常简单的规则.但是有一些棘手的情况；例如，我们什么时候应该决定 a1 ->a2<=b1->b2?

The intuition behind subtyping is that "a is a subtype of b (which I'll write a <= b) when an a can be used anywhere a b was expected instead". Deciding subtyping is straightforward in a lot of cases; for products, (a1, a2) <= (b1, b2) whenever a1 <= b1 and a2 <= b2, for example, which is a very straightforward rule. But there are a few tricky cases; for example, when should we decide that a1 -> a2 <= b1 -> b2?

好吧，我们有一个函数 f :: a1 ->a2 和一个需要 b1 -> 类型函数的上下文b2.所以上下文将使用 f 的返回值，就好像它是一个 b2，因此我们必须要求 a2 <= b2.棘手的是上下文将提供带有 b1 的 f，即使 f 会像使用它一样使用它一个 a1.因此，我们必须要求 b1 <= a1 —— 这与您可能猜到的相反！我们说a2 和b2 是协变的"，或者出现在正位"，而a1 和b1code> 是逆变的"，或者出现在负的位置".

Well, we have a function f :: a1 -> a2 and a context expecting a function of type b1 -> b2. So the context is going to use f's return value as if it were a b2, hence we must require that a2 <= b2. The tricky thing is that the context is going to be supplying f with a b1, even though f is going to use it as if it were an a1. Hence, we must require that b1 <= a1 -- which looks backwards from what you might guess! We say that a2 and b2 are "covariant", or occur in a "positive position", and a1 and b1 are "contravariant", or occur in a "negative position".

(顺便说一句:为什么是正"和负"?它的动机是乘法.考虑这两种类型:

(Quick aside: why "positive" and "negative"? It's motivated by multiplication. Consider these two types:

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

什么时候 f1 的类型应该是 f2 类型的子类型?我陈述这些事实(练习:使用上面的规则检查这一点):

When should f1's type be a subtype of f2's type? I state these facts (exercise: check this using the rule above):

• 我们应该有 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，在整个类型中处于负数位置.正 * 负 * 负 = 正，它是协变的.你明白了.)

e1 is in a positive position in d1 -> e1, which is in turn in a positive position in the type of f1; moreover, e1 is in a positive position in the type of f1 overall (since it is covariant, per the fact above). Its position in the whole term is the product of its position in each subterm: positive * positive = positive. Similarly, d1 is in a negative position in d1 -> e1, which is in a positive position in the whole type. negative * positive = negative, and the d variables are indeed contravariant. b1 is in a positive position in the type a1 -> b1, which is in a negative position in (a1 -> b1) -> c1, which is in a negative position in the whole type. positive * negative * negative = positive, and it's covariant. You get the idea.)

现在，让我们来看看 MonadIO 类:

Now, let's take a look at the MonadIO class:

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

我们可以将其视为子类型的显式声明:我们提供了一种方法，使 IO a 成为某些具体 m<的 ma 的子类型/代码>.我们马上就知道我们可以使用 IO 构造函数在正位置取任何值并将它们转换为 ms.但这就是全部:我们无法将否定的 IO 构造函数转换为 ms —— 为此我们需要一个更有趣的类.

We can view this as an explicit declaration of subtyping: we are giving a way to make IO a be a subtype of m a for some concrete m. Right away we know we can take any value with IO constructors in positive positions and turn them into ms. But that's all: we have no way to turn negative IO constructors into ms -- we need a more interesting class for that.

这篇关于在 Haskell 中提升高阶函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！