转向A => M [B]变换成M [A => B] [英] Turning A => M[B] into M[A => B]
问题描述
对于monad M
,是否可以将 A => M [B]
到 M [A => B]
?
我尝试过以下类型无济于事,这让我觉得这是不可能的,但我认为我会反正问问题。此外,在Hoogle中搜索 a - > m b - > m(a - > b)
没有返回任何东西,所以我没有多少运气。 / b> 练习
不,不能这样做,至少不能以有意义的方式。
考虑这个Haskell代码
action :: Int - > IO字符串
操作n =打印n>> getLine
首先打印 n
(IO在这里执行),然后从用户读取一行。
假设我们有一个假设
transform ::(a - > IO b ) - > IO(a - > b)
。然后作为心理实验,考虑:$ b
action':: IO(Int - > String )
action'=转换动作
以上所有事先都要做IO,在知道 n
之前,然后返回一个纯函数。这不能等同于上面的代码。
为了强调这一点,请考虑下面这个无意义的代码:
test :: IO()
test = do f < - action'
putStrenter n
n< ; - readLn
putStrLn(fn)
神奇地, action'
应该事先知道用户将要输入的内容!一个会话看起来像
42(由行动打印)
hello(输入用户在getLine运行时)
输入n
42(在readLn运行时由用户键入)
hello(由测试打印)
这需要一个时间机器,所以它不能完成。
理论上
不,不能完成。这个论点类似于我给类似问题的一个。
假设矛盾 transform :: forall ma b。 Monad m => (a - > m b) - > m(a - > b)
存在。
对继续monad ((_ - > r) - > r)
进行特殊设置 m
我省略了newtype wrapper)。
transform :: forall ab 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
通过咖喱霍华德同构,以下是一个直觉主义重言式$ b $ ((A→B)→A)→B→B $ b <$ P $ A
但这是皮尔士定律,这在直觉逻辑中是不可证明的。矛盾。
For a monad M
, Is it possible to turn A => M[B]
into 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.
Consider this Haskell code
action :: Int -> IO String
action n = print n >> getLine
This takes n
first, prints it (IO performed here), then reads a line from the user.
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
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)
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.
In Theory
No, it can not be done. The argument is similar to the one I gave to a similar question.
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
Specialize r=a
:
transform :: forall a b. (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a
Apply:
transform const :: forall a b. ((a -> b) -> a) -> a
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 => B]的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!