10 Apr 14:48 2009

## Re: Referential Transparency and Monads

Jason Dusek <jason.dusek <at> gmail.com>

2009-04-10 12:48:47 GMT

2009-04-10 12:48:47 GMT

2009/04/09 Mark Spezzano <mark.spezzano <at> chariot.net.au>: > How exactly do monads “solve” the problem of referential transparency? I > understand RT to be such that a function can be replaced with a actual > value. With referential transparency, an **expression** can be replaced with an evaluated variant of itself. When we choose to do the evaluation is not important. So we have some function: f :: SomeType -> SomeOther -> YetAnother -> SomethingElse One time, when we encounter `f a b c` and evaluate it to get `d`. Now whenever we see `f a b c` again, referential transparency tells us we can just stick the `d` right there and not bother about running the program that is inside `f`. What you have with the IO monad is things that look like the same expression but actually aren't; you also have rules of evaluation that force the reduction strategy to reduce things in order. Consider this: main = do c0 <- getChar c1 <- getChar print c1 At first glance, Pooh (or even Owl) might say, "The first `getChar` is just the same as the second.". Doesn't referential transparency say that we should just evaluate it one time and thus get only the first character in the stream? Well, no. Doesn't laziness say, we only need `c1` so we'll just read the first character off the stream? No again. The do notation is a great convenience; it is syntax transformed to this: main = getChar >>= (\c0 -> (getChar >>= (\c1 -> print c1))) We see right away that, in order to get at the second `getChar`, we need to provide an argument to the first lambda. Likewise, to get at the `print`, we need to provide an argument to the second lambda. The `>>=` is called "bind" and plays an essential role here. Each monad has its own bind -- bind is an integral part of its evaluation strategy. Let us consider a simplified implementation of the IO monad: data World = World ... data IO t = IO (World -> (t, World)) Every value of type `IO t` contains a function that takes us from `World` to a pair of `World` and `t`. The `World` is not important beyond the notion that no two are alike. Our implementation of `>>=` (also simplified compared to a real one): >>= :: IO a -> (a -> IO b) -> IO b IO act1 >>= f = IO (\w1 -> let { (t, w2) = act1 w1 ; IO act2 = f t } in act2 w2) Then we have `getChar` and `print`: getChar = IO charOp {- `charOp` is some unsafe operation that does the getting. -} print something = IO (printOp something) {- `printOp` is some unsafe operation that does the printing. -} Now let's substitute that into the above and see what we get: main = getChar >>= (\c0 -> (getChar >>= (\c1 -> print c1))) main = IO charOp >>= (\c0 -> (getChar >>= (\c1 -> print c1))) main = IO (\w1 -> let (c, w2) = charOp w1 IO act2 = (\c0 -> (getChar >>= (\c1 -> print c1))) c in act2 w2 ) main = IO (\w1 -> let (c, w2) = charOp w1 IO act2 = (getChar >>= (\c1 -> print c1)) in act2 w2 ) Let's work on just `act2`: IO act2 = (getChar >>= (\c1 -> print c1)) IO act2 = (IO charOp >>= (\c1 -> print c1)) IO act2 = IO (\w -> let (c', w3) = charOp w IO act3 = (\c1 -> print c1) c' in act3 w3 ) IO act2 = IO (\w -> let (c', w3) = charOp w IO act3 = print c' in act3 w3 ) IO act2 = IO (\w -> let (c', w3) = charOp w IO act3 = IO (printOp c') in act3 w3 ) IO act2 = IO (\w -> let (c', w3) = charOp w in (printOp c') w3 ) IO act2 = IO (\w -> let (c', w3) = charOp w in (printOp c') w3) Substituting: main = IO (\w1 -> let (c, w2) = charOp w1 IO act2 = IO (\w -> let (c', w3) = charOp w in (printOp c') w3) in act2 w2 ) main = IO (\w1 -> let (c, w2) = charOp w1 in (\w -> let (c', w3) = charOp w in (printOp c') w3) w2 ) main = IO (\w1 -> let (c, w2) = charOp w1 in let (c', w3) = charOp w2 in (printOp c') w3 ) So we let's review. Are the two `getChar`s the same expression? No -- one is called against one world, the other against another. Furthermore, they are ordered -- we need the world from the first one to get the world from the second. We need the second world to `print`. This is guaranteed by the semantics of "bind" in the IO monad. The expressions are not the same so referential transparency does not does not lead to dangerous elision; the data dependencies are explicit and so there is no way to re-order the evaluation of the expressions. Notice that these properties fall out of our rules for evaluation and not any "special sauce" for monads. > Just curious as to the rationale behind referential > transparency and how it applies to monads. That depends on the monad. -- Jason Dusek