在Haskell中提升高阶函数

Question

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

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

tmonad变压器在哪里？具体来说,我有兴趣这样做:

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

我摆弄了一些Haskell巫术库,但无济于事.我如何做到正确,或者在某个我找不到的地方有一个现成的解决方案？

Answer 1

MonadIO由于IO类型处于负位置,因此无法在所有实例中进行此操作.hackage上有一些库可以针对特定实例(monad-control,monad-peel)执行此操作,但是关于它们是否在语义上是合理的,特别是关于它们如何处理异常和类似的奇怪IO事物,存在一些争论.

编辑:有些人似乎对积极/消极的地位区分感兴趣.实际上,没有什么可说的(你可能已经听过了,但用不同的名字).术语来自子类型世界.

子类型背后的直觉是" 当一个可以在预期的任何地方使用时,它a是b(我将写的a <= b)的子类型".在很多情况下,确定子类型很简单; 产品,只要和,例如,这是一个非常简单的规则.但是有一些棘手的案例; 例如,我们什么时候应该决定？ab(a1, a2) <= (b1, b2)a1 <= b1a2 <= b2a1 -> a2 <= b1 -> b2

好吧,我们有一个函数f :: a1 -> a2和一个期望类型函数的上下文b1 -> b2.因此,上下文将使用f返回值,就像它是a一样b2,因此我们必须要求它a2 <= b2.棘手的是,上下文将提供f一个b1,即使f它将使用它,就像它是一个a1.因此,我们必须要求b1 <= a1- 从你可能猜到的东西向后看!我们说a2并且b2是"协变",或者发生在"正面位置",a1并且b1是"逆变",或者发生在"负面位置".

(撇开:为什么"积极"和"消极"？它的动机是乘法.考虑这两种类型:

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成为m a某些具体的子类型m.我们知道我们可以在IO构造函数处于正位置时采用任何值,并将它们转换为ms.但这就是全部:我们无法将负面IO构造函数转换为ms - 我们需要一个更有趣的类.