如何将高阶函数应用于Haskell中的有效函数？ [英] How to apply higher order function to an effectful function in Haskell?

问题描述

我有太多的功能：

  higherOrderPure ::（a  - > b） - > c 
有效:: Monad m => （a  - > mb）
  

我想将第一个函数应用于第二个函数： / p>

  higherOrderPure`someOp` effectful :: Monad m => mc 
  

其中

  someOp :: Monad m => （（a→b）→c）→> （a  - > m b） - > mc 
  

示例：

  curve ::（Double  - > Double） - > Dia任何
曲线f = fromVertices $ map p2 [（x，f x）| x < -  [1..100]] 
 
 func :: Double  - >或者String Double 
 func _ = LeftParse error - 在其他情况下，这个func可以作为一个有用的算术运算作为一个Right值
 
 someOp ::（（Double  - > Double ） - >直径任意） - > （双 - >任一字符串双） - >或者String（Dia Any）
 someOp = ??? 
 
 curve`someOp` func ::任一字符串（Dia Any）
  

解决方案

类型

  Monad m => （（a→b）→c）→> （a  - > m b） - > mc 
  

没有人居住，即没有任何词语 t 具有该类型（除非你利用分歧，例如无限递归，错误， undefined 等） 。

不幸的是，这是不可能实现的。 someOp 。

证明

为了证明构建这样一个 t 是不可能的，我们通过矛盾进行。
假设 t 存在于类型

中

  t :: Monad m => （（a→b）→c）→> （a  - > m b） - > mc 
  

现在，将 c 改为（a - > b）。我们获得

  t :: Monad m => （（a→b）→a→b）→> （a  - > m b） - > m（a  - > b）
  

因此，

  t id :: Monad m => （a  - > m b） - > m（a  - > b）
  

然后，将monad m 延续monad （* - > r） - > r

  t id ::（a  - >（b  - > r） - > ; r） - > （（a→b）→r）→> r 
  

进一步特殊化 r 至 a

  t id ::（a  - >（b  - > a ）→> a）→> （（a→b）→a）→ a 
  

因此，我们获得

<$ p $ （a - > b） - > a） - > a

最后，由 Curry-Howard同构，我们推断以下是一个直觉主义同语：

<$ p $ （（A-> B） - > A） - > A

但以上是众所周知的 Peirce's law ，这在直觉主义逻辑中是不可证明的。因此，我们得到一个矛盾。

结论

以上证明 t 不能以一般方式实现，即以任何monad工作。在一个特定的monad中，这仍然是可能的。

I have too functions:

higherOrderPure :: (a -> b) -> c
effectful :: Monad m => (a -> m b)

I'd like to apply the first function to the second:

higherOrderPure `someOp` effectful :: Monad m => m c

where

someOp :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Example:

curve :: (Double -> Double) -> Dia Any 
curve f = fromVertices $ map p2 [(x, f x) | x <- [1..100]]

func :: Double -> Either String Double
func _ = Left "Parse error" -- in other cases this func can be a useful arithmetic computation as a Right value

someOp :: ((Double -> Double) -> Dia Any) -> (Double -> Either String Double) -> Either String (Dia Any)
someOp = ???

curve `someOp` func :: Either String (Dia Any)

解决方案

The type

Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

is not inhabited, i.e., there is no term t having that type (unless you exploit divergence, e.g. infinite recursion, error, undefined, etc.).

This means, unfortunately, that it is impossible to implement the operator someOp.

Proof

To prove that it is impossible to construct such a t, we proceed by contradiction. Assume t exists with type

t :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Now, specialize c to (a -> b). We obtain

t :: Monad m => ((a -> b) -> a -> b) -> (a -> m b) -> m (a -> b)

Hence

t id :: Monad m => (a -> m b) -> m (a -> b)

Then, specialize the monad m to the continuation monad (* -> r) -> r

t id :: (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

Further specialize r to a

t id :: (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

So, we obtain

t id const :: ((a -> b) -> a) -> a

Finally, by the Curry-Howard isomorphism, we deduce that the following is an intuitionistic tautology:

((A -> B) -> A) -> A

But the above is the well-known Peirce's law, which is not provable in intuitionistic logic. Hence we obtain a contradiction.

Conclusion

The above proves that t can not be implemented in a general way, i.e., working in any monad. In a specific monad this may still be possible.

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