转动 A =>M[B] 到 M[A =>乙] [英] Turning A => M[B] into M[A => B]

问题描述

对于一个monad M，是否可以将A =>M[B] 变成 M[A =>B]?

For a monad M, Is it possible to turn A => M[B] into M[A => B]?

我试过遵循这些类型无济于事，这让我认为这是不可能的，但我想我还是会问.另外，在 Hoogle 中搜索 a ->m b ->m (a -> b) 没有返回任何东西，所以我运气不佳.

I've tried following the types to no avail, which makes me think it's not possible, but I thought I'd ask anyway. Also, searching Hoogle for a -> m b -> m (a -> b) didn't return anything, so I'm not holding out much luck.

推荐答案

实践中

不，它不能完成，至少不能以有意义的方式完成.

In Practice

No, it can not be done, at least not in a meaningful way.

考虑这个 Haskell 代码

Consider this Haskell code

action :: Int -> IO String
action n = print n >> getLine

这首先需要 n，打印它(这里执行 IO)，然后从用户那里读取一行.

This takes n first, prints it (IO performed here), then reads a line from the user.

假设我们有一个假设的 transform :: (a -> IO b) ->IO (a -> b).然后作为一个心理实验，考虑:

Assume we had an hypothetical transform :: (a -> IO b) -> IO (a -> b). Then as a mental experiment, consider:

action' :: IO (Int -> String)
action' = transform action

上面要提前做好所有的IO，才知道n，然后返回一个纯函数.这不能等价于上面的代码.

The above has to do all the IO in advance, before knowing n, and then return a pure function. This can not be equivalent to the code above.

为了强调这一点，请考虑下面这段无意义的代码:

To stress the point, consider this nonsense code below:

test :: IO ()
test = do f <- action'
          putStr "enter n"
          n <- readLn
          putStrLn (f n)

神奇的是，action' 应该提前知道用户接下来要输入什么！一个会话看起来像

Magically, action' should know in advance what the user is going to type next! A session would look as

42     (printed by action')
hello  (typed by the user when getLine runs)
enter n
42     (typed by the user when readLn runs)
hello  (printed by test)

这需要时间机器，所以做不到.

This requires a time machine, so it can not be done.

不，这是不可能的.这个论点类似于我对类似问题提出的论点.

No, it can not be done. The argument is similar to the one I gave to a similar question.

矛盾假设 transform :: forall m a b.单子 m =>(a -> m b) ->m (a -> b) 存在.将 m 特化为 continuation monad ((_ -> r) -> r)(我省略了 newtype 包装器).

Assume by contradiction transform :: forall m a b. Monad m => (a -> m b) -> m (a -> b) exists. Specialize m to the continuation monad ((_ -> r) -> r) (I omit the newtype wrapper).

transform :: forall a b r. (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

专门化r=a:

transform :: forall a b. (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

申请:

transform const :: forall a b. ((a -> b) -> a) -> a

根据 Curry-Howard 同构，以下是一个直觉重言式

By the Curry-Howard isomorphism, the following is an intuitionistic tautology

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

但这是皮尔斯定律，在直觉逻辑中无法证明.矛盾.

but this is Peirce's Law, which is not provable in intuitionistic logic. Contradiction.

这篇关于转动 A =>M[B] 到 M[A =>乙]的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！