44

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.

Will Ness
  • 70,110
  • 9
  • 98
  • 181
Noel M
  • 15,812
  • 8
  • 39
  • 47
  • 8
    (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.) – AndrewC Dec 03 '14 at 14:22

4 Answers4

63

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.

Community
  • 1
  • 1
chi
  • 111,837
  • 3
  • 133
  • 218
  • Can you give a definition for `transform`? – ErikR Dec 03 '14 at 09:33
  • 5
    @user5402 `transform` is a theoretical function requested by OP – Odomontois Dec 03 '14 at 09:39
  • 5
    @user5402 The above actually shows that `transform` can not be implemented. – chi Dec 03 '14 at 09:40
  • 4
    @user5402 It can exist for some specific monads (e.g. Reader), but not for all monads (e.g. IO). – chi Dec 03 '14 at 09:45
  • 1
    @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)? – Zeta Dec 03 '14 at 10:01
  • 2
    @Zeta 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. – chi Dec 03 '14 at 10:20
  • 1
    @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 . )`. – Zeta Dec 03 '14 at 10:54
  • @Zeta IPC = Intuitionistic Propositional Calculus – chi Dec 03 '14 at 11:01
  • "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](http://homepages.inf.ed.ac.uk/slindley/papers/aeia.pdf). – gallais Dec 03 '14 at 11:16
  • 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? ;) – Yakk - Adam Nevraumont Dec 03 '14 at 14:38
  • @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 – chi Dec 03 '14 at 16:06
  • 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. – Noel M Dec 03 '14 at 17:20
  • 1
    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`. – dfeuer Mar 12 '15 at 20:33
4

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
svenningsson
  • 4,009
  • 1
  • 24
  • 32
2

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?

ZhekaKozlov
  • 36,558
  • 20
  • 126
  • 155
0

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.

RowanStone
  • 160
  • 3
  • 11