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

Question

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.

Strephonn

(side note: you really wanted Monad m => (a -> m b) -> m (a ->b) from Hoogle. Note the extra brackets, meaning one argument rather than "two". Of course, as chi has proven, that type isn't inhabited beyond use of bottom, so you'll still get no results.) – Infundibulum

Answer 1

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.

Countermarch

Can you give a definition for transform? – Scheers

@user5402 transform is a theoretical function requested by OP – Prescription

@user5402 The above actually shows that transform can not be implemented. – Countermarch

@user5402 It can exist for some specific monads (e.g. Reader), but not for all monads (e.g. IO). – Countermarch

@chi: Can you recommend a book where one can learn more about Curry-Howard, Peirce's law, etc? Is "Type Theory & Functional Programming" by Simon Thompson still relevant (1991)? – Homespun

@Homespun That book is nice, in my opinion. I do not know about books covering general and more advanced material. I'd like to see one myself. Some general fact can be found in Coq's books or in the HoTT book, even though the aim of these is more precise. I would also recommend to learn about cut-elimination and sequent calculus -- I would not be able to prove that Peirce's law is not provable in IPC otherwise. – Countermarch

@chi: Where IPC stands for…? So far I've only had a look at ZFC. But BTT: I would add that it's possible to write transform if M is also a comonad: return . (extract . ). – Homespun

@Homespun IPC = Intuitionistic Propositional Calculus – Countermarch

"The above has to do all the IO in advance, before knowing n". Sam Lindley has a nice characterization of idiom, arrow and monad in terms of data / control flow which is clearly making that point. pdf of the paper. – Haematite

Yum: I love me some Howard curry. So in practice, if one had a time machine, one could do the transformation on at least one case. Is a time machine sufficient in general, and how would it invalidate the proof? ;) – Wilcher

@Yakk It does not invalidate the proof. In fact, using said time machine I can prove that the statement is both true and false at the same time (fetch the proof today, remember to send back a copy tomorrow). So, in particular, the statement is true. :P – Countermarch

Thanks for the constructive and detailed response. Yeah, the more I think about it the less sense it makes. I suppose it's one of those times where thinking about it in terms of concrete implementations rather than in an abstract way helps. – Strephonn

Your theoretical explanation could be turned into a practical one by noting that the only way to get an a out of an (a->b)->a is to supply an a->b, and there's no way to make one of those without knowing anything more about a and b. – Sigrid

Answer 2

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

Blumenthal

Answer 3

No.

For example, Option is a monad, but the function (A => Option[B]) => Option[A => B] has no meaningful implementation:

def transform[A, B](a: A => Option[B]): Option[A => B] = ???

What do you put instead of ???? Some? Some of what then? Or None?

Brume

Although the answer is correct, beware of "proof by lack of imagination". – Licking

Answer 4

Just to complete @svenningsson's answer. One example where it is particularly useful is in QuickCheck to generate random functions. The generator there is defined as:

newtype Gen a = MkGen {
  unGen :: QCGen -> Int -> a
}

And it has a Monad instance which is in a sense Reader but with bind always splitting random generator for all sub-computations.

That means we can define a function which acts on a generator as a generator of functions!

promote :: (a -> Gen b) -> Gen (a -> b)
promote f = MkGen $ \gen n -> \a -> let MkGen h = f a in h gen n

And it is even more general in the library.

Now the problem is how to get a function which acts on generators in the first place, but that's another question which is nicely explained here.

Obduliaobdurate