Re: philosophy of Haskell

older
FW: [TYPES/announce] CUFP 2010...

Patai Gergely

15 Aug 2010 15 Aug '10

6:31 a.m.

I don't agree. A concurrent change is the effect of an IO action, not of the thread. For example if a concurrent thread writes to an MVar, then that change becomes the effect of the next takeMVar, which gets executed. If a concurrent thread changes a file on disk, then that changing becomes the effect of the next readFile, which reads the changed file. But that's exactly what the model cannot handle. Look at the following snippet again:

...

let (x, world1) = getLine world0 world2 = print (x+1) world1

This clearly says that the world returned by getLine and the world consumed by print is the same one, since the state monad model is pure, therefore world1 is immutable. However, this is not true, since someone else could have modified it in the meantime. The state monad can only describe a single thread, but that's a non-existent situation in the case of I/O, since the world keeps changing outside the program even if the program itself is single-threaded. Gergely -- http://www.fastmail.fm - IMAP accessible web-mail

Show replies by date

Ertugrul Soeylemez

15 Aug 15 Aug

11:30 a.m.

New subject: philosophy of Haskell

"Patai Gergely" wrote:

...

...
I don't agree. A concurrent change is the effect of an IO action, not of the thread. For example if a concurrent thread writes to an MVar, then that change becomes the effect of the next takeMVar, which gets executed. If a concurrent thread changes a file on disk, then that changing becomes the effect of the next readFile, which reads the changed file.

But that's exactly what the model cannot handle. Look at the following snippet again:

...
let (x, world1) = getLine world0 world2 = print (x+1) world1

This clearly says that the world returned by getLine and the world consumed by print is the same one, since the state monad model is pure, therefore world1 is immutable. However, this is not true, since someone else could have modified it in the meantime. The state monad can only describe a single thread, but that's a non-existent situation in the case of I/O, since the world keeps changing outside the program even if the program itself is single-threaded.

No. As you say the world1 value is immutable, but that's not contradictory. If between 'getLine' and 'print' something was done by a concurrent thread, then that change to the world is captured by 'print'. See for example the following code: var <- newEmptyMVar forkIO $ threadDelay 1000000 >> putMVar var 15 takeMVar var >>= print Let's translate it: \world0 -> let (var, world1) = newEmptyMVar world0 world2 = (forkIO $ threadDelay 1000000 >> putMVar var 15) world1 (result, world3) = takeMVar var world2 in print result world3 The subthread has the following code: \world0 -> let world1 = threadDelay 1000000 world0 in putMVar var 15 world1 In the main thread the delay of one second and the change to the MVar is /not/ an effect of another thread. There is no notion of threads at all. It's a side effect of takeMVar. The thread launched by forkIO becomes part of the opaque world variable, which captures everything. Otherwise we would have to say that the state monad model doesn't capture user input either, because conceptually there is no difference between a user typing something and a concurrent thread writing to stdin. IO has no specific notion for threads. Threads are just side effects. Things caused by threads is captured by normal IO actions like getLine and takeMVar. That's not a flaw of the interpretation as a state monad. That's a flaw of the IO monad itself. Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

Tillmann Rendel

11:40 a.m.

New subject: philosophy of Haskell

Ertugrul Soeylemez wrote:

...

...
...
let (x, world1) = getLine world0 world2 = print (x+1) world1

If between 'getLine' and 'print' something was done by a concurrent thread, then that change to the world is captured by 'print'.

But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread. If print is not restricted to be a pure Haskell function, we don't need the world passing in the first place. Tillmann

Bulat Ziganshin

12:15 p.m.

New subject: Re[2]: Re: philosophy of Haskell

Hello Tillmann, Sunday, August 15, 2010, 7:40:54 PM, you wrote:

...

But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

the whole World includes any concurrent thread though ;) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

Tillmann Rendel

12:38 p.m.

New subject: philosophy of Haskell

Bulat Ziganshin wrote:

...

...
But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

the whole World includes any concurrent thread though ;)

Oh I see. So given world1, print can simulate the behavior of the concurrent thread to take it into account when constructing world2. Since that simulation depends only on world1, print is still pure. Does that mean that world passing *does* account for concurrency after all? Tillmann

Ertugrul Soeylemez

3:25 p.m.

New subject: philosophy of Haskell

Tillmann Rendel wrote:

...

Bulat Ziganshin wrote:

...
...
But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

the whole World includes any concurrent thread though ;)

Oh I see. So given world1, print can simulate the behavior of the concurrent thread to take it into account when constructing world2. Since that simulation depends only on world1, print is still pure.

Does that mean that world passing *does* account for concurrency after all?

Exactly. If at any point you use forkIO, then the world is updated to include the new thread. That's why I find it wrong to say that this mental model doesn't capture concurrency. It just has no explicit notion for it, but neither has IO. Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

Bill Atkins

4:36 p.m.

New subject: philosophy of Haskell

On Sunday, August 15, 2010, Tillmann Rendel wrote:

...

Bulat Ziganshin wrote:

But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

the whole World includes any concurrent thread though ;)

