Re: [Haskell-cafe] Referential Transparency and Monads

10 Apr 2009

      2009/04/09 Mark Spezzano :
...
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