Search code examples
scalahaskelltypesmonadsscalaz

Turning A => M[B] into M[A => B]


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.


Solution

  • 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.