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

问题描述

我试图构造一个类型的函数：
$ b

  liftSumthing ::（ a  - > mb） - > mb） - > （a  - > t m b） - > t m b 
  

其中 t 是一个monad变换器。具体来说，我有兴趣这样做：

  liftSumthingIO :: MonadIO m => （（a→IO b）→IO b）→> （a  - > m b） - > m b 
  

我摆弄了一些Haskell的魔法库，但无济于事。如何获得
的权利，或者有一个我找不到的准备好的解决方案？

解决方案

对于 MonadIO 实例，这是不可能的，因为 IO 类型处于负值位置。有一些关于hackage的库为特定实例执行此操作（ monad-control ， monad-peel ），但是他们是否在语义上听起来有些争议，特别是关于他们如何处理异常和类似的奇怪 IO y事情。

编辑：有些人似乎对正面/负面感兴趣位置区分。实际上，没有什么可说的了（你可能已经听说过了，但是以不同的名字）。子类型背后的直觉是： a 是子类型的子类型。 当$ a 时，我会写 a< = b c $ c>可以在任何需要 b 的地方使用。在很多情况下确定子类型是很直接的。对于产品，每当 a1 <= b1 和时，（a1，a2）<=（b1，b2） a2 <= b2 ，这是一个非常简单的规则。但是有一些棘手的案例。例如，我们应该什么时候决定 a1 - > a2 <= b1 - > b2 ？

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

（快速放在一边：为什么是正面和负面？它的动机是乘法。 c> f1 ::（（a1→b1）→c1）→（d1→e1）
f2 ::（（a2→b2）→c2）→ ;（d2 - > e2）

当 f1 的类型是 f2 类型的子类型吗？我陈述了这些事实（练习：使用上面的规则检查它）：

• 我们应该有 e1 <= e2 。


• d2 <= d1 。


• 我们应该有 c2 <= c1 。


• 我们应该有 b1 <= b2 。


• $ b

  e1 在<$中处于正面位置c $ c> d1 - > e1 ，这在 f1 类型中依次处于正面位置;此外， e1 在整体 f1 类型中处于积极的位置（因为它是协变的，根据上面的事实）。它在整个学期中的位置是它在每个子项中的位置的结果：positive * positive = positive。同样， d1 在 d1 - > e1 ，这在整个类型中处于积极的位置。负值*正值=负值， d 变量确实是逆变。 b1 在类型 a1 - > b1 ，它在（a1 - > b1） - > c1 ，它在整个类型中处于负值位置。正面*负面*负面=正面，而且是协变的。 ）

  
  
  

  现在，我们来看看 MonadIO 类：

    class Monad m => MonadIO m其中
   liftIO :: IO a  - > ma 
    

  我们可以将其视为子类型的明确声明：我们正在给出一种方法来使<对于某些具体的 m ，c $ c> IO a 是 ma 的子类型。马上我们知道我们可以用正值位置的 IO 构造函数取任何值，并将它们变成 m s。但就这些而言：我们无法将负面 IO 构造函数转化为 m s - 我们需要一个更有趣的类为此。

  
  

  I'm trying to construct a function of type:

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

  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
  

  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?

  解决方案

  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.

  Edit: 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.

  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?

  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)
  

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

  • We should have e1 <= e2.
  • We should have d2 <= d1.
  • We should have c2 <= c1.
  • We should have b1 <= b2.
  • We should have a2 <= a1.

  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.)

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

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

  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屋！