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.
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.
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.
The other replies have nicely illustrated that in general it is not possible to implement a function from a -> m b
to m (a -> b)
for any monad m
. However, there are specific monads where it is quite possible to implement this function. One example is the reader monad:
data Reader r a = R { unR :: r -> a } commute :: (a -> Reader r b) -> Reader r (a -> b) commute f = R $ \r a -> unR (f a) r
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With