Oh I see. So given world1, print can simulate the behavior of the concurrent thread to take it into account when constructing world2. Since that simulation depends only on world1, print is still pure.

Does that mean that world passing *does* account for concurrency after all?

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

I guess I don't see how forkIO, MVar's etc are more problematic than any other kind of I/O. Consider: line <- hGetLine myHandle putStrLn line The "world" could very easily change between these two statements - someone could delete the file we're reading from or change its contents or truncate it. In fact, the "RealWorld" will always be in flux and will never, ever be the same from one call to the next (even consider things like the wall clock, which will tick in between the time you generated world0 and the time you pass world0 to a new IO action). I don't think threads are the only problem with the "State RealWorld a" interpretation.

Brandon S Allbery KF8NH

12:49 p.m.

New subject: philosophy of Haskell

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 8/15/10 11:40 , Tillmann Rendel wrote:

...

But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

If print is not restricted to be a pure Haskell function, we don't need the world passing in the first place.

I am confused by this discussion. I originally thought some time back that IO was about "world passing", but in fact it's just handing off a baton to insure that a particular sequence of IO functions is executed in the specified sequence and not reordered. Nothing in the "baton" is intended to represent the actual "state of the world", nor is anything said about concurrent actions either in another thread of the current program or elsewhere outside the program; only ordering of calls in the *current* thread of execution. (Which, hmm, implies that unsafePerformIO and unsafeInterleaveIO are conceptually similar to forkIO.) - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxoGpUACgkQIn7hlCsL25U5SwCglJdUpOKbrFLmDO2X22nDq/no UTIAoMllTt9LXOlblVaocbtVnRIx4dMY =hCIW -----END PGP SIGNATURE-----

Tillmann Rendel

1:27 p.m.

New subject: philosophy of Haskell

Brandon S Allbery KF8NH wrote:

...

I am confused by this discussion. I originally thought some time back that IO was about "world passing", but in fact it's just handing off a baton to insure that a particular sequence of IO functions is executed in the specified sequence and not reordered. Nothing in the "baton" is intended to represent the actual "state of the world", nor is anything said about concurrent actions either in another thread of the current program or elsewhere outside the program; only ordering of calls in the *current* thread of execution.

That explains how the IO monad forces side-effecting functions into a specified sequence, but this discussion is about how to understand what these side-effecting functions do in a *pure* framework. So the idea is to regard, for example, putStr as a pure function from a world state to a different world state, assuming that the world state contains a String which represents the contents of the terminal. We could then implement and understand putStr in pure Haskell: data World = World { terminal :: String ... } type IO a = World -> (World, a) putStr :: String -> World -> (World, ()) putStr str world = (world {terminal = terminal world ++ str}, ()) The benefit of this point of view is that we can analyze the behavior of putStr. For example, by equational reasoning, we could derive the following equation: putStr s1 >> putStr s2 == putStr (s1 ++ s2) It seems that we can account for more features of IO by adding more fields to the World record. This discussion is about whether we can account for *all* of IO this way. Tillmann

Brandon S Allbery KF8NH

2:07 p.m.

New subject: philosophy of Haskell

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 8/15/10 13:27 , Tillmann Rendel wrote:

...

Brandon S Allbery KF8NH wrote:

...
I am confused by this discussion. I originally thought some time back that IO was about "world passing", but in fact it's just handing off a baton to insure that a particular sequence of IO functions is executed in the specified sequence and not reordered. Nothing in the "baton" is intended to represent the actual "state of the world", nor is anything said about concurrent actions either in another thread of the current program or elsewhere outside the program; only ordering of calls in the *current* thread of execution.

That explains how the IO monad forces side-effecting functions into a specified sequence, but this discussion is about how to understand what these side-effecting functions do in a *pure* framework. So the idea is to

I think that *is* included in what I said, by negation: it doesn't. Period. (As Conal observed.) Trying to take the Haskell representation of IO as the basis for a formal description of I/O actions is pretty much doomed from the start; adding records or etc. will at best mask the symptoms. - -- brandon s. allbery [linux,solaris,freebsd,perl] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.10 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxoLP8ACgkQIn7hlCsL25W4QACgtJ4bz/W5fHVV/DxNgt8R39C8 ZkEAnj7rUnoUh4UQDFRdLeHKVmP8HLKS =jnty -----END PGP SIGNATURE-----

Ertugrul Soeylemez

3:30 p.m.

New subject: philosophy of Haskell

Brandon S Allbery KF8NH wrote:

...

On 8/15/10 11:40 , Tillmann Rendel wrote:

...
But in a world passing interpretation of IO, print is supposed to be a pure Haskell function. So the value world2 can only depend on the values of print and world1, but not on the actions of some concurrent thread.

If print is not restricted to be a pure Haskell function, we don't need the world passing in the first place.

I am confused by this discussion. I originally thought some time back that IO was about "world passing", but in fact it's just handing off a baton to insure that a particular sequence of IO functions is executed in the specified sequence and not reordered. Nothing in the "baton" is intended to represent the actual "state of the world", nor is anything said about concurrent actions either in another thread of the current program or elsewhere outside the program; only ordering of calls in the *current* thread of execution. (Which, hmm, implies that unsafePerformIO and unsafeInterleaveIO are conceptually similar to forkIO.)

IO is just a simple language to express impure operations. What we discuss is how to /interpret/ IO, or more specifically how to translate IO computations into pure ones mentally. Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/

wren ng thornton

8:32 p.m.

New subject: philosophy of Haskell

Brandon S Allbery KF8NH wrote:

...

only ordering of calls in the *current* thread of execution. (Which, hmm, implies that unsafePerformIO and unsafeInterleaveIO are conceptually similar to forkIO.)

Implementationally they are very similar (at least as far as the baton is concerned). How hard we should press that for getting semantics out of them ...well, that's a different question :) -- Live well, ~wren

Brandon S Allbery KF8NH

8:57 p.m.

New subject: philosophy of Haskell

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 08/15/2010 08:32 PM, wren ng thornton wrote:

...

Brandon S Allbery KF8NH wrote:

...
only ordering of calls in the *current* thread of execution. (Which, hmm, implies that unsafePerformIO and unsafeInterleaveIO are conceptually similar to forkIO.)

Implementationally they are very similar (at least as far as the baton is concerned). How hard we should press that for getting semantics out of them ...well, that's a different question :)

I would say the discussion to this point is at worst neutral and at best mildly supports doing so. -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkxojO0ACgkQIn7hlCsL25XHmwCglxNzX6CvccQs42lXXrNmWA37 LG0An3+vlcvhdcXd5XmNnuO0Vw/Uu2A1 =on2m -----END PGP SIGNATURE-----

Paolo G. Giarrusso

27 Aug 27 Aug

6:08 a.m.

New subject: philosophy of Haskell

Hi all, how comes that it is considered safe to use Control.Monad.Primitive.primitive and .internal [1]? Why aren't they called, i.e.., unsafePrimitive and unsafeInternal? primitive allows accessing the RealWorld state and, say, passing it to two different IO actions unwrapped through internal? You get unsafeInterleaveIO through 'safe' primitives. Also, one could probably produce Haskell code showing all the inconsistencies we discussed through these primitives, couldn't one? [1] http://hackage.haskell.org/packages/archive/primitive/0.3/doc/html/Control-M... After reading the subsequent discussion, I wanted to point out a couple of further things - see below. 1) There is reason to this confusion: not only that state-passing is used as the actual (inaccessible) implementation of IO, but also that (it seems) the mistake used to be made by Haskell inventors - in "Lazy Functional State Threads", at least (which is still cited as documentation for Control.Monad.ST). "Tackling the Awkward Squad" instead introduces this idea to later explain it does not work. 2) I cannot reconcile the result of the discussion with referential transparency. Is everybody wrong in claiming that Haskell is completely referentially transparent? "Lazy Functional State Threads" explicitly explains referential transparency in terms of state passing. I am now reading "Tackling the Awkward Squad", and from section 2.8 it is already clear enough that IO is not referentially transparent (although they never mention referential transparency in that paper). In their example, after "let (c, world1) = getChar world0", replacing c by "fst getChar world0" is not valid, and this violates referential transparency. See below for a more interesting example with concurrency. On Aug 15, 5:30 pm, Ertugrul Soeylemez wrote:

...

"Patai Gergely" wrote:

...
...
I don't agree. A concurrent change is the effect of an IO action, not of the thread. For example if a concurrent thread writes to an MVar, then that change becomes the effect of the next takeMVar, which gets executed. If a concurrent thread changes a file on disk, then that changing becomes the effect of the next readFile, which reads the changed file.

...

No. As you say the world1 value is immutable, but that's not contradictory. If between 'getLine' and 'print' something was done by a concurrent thread, then that change to the world is captured by 'print'.

Introducing a data race in your example creates another kind of problem. In your example, takeMVar is a synchronization primitive, and that ensures that print always gives the same result:

...

var <- newEmptyMVar forkIO $ threadDelay 1000000 >> putMVar var 15 takeMVar var >>= print

Let us make the example more interesting by introducing a data race on a IORef: ghci> var <- newIORef 10 ghci> (forkIO $ writeIORef var 20) >> readIORef var >>= print 10 ghci> readIORef var >>= print 20 Because of the data race, applying your reasoning, we get that either readIORef or print has changed the value referred to by var. Which is even more counterintuitive at best. I can remove the print from the middle by saving the result of readIORef, apply the concept that readIORef does not change the state to the first read, and obtain that the second readIORef gives a different result on the same input and is thus an impure function.

...

nightmare = unsafePerformIO (getWrongWife >>= sex) LOL

Greetings, Paolo -- Paolo Giarrusso - Ph.D. Student http://www.informatik.uni-marburg.de/~pgiarrusso/

5380

Age (days ago)

5392

Last active (days ago)

List overview

Download

13 comments

8 participants

participants (8)

Bill Atkins
Brandon S Allbery KF8NH
Bulat Ziganshin
Ertugrul Soeylemez
Paolo G. Giarrusso
Patai Gergely
Tillmann Rendel
wren ng thornton