4

There have been claims that the IO monad has no monad transformer, or even cannot have a monad transformer. Why is there no IO transformer in Haskell?

First question: Then, what is this code? https://hackage.haskell.org/package/acme-iot-0.1.0.1/docs/Control-Monad-Trans-IO.html Is this not a monad transformer for IO, "adding IO capabilities to any monad" as the documentation says?

Second question: There is this blog post: http://h2.jaguarpaw.co.uk/posts/io-transformer/ where it is claimed that IOT m a = (forall x. m x -> IO x) -> IO a is a monad transformer for IO applied to an arbitrary foreign monad m. It is assumed, however, that the functions of type m x -> IO x must be monad morphisms. The blog post elaborates on this to show that (at least) the monad morphism laws hold for the map m a -> IOT m a.

Now, this construction seems to apply to arbitrary monads and seems to give a formula for a monad transformer for a completely arbitrary base monad Base a. The monad transformer BaseT is defined by:

 BaseT base m a = (forall x. m x -> base x) -> base a

Here the functions of type forall x. m x -> base x are assumed to be monad morphisms. (The code does not express that requirement in the type.)

Does this formula give a completely general monad transformer for any base monad base and any foreign monad m?

Are there monad morphisms lift: m a -> BaseT base m a and hoist :: (forall x. m x -> n x) -> BaseT base m a -> BaseT base n a?

Are there any other laws that a monad transformer must satisfy and BaseT does not satisfy?

One of my misgivings about BaseT is that the type forall x. m x -> base x could be void, for some m and base, even if we do not assume that it must be a monad morphism. There are some monads m and base for which there are simply no natural transformations of type forall x. m x -> base x, for example, m a = Maybe a and base a = a. So, in that case, the void type gets substituted into the formula and we get BaseT base m a = Void -> m a, which is equivalent to Unit. A monad transformer that is identically equal to Unit is useless for practical applications but does satisfy the monad morphism laws (as Unit is a lawful monad and any other monad can be mapped to Unit by a monad morphism). So, BaseT base m may not give a useful answer for some base and m. Does it mean that it is nevertheless useful when base = IO?

winitzki
  • 3,179
  • 24
  • 32
  • Implementing `lift` and `hoist` is easy, you should try it yourself. Also, you can find the laws which must be satisfied on [wikipedia](https://en.wikipedia.org/wiki/Monad_transformer). – Noughtmare Mar 23 '23 at 10:49
  • @Noughtmare The laws listed in wikipedia are not enough to ensure that a monad transformer is actually useful. For example, as I wrote in my post, we can just define `t m a = Unit` and it will satisfy all laws but it's completely useless. There must be more laws, at least there must be some non-degeneracy laws to ensure that a monad b's monad transformer applied to a monad `m` actually includes the effects of both monads. – winitzki Mar 23 '23 at 11:14
  • @Noughtmare Implementing is easy, proving the monad morphism laws is less easy. – winitzki Mar 23 '23 at 11:14
  • In light of your comments I'd recommend to focus your question more on one particular question. Is your question whether `BaseT` is useful (be careful to avoid asking for opinions), or whether it satisfies the laws (show where you get stuck in proving the laws), or whether it is possible to implement `lift` and `hoist`, or ...? – Noughtmare Mar 23 '23 at 11:39
  • 1
    Already mentioned in the answers, but there exists the convention that Hackage packages which begin with "acme-" https://hackage.haskell.org/packages/search?terms=acme are "joke" packages that do some thing in an extremely convoluted way, claim some kind of "safety" while in reality being really unsafe, or claim to do something that is actually impossible. The name of course is a reference to the fictional Acme corporation in the Road Runner cartoons https://en.wikipedia.org/wiki/Acme_Corporation – danidiaz Mar 23 '23 at 14:25

1 Answers1

3

acme-iot, as its name implies, is a joke package. It breaks purity. The following program prints when a value is forced (which would require unsafeInterleaveIO or unsafePerformIO).

module Main where

import Control.Monad.Trans.IO
import Control.Monad.Trans.Class

e :: IOT [] ()
e = do
  x <- lift [1,2]
  sequenceIO [print (x :: Int)]

main :: IO ()
main = do
  _ <- runIOT e -- prints nothing

  [a,b] <- runIOT e  -- a, b :: ()  -- prints nothing
  b `seq` pure ()  -- prints 2  (even though  () `seq` pure ()   should be equal to  pure ())
  a `seq` pure ()  -- prints 1

The notion of "a monad transformer for a particular monad" is not well-defined. One may be "a monad transformer t such that t Identity is isomorphic to IO", and the generic construction you point out does satisfy that definition. The myth that there is no "IO monad transformer" comes from a mix of (1) if you make strong enough requirements for what that even means it may indeed not exist, (2) when it does exist, there may be no use case for such a thing.

Another generic construction that may be relevant is the free monad transformer. FreeT IO is a monad transformer and it has IO in it.

Li-yao Xia
  • 31,896
  • 2
  • 33
  • 56
  • A "monad transformer for a particular base monad `b`" is in my view well defined: as you say, it is a transformer `t` such that `t Identity` is isomorphic to `b`. It is useful to talk about a "transformer for a given monad" because that's what a programmer usually needs in the code (to combine two or more monads). Also, since `FreeT IO Identity` is isomorphic to `Free IO` but not isomorphic to `IO`, I would not say that `FreeT IO` is a monad transformer for `IO`. – winitzki Mar 23 '23 at 11:10
  • The usual definition of monad transformer is that there must be a monad morphism `m a -> t m a`. This is not enough to make it useful. For example, `t m a = Unit` is useless but satisfies the requirement of having a monad morphism. There must be more laws for monad transformers to be useful. For example, there must be a non-degeneracy law of some kind. – winitzki Mar 23 '23 at 11:12
  • You can quotient `FreeT IO` by a suitable equivalence relation. – Li-yao Xia Mar 23 '23 at 11:32
  • You say in your answer that "t Identity is isomorphic to IO" for the construction in my question. I thought so too, but now I looked back and see that `IOT Identity` is actually not `IO` but instead `IOT Identity a = IO Unit -> IO a`. And in general `BaseT base Identity a = base Unit -> base a` and not just `base a`. So, `BaseT` is a transformer for the (valid) monad `base Unit -> base a`. – winitzki Mar 26 '23 at 19:50
  • The isomorphism assumes that `forall a. m a -> IO a` denotes monad morphisms. – Li-yao Xia Mar 27 '23 at 08:12
  • Yes, thank you, I forgot about that requirement. The type of monad morphisms `forall a. a -> IO a` is isomorphic to `Unit` because there is only one monad morphism `Identity -> m` for any monad `m`. – winitzki Mar 27 '23 at 09:46