Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-19 Thread Alexander Solla
On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr timon.g...@gmx.ch wrote: Please see Sec 10.2 Unique supply trees -- you might see some familiar code. Although my example was derived independently, it has the same kernel of badness as the example in Launchbury and Peyton-Jones. The authors

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-18 Thread Duncan Coutts
On Mon, 2013-04-15 at 20:44 +0200, David Sabel wrote: A very interesting discussion, I may add my 2 cents: making unsafeInterleaveIO nondeterministic indeed seems to make it safe, more or less this was proved in our paper:

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-18 Thread David Sabel
Am 18.04.2013 15:17, schrieb Duncan Coutts: On Mon, 2013-04-15 at 20:44 +0200, David Sabel wrote: A very interesting discussion, I may add my 2 cents: making unsafeInterleaveIO nondeterministic indeed seems to make it safe, more or less this was proved in our paper:

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-15 Thread David Sabel
Am 13.04.2013 00:37, schrieb Timon Gehr: On 04/12/2013 10:24 AM, o...@okmij.org wrote: Timon Gehr wrote: I am not sure that the two statements are equivalent. Above you say that the context distinguishes x == y from y == x and below you say that it distinguishes them in one possible run.

[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-12 Thread oleg
Timon Gehr wrote: I am not sure that the two statements are equivalent. Above you say that the context distinguishes x == y from y == x and below you say that it distinguishes them in one possible run. I guess this is a terminological problem. The phrase `context distinguishes e1 and e2' is

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-12 Thread oleg
Lazy I/O *sounds* safe. And most of the alternatives (like conduits) hurt my head, so it is really *really* tempting to stay with lazy I/O and think I'm doing something safe. Well, conduit was created for the sake of a web framework. I think all web frameworks, in whatever language, are

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-12 Thread Chris Smith
On Fri, Apr 12, 2013 at 1:44 AM, o...@okmij.org wrote: As to alternatives -- this is may be the issue of familiarity or the availability of a nice library of combinators. It is certainly not just a matter of familiarity, nor availability. Rather, it's a matter of the number of names that are

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe

2013-04-12 Thread Timon Gehr
On 04/12/2013 10:24 AM, o...@okmij.org wrote: Timon Gehr wrote: I am not sure that the two statements are equivalent. Above you say that the context distinguishes x == y from y == x and below you say that it distinguishes them in one possible run. I guess this is a terminological problem.

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-11 Thread Tom Ellis
On Thu, Apr 11, 2013 at 12:49:40PM +1200, Richard A. O'Keefe wrote: On 10/04/2013, at 2:45 PM, o...@okmij.org wrote: ... unsafeInterleaveST is really unsafe ... import Control.Monad.ST.Lazy (runST) import Control.Monad.ST.Lazy.Unsafe (unsafeInterleaveST) import Data.STRef.Lazy

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-11 Thread Timon Gehr
On 04/10/2013 04:45 AM, o...@okmij.org wrote: ... And yet there exists a context that distinguishes x == y from y ==x. That is, there exists bad_ctx :: ((Bool,Bool) - Bool) - Bool such that *R bad_ctx $ \(x,y) - x == y True *R bad_ctx $ \(x,y) - y == x

[Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-10 Thread oleg
One may read this message as proving True === False without resorting to IO. In other words, referential transparency, or the substitution of equals for equals, may fail even in expressions of type Bool. This message is intended as an indirect stab at lazy IO. Unfortunately, Lazy IO and even

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-10 Thread Richard A. O'Keefe
On 10/04/2013, at 2:45 PM, o...@okmij.org wrote: ... unsafeInterleaveST is really unsafe ... import Control.Monad.ST.Lazy (runST) import Control.Monad.ST.Lazy.Unsafe (unsafeInterleaveST) import Data.STRef.Lazy bad_ctx :: ((Bool,Bool) - Bool) - Bool bad_ctx body = body $ runST (do r -

Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]

2013-04-10 Thread kudah
On Thu, 11 Apr 2013 12:49:40 +1200 Richard A. O'Keefe o...@cs.otago.ac.nz wrote: And most of the alternatives (like conduits) hurt my head I've understood conduits when I've read the awesome pipes tutorial.