[Haskell-cafe] Referential Transparency and Monads

[Jonathan Cast]

On Thu, 2009-04-09 at 22:47 -0400, Brandon S. Allbery KF8NH wrote:
> On 2009 Apr 9, at 22:30, Jonathan Cast wrote:
> > On Thu, 2009-04-09 at 21:57 -0400, Brandon S. Allbery KF8NH wrote:
> >> On 2009 Apr 9, at 16:09, Luke Palmer wrote:
> >>> On Thu, Apr 9, 2009 at 1:33 PM, Miguel Mitrofanov
> >>> <miguelimo38 at yandex.ru> wrote:
> >>>                I'm not sure what you mean by that, but semantically
> >>>                IO is definitely
> >>>                *not* a state monad.  Under any circumstances or any
> >>>                set of assumptions.
> >>>
> >>>        Ehm? Why not?
> >>>
> >>> Mainly forkIO.  There may be other reasons.
> >>
> >> I thought I had excluded that stuff to simplify the question; the  
> >> fact
> >> that IO is Haskell's toxic waste dump is more or less irrelevant to
> >> the core concept.
> >
> > Well, the `core concept' of IO includes the concept of a user who's
> > watching and interacting with your program as it runs, no?
> 
> Yes.  That's the opaque "real world";  an I/O operation conceptually  
> modifies this state,

Pedantic nit-pick: modification is not referentially transparent.  You
mean `returns a modified copy'.

> which is how things get tied together.  Ordinary  
> user programs can't interact with the "real world" sate except via  
> functions defined on IO, which are assumed to modify the state; that's  
> exactly how non-RT actions are modeled via RT code.
> 
> Stuff like forkIO and newIORef can also be understood that way, it's  
> just a bit more complex to follow them around.
> 
> Please note that ghc *does* implement IO (from Core up, at least) this  
> way, modulo unboxed tuples, so claims that it is "wrong" are dubious  
> at best.

No, GHC implements IO using an internal side-effectful language.  (Note
that the `state' IO uses internally is an (un-boxed and un-pointed)
0-bit word!  It certainly doesn't have enough semantic content
to /actually/ contain the entire state of the computer.)  The difference
between GHC core and a truly referentially transparent language is that
you can't implement unsafePerformIO unless your language has side
effects.

Oh, and I should have cited Tackling the Awkward Squad as the source of
my dubious claim.

> >     s <- readFile "/my_file"
> >     writeFile "/my_file" "Hello, world!\n"
> >     threadDelay 10000 -- If you don't like threadDelay, just  
> > substitute forcing
> >                       -- an expensive thunk here
> >     writeFile "/my_file" s
> >
> > As a function from initial state to final state, this program is just
> > the identity; but surely this program should be considered different
> 
> It is?
> 
>  > -- these implicitly are considered to return a modified RealWorld
>  > readFile :: RealWorld -> (String,RealWorld)
>  > writeFile :: RealWorld -> ((),RealWorld)
>  > threadDelay :: RealWorld -> ((),RealWorld)
>  >
>  > main :: RealWorld -> ((),RealWorld)
>  > main state =
>  >   case readFile state "/my_file" of
>  >     (s,state') ->
>  >        case writeFile state' "/my_file" "Hello, world!\n" of
>  >          (_,state'') ->
>  >             case threadDelay state'' 10000 of
>  >               (_,state'') -> writeFile "/my_file" s state''

(This has arguments very much in the wrong order throughout, of course.)

> This is just the State monad, unwrapped.

What on earth does that have to do with anything?  If I change your last
line to

>                 (_,state''') -> case writeFile "/my_file" s state''' of
>                    (x, state'''') -> (x, state'''')

Then I can observe that state'''', if it really names the current state
of the system as of the program's finish-point, is exactly equivalent to
state (e.g., in both states every file has exactly the same contents).
(The only difference, which I forgot, is that the current time is >
10sec later than in state.  Doesn't affect the point.)

Now, the *definition* you gave is, in form, different than the
definition of

  threadDelay 10000

However, the point of referential transparency is that you can inline
the definitions of readFile and writeFile into the scrutinees of your
case statements, and then (possibly after something like a case-of-case
transformation) you can eliminate the case expressions and intermediate
states and get something like:

  \ (!state) -> let
                  s = fileContents "/my_file" state
                in case threadDelay 10000 state of
                     (_, state') ->
                       ((), setFileContents "/my_file" s state')

where, since threadDelay has no side effects but increasing the current
time, 

     fileContents "/my_file" state'
  == fileContents "/my_file" state

so the above is equivalent to

  \ (!state) -> case threadDelay 10000 state of
       (_, state') ->
         ((), setFileContents "/my_file" (fileContents "/my_file"
state') state')

but obviously

     setFileContents fn (fileContents fn state') state'
  == state'

so therefore the above is equivalent to

  \ (!state) -> case threadDelay 10000 state of
       (_, state') ->
         ((), state')

which (since threadDelay is presumably strict in its state argument and
always returns ()) is equivalent to

  threadDelay 10000

as claimed. 

And if you don't see that, I really don't think I can put it more clearly than that.

> And the differences between  
> this and the actual GHC implementation

Implementation != semantics, btw.  And GHC's implementation is not
referentially transparent!

> are the use of unboxed tuples  
> and RealWorld actually being a type that can't be accessed by normal  
> Haskell code.

Pedantic nit-pick: State# (not RealWorld!) *is* a type that can be
accessed by normal Haskell code.  It's just not portable to do so (you
have to import one of the GHC.* modules).

jcc