将A => M [B]变为M [A => B]

Question

对于monad M,是否有可能A => M[B]变成M[A => B]？

我试过跟踪这些类型无济于事,这让我认为这是不可能的,但我想我还是会问.此外,搜索Hoogle a -> m b -> m (a -> b)没有返回任何东西,所以我不会抱太多运气.

Answer 1

在实践中

不,这是不可能的,至少不是以有意义的方式.

考虑一下这个Haskell代码

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

这需要n第一,打印它(IO执行这里),然后读取来自用户的线路.

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

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

以上必须事先做所有的IO,才知道n,然后返回一个纯函数.这不能等同于上面的代码.

要强调这一点,请考虑以下无意义的代码:

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

奇怪的是,action'应该事先知道用户下一步要输入的内容!会话看起来像

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)

这需要一台时间机器,因此无法完成.

理论上

不,它无法完成.这个论点类似于我对类似问题的论证.

假设transform :: forall m a b. Monad m => (a -> m b) -> m (a -> b)存在矛盾.专注m于continuation monad ((_ -> r) -> r) (我省略了newtype包装器).

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

通过库里 - 霍华德的同构,以下是一种直觉主义的同义反复

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

但这是皮尔士定律,这在直觉主义逻辑中是不可证明的.矛盾.