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?

On 2009 Apr 9, at 16:09, Luke Palmer wrote:

On Thu, Apr 9, 2009 at 1:33 PM, Miguel Mitrofanov

...

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. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

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 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, 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.

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

This is just the State monad, unwrapped. And the differences between this and the actual GHC implementation are the use of unboxed tuples and RealWorld actually being a type that can't be accessed by normal Haskell code. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

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 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

On 2009 Apr 10, at 0:14, Luke Palmer wrote:

On Thu, Apr 9, 2009 at 8:47 PM, Brandon S. Allbery KF8NH

...

wrote: Stuff like forkIO and newIORef can also be understood that way, it's just a bit more complex to follow them around.

Have you tried forkIO? I used to think that "world passing" was an acceptable, if ugly, semantics for IO. However, after doing some formal modeling, I realized that forkIO breaks the model altogether. What happens to the end state of the forked thread?

What happens to it when main returns? When you fork a subprocess, and when it exits? Same answer, although it might be better modeled as passing a reference to the RealWorld around to model independent threads all doing I/O (at least, I don't *think* forkIO is just a funny-looking unsafeInterleaveIO). In any case, threads and process forks do complicate things but could be emulated if I wanted to go to the effort of implementing green threads in single-threaded Haskell code; the RealWorld is the least of the problems introduced, it's best thought of as cloning part (threads) or all (processes) of the program's own state, which is *also* conceptually contained in the RealWorld. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On Fri, 2009-04-10 at 07:29 +0400, Miguel Mitrofanov wrote:

On 10 Apr 2009, at 06:30, Jonathan Cast wrote:

...

do 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;

No, since world state includes the user state itself, not just files contents.

My programs are passing me around inside a state token? jcc

Jonathan Cast wrote:

On Fri, 2009-04-10 at 07:29 +0400, Miguel Mitrofanov wrote:

...

On 10 Apr 2009, at 06:30, Jonathan Cast wrote:

...

do 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;

No, since world state includes the user state itself, not just files contents.

My programs are passing me around inside a state token?

Sure. http://en.wikipedia.org/wiki/File:8-cell.gif Inside and outside become quite mindboggling when dealing with more dimensions than you expect... -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

On 2009 Apr 10, at 0:33, Heinrich Apfelmus wrote:

Luke Palmer wrote:

...

Miguel Mitrofanov 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. loop' :: IO () loop' = putStr "o" >> loop'

are indistinguishable in the

IO a ~ World -> (a, World)

I still don't understand this; we are passing a World and getting a World back, *conceptually* the returned World is modified by putStr. It's not in reality, but we get the same effects if we write to a buffer and observe that buffer with a debugger --- state threading constrains the program to the rules that must be followed for ordered I/O, which is what matters. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On 2009 Apr 10, at 0:52, Jonathan Cast wrote:

On Fri, 2009-04-10 at 00:46 -0400, Brandon S. Allbery KF8NH wrote:

...

...

IO a ~ World -> (a, World)

I still don't understand this; we are passing a World and getting a World back,

We are? Why do you think that?

Because that's what (World -> (a,World)) means, last I checked. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On 2009 Apr 10, at 1:09, Jonathan Cast wrote:

On Fri, 2009-04-10 at 01:03 -0400, Brandon S. Allbery KF8NH wrote:

...

On 2009 Apr 10, at 0:52, Jonathan Cast wrote:

...

On Fri, 2009-04-10 at 00:46 -0400, Brandon S. Allbery KF8NH wrote:

...

...

IO a ~ World -> (a, World)

I still don't understand this; we are passing a World and getting a World back,

We are? Why do you think that?

Because that's what (World -> (a,World)) means, last I checked.

Does

undefined :: (a, World)

contain a World?

Does

undefined :: Sum Int

contain an Int? Please use some common sense, your recent responses are increasingly incoherent. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

2009/4/10 Stefan Monnier :

...

...

...

...

IO a  ~  World -> (a, World) I still don't understand this; we are passing a World and getting a World back, We are?  Why do you think that? Because that's what (World -> (a,World)) means, last I checked.

No: Hasekll functions are partial, which means that "a -> b" means "takes an object of type `a' and if it terminates, it returns an object of type `b'".  Note the "if it terminates".

Since neither loop nor loop' terminate, their return type is actually meaningless.

Why? They both return _|_, which is a quite legal value of that type.

       Stefan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

2009/4/10 Heinrich Apfelmus :

Brandon S. Allbery wrote:

...

Heinrich Apfelmus wrote:

...

loop' :: IO () loop' = putStr "o" >> loop'

are indistinguishable in the

IO a ~ World -> (a, World)

I still don't understand this; we are passing a World and getting a World back, *conceptually* the returned World is modified by putStr. It's not in reality, but we get the same effects if we write to a buffer and observe that buffer with a debugger --- state threading constrains the program to the rules that must be followed for ordered I/O, which is what matters.

Basically, the problem is that neither computation returns the final World because neither one terminates.

More precisely, the goal of the

IO a ~ World -> (a, World)

semantics is to assign each expression of type IO a a pure function World -> (a, World) . For instance, the expression

putChar 'c'

would be assigned a function

\world -> ((), world where 'c' has been printed)

or similar.

Now, the problem is that both loop and loop' are being assigned the same semantic function

loop ~ \world -> _|_ loop' ~ \world -> _|_

We can't distinguish between a function that mutilates the world and then doesn't terminate and a function that is harmless but doesn't terminate either. After all, both return the same result (namely _|_) for the same input worlds.

I'm not sure I follow.

ones = 1:ones

is similar to loop or loop' but I can 'take 5' from it. Even if loop or loop' do not terminate, some value is produced, isn't it ? Thu

2009/4/10 Heinrich Apfelmus :

minh thu wrote:

...

Heinrich Apfelmus wrote:

...

Basically, the problem is that neither computation returns the final World because neither one terminates.

More precisely, the goal of the

   IO a  ~  World -> (a, World)

semantics is to assign each expression of type  IO a  a pure function World -> (a, World) . For instance, the expression

   putChar 'c'

would be assigned a function

   \world -> ((), world where 'c' has been printed)

or similar.

Now, the problem is that both  loop  and  loop'  are being assigned the same semantic function

   loop   ~  \world -> _|_    loop'  ~  \world -> _|_

We can't distinguish between a function that mutilates the world and then doesn't terminate and a function that is harmless but doesn't terminate either. After all, both return the same result (namely _|_) for the same input worlds.

I'm not sure I follow.

...

ones = 1:ones

is similar to loop or loop' but I can 'take 5' from it.

Even if loop or loop' do not terminate, some value is produced, isn't it ?

No. Unlike  loop  and  loop'  which are both  _|_ ,  ones  is a proper value, namely it's an infinite list of 1 . Granted, saying that  ones is "terminating" is a bit silly, but it's not "non-terminating" in the sense that it's not _|_.

The fact that some recursive definition are _|_ and some are not is rather unsurprising when looking at functions. For instance,

  foo x = foo x                                -- is _|_   fac n = if n == 0 then 1 else n * fac (n-1)  -- is not _|_

For more on the meaning of recursive definitions, see also

  http://en.wikibooks.org/wiki/Haskell/Denotational_semantics

Here the detailed calculation of why both  loop  and  loop'  are _|_ :

*loop*

    loop = fix f where f = \x -> x

  Hence, the iteration sequence for finding the fixed point reads

    _|_     f _|_ = (\x -> x) _|_ = _|_

  and the sequence repeats already, so  loop = _|_ .

*loop'*

    loop' = fix f where f = \x -> putStr 'o' >> x

  Hence, the iteration sequence for finding the fixed point reads

    _|_     f _|_ = putStr 'o' >> _|_           = \w -> let (_,w') = putStr 'o' w in _|_ w'           = _|_

  Again, the sequence repeats already and we have  loop' = _|_ .

Makes sense. The thing that is lacking to show difference between these two functions is that there is no way to 'erase' information from the world. T.i., even _|_ w' can't "really" be _|_, it must be a value that contains all the information from w'. _|_ w' /= _|_ is nonsense, thus a state monad does not suffice. I wonder what does...

Regards, apfelmus

-- http://apfelmus.nfshost.com

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru

On Thu, Apr 9, 2009 at 11:46 PM, Brandon S. Allbery KF8NH wrote:

I still don't understand this; we are passing a World and getting a World back, *conceptually* the returned World is modified by putStr.  It's not in reality, but we get the same effects if we write to a buffer and observe that buffer with a debugger --- state threading constrains the program to the rules that must be followed for ordered I/O, which is what matters.

You might find it useful to back up and think about the nature of computation. I did, anyway, when I was slogging through this stuff. Computability is all based on intuition about the *process* of calculating (see section 9 I think it is of Turing's original paper). IO "operations" - whatever one calls them - are by definition not computable. "Referentially transparent IO expressions" is an oxymoron, since the operations involved do not (cannot) correspond to any process that corresponds intuitively to computation and thus cannot refer transparently. So (going back to your original question) we can never get RT, but we can get the next best thing, which is manageability, which is what monads and other IO techniques are all about. YMMV, but for me the IO-as-state-transformer-operating-on-World is quite misleading. It's one possible method for dealing with IO conceptually but it's easy to get the incorrect impression that IO *is* some kind of state transformation, when in fact there is no essential connection between the two. There is no "state" nor "transformation" involved; an IO expression just references the result of some indeterminate non-computing process, just like a referentially transparent expression like '3+2' references the result of a determinate computing process. Monads etc. just allow us to use IO expressions as if they were computable even though they're not, by enforcing sequencing. Or to put it another way, what really counts is predictability, not referential transparency. -gregg