Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
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 point out a subtlety in the code, admitting that they fell into the trap themselves. They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.) If the final result depends on the order of evaluation, then the context in which the result is defined is not referentially transparent. If a context is referentially opaque, then equational reasoning can fail -- i.e., it is no longer a valid technique of analysis, since the axioms on which it depends are no longer satisfied: It is necessary that four and four is eight The number of planets is eight does not imply It is necessary that the number of planets is eight, as equational reasoning (or, better put, substitution of equals, the first order axiom for equality witnessing Leibniz equality) requires. In particular, quotation marks, necessity, and unsafeInterleaveST are referentially opaque contexts. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
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: http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf slides: http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf there we proposed an extension to Concurrent Haskell which adds a primitive future :: IO a - IO a Roughly speaking future is like unsafeInterleaveIO, but creates a new concurrent thread to compute the result of the IO-action interleaved without any fixed order. That's very interesting to hear. It has always been my intuition that the right way to understand unsafeInterleaveIO is using a concurrency semantics (with a demonic scheduler). And whenever this unsafeInterleaveIO is unsound issue comes up, that's the argument I make to whoever will listen! ;-) That intuition goes some way to explain why unsafeInterleaveIO is fine but unsafeInterleaveST is right out: ST is supposed to be deterministic, but IO can be non-deterministic. We have shown that adding this primitive to the functional core language is 'safe' in the sense that all program equations of the pure language still hold in the extended language (which we call a conservative extension in the above paper) The used equality is contextual equivalence (with may- and a variant of must-convergence in the concurrent case). Ok. We also showed that adding unsafeInterleaveIO (called lazy futures in the paper..) - which delays until its result is demanded - breaks this conservativity, since the order of evaluation can be observed. My conjecture is that with a concurrent semantics with a demonic scheduler then unsafeInterleaveIO is still fine, essentially because the semantics would not distinguish it from your 'future' primitive. That said, it might not be such a useful semantics because we often want the lazy behaviour of a lazy future. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
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: http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf slides: http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf there we proposed an extension to Concurrent Haskell which adds a primitive future :: IO a - IO a Roughly speaking future is like unsafeInterleaveIO, but creates a new concurrent thread to compute the result of the IO-action interleaved without any fixed order. That's very interesting to hear. It has always been my intuition that the right way to understand unsafeInterleaveIO is using a concurrency semantics (with a demonic scheduler). And whenever this unsafeInterleaveIO is unsound issue comes up, that's the argument I make to whoever will listen! ;-) That intuition goes some way to explain why unsafeInterleaveIO is fine but unsafeInterleaveST is right out: ST is supposed to be deterministic, but IO can be non-deterministic. I agree. We have shown that adding this primitive to the functional core language is 'safe' in the sense that all program equations of the pure language still hold in the extended language (which we call a conservative extension in the above paper) The used equality is contextual equivalence (with may- and a variant of must-convergence in the concurrent case). Ok. We also showed that adding unsafeInterleaveIO (called lazy futures in the paper..) - which delays until its result is demanded - breaks this conservativity, since the order of evaluation can be observed. My conjecture is that with a concurrent semantics with a demonic scheduler then unsafeInterleaveIO is still fine, essentially because the semantics would not distinguish it from your 'future' primitive. Yes our result should hold for any scheduling. That said, it might not be such a useful semantics because we often want the lazy behaviour of a lazy future. Yes I agree with that, too. Best wishes, David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
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. I guess this is a terminological problem. It likely is. The phrase `context distinguishes e1 and e2' is the standard phrase in theory of contextual equivalence. Here are the nice slides http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf The only occurrence of 'distinguish' is in the Leibniz citation. Please see adequacy on slide 17. An expression relation between two boolean expressions M1 and M2 is adequate if for all program runs (for all initial states of the program s), M1 evaluates to true just in case M2 does. If in some circumstances M1 evaluates to true but M2 (with the same initial state) evaluates to false, the expressions are not related or the expression relation is inadequate. In my mind, 'evaluates-to' is an existential statement. The adequacy notion given there is inadequate if the program execution is indeterministic, as I would have expected it to be in this case. (They quickly note this on slide 18, giving concurrency features as an example.) See also the classic http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz (p11 for definition and Theorem 3.8 for an example of a distinguishing, or witnessing context). Thanks for the pointer, I will have a look. However, it seems that the semantics the definition and the proof rely on are deterministic? In essence, lazy IO provides unsafe constructs that are not named accordingly. (But IO is problematic in any case, partly because it depends on an ideal program being run on a real machine which is based on a less general model of computation.) I'd agree with the first sentence. As for the second sentence, all real programs are real programs executing on real machines. We may equationally prove (at time Integer) that 1 + 2^10 == 2^10 + 1 but we may have trouble verifying it in Haskell (or any other language). That does not mean equational reasoning is useless: we just have to precisely specify the abstraction boundaries. Which is really hard. I think equational reasoning is helpful because it is valid for ideal programs and it seems therefore to be a good heuristic for real ones. BTW, the equality above is still useful even in Haskell: it says that if the program managed to compute 1 + 2^10 and it also managed to compute 2^10 + 1, the results must be the same. (Of course in the above example, the program will probably crash in both cases). What is not adequate is when equational theory predicts one finite result, and the program gives another finite result -- even if the conditions of abstractions are satisfied (e.g., there is no IO, the expression in question has a pure type, etc). The abstraction bound is where exact reasoning necessarily stops. I think this context cannot be used to reliably distinguish x == y and y == x. Rather, the outcomes would be arbitrary/implementation defined/undefined in both cases. My example uses the ST monad for a reason: there is a formal semantics of ST (denotational in Launchbury and Peyton-Jones and operational in Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury and Peyton-Jones. The semantics is explained in Sec 6. InterleaveST is first referred to in chapter 10. As far as I can tell, the construct does not have specified a formal semantics. 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 point out a subtlety in the code, admitting that they fell into the trap themselves. They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.) So, unsafeInterleaveST is really bad -- and the people who introduced it know that, all too well. I certainly do not disagree that it is bad. However, I am still not convinced that the example actually shows a violation of equational reasoning. The valid outputs, according to the informal specification in chapter 10, are the same for both expressions. 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: http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf slides: http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf there we proposed an extension to Concurrent Haskell which adds a primitive future :: IO a - IO a Roughly speaking future is like unsafeInterleaveIO, but creates a new concurrent thread to
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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 quite complex, with a steep learning curve. As to alternatives -- this is may be the issue of familiarity or the availability of a nice library of combinators. Here is the example from my FLOPS talk: count the number of words the in a file. Lazy IO: run_countTHEL fname = readFile fname = print . length . filter (==the) . words Iteratee IO: run_countTHEI fname = print = fileL fname $ wordsL $ filterL (==the) $ count_i The same structure of computation and the same size (and the same incrementality). But there is even a simple way (when it applies): generators. All languages that tried generators so far (starying from CLU and Icon) have used them to great success. Derek Lowe has a list of Things I Won't Work With. http://pipeline.corante.com/archives/things_i_wont_work_with/ This is a really fun site indeed. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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 required in a working set. Any Haskell programmer, regardless of whether they use lazy I/O, will already know the meanings of (.), length, and filter. On the other hand, ($), count_i, and filterL are new names that must be learned from yet another library -- and much harder than learned, also kept in a mental working set of fluency. This ends up being a rather strong argument for lazy I/O. Not that the code is shorter, but that it (surprisingly) unifies ideas that would otherwise have required separate vocabulary. I'm not saying it's a sufficient argument, just that it's a much stronger one than familiarity, and that it's untrue that some better library might achieve the same thing without the negative consequences. (If you're curious, I do believe that it often is a sufficient argument in certain environments; I just don't think that's the kind of question that gets resolved in mailing list threads.) -- Chris Smith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe
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. It likely is. The phrase `context distinguishes e1 and e2' is the standard phrase in theory of contextual equivalence. Here are the nice slides http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf The only occurrence of 'distinguish' is in the Leibniz citation. Please see adequacy on slide 17. An expression relation between two boolean expressions M1 and M2 is adequate if for all program runs (for all initial states of the program s), M1 evaluates to true just in case M2 does. If in some circumstances M1 evaluates to true but M2 (with the same initial state) evaluates to false, the expressions are not related or the expression relation is inadequate. In my mind, 'evaluates-to' is an existential statement. The adequacy notion given there is inadequate if the program execution is indeterministic, as I would have expected it to be in this case. (They quickly note this on slide 18, giving concurrency features as an example.) See also the classic http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz (p11 for definition and Theorem 3.8 for an example of a distinguishing, or witnessing context). Thanks for the pointer, I will have a look. However, it seems that the semantics the definition and the proof rely on are deterministic? In essence, lazy IO provides unsafe constructs that are not named accordingly. (But IO is problematic in any case, partly because it depends on an ideal program being run on a real machine which is based on a less general model of computation.) I'd agree with the first sentence. As for the second sentence, all real programs are real programs executing on real machines. We may equationally prove (at time Integer) that 1 + 2^10 == 2^10 + 1 but we may have trouble verifying it in Haskell (or any other language). That does not mean equational reasoning is useless: we just have to precisely specify the abstraction boundaries. Which is really hard. I think equational reasoning is helpful because it is valid for ideal programs and it seems therefore to be a good heuristic for real ones. BTW, the equality above is still useful even in Haskell: it says that if the program managed to compute 1 + 2^10 and it also managed to compute 2^10 + 1, the results must be the same. (Of course in the above example, the program will probably crash in both cases). What is not adequate is when equational theory predicts one finite result, and the program gives another finite result -- even if the conditions of abstractions are satisfied (e.g., there is no IO, the expression in question has a pure type, etc). The abstraction bound is where exact reasoning necessarily stops. I think this context cannot be used to reliably distinguish x == y and y == x. Rather, the outcomes would be arbitrary/implementation defined/undefined in both cases. My example uses the ST monad for a reason: there is a formal semantics of ST (denotational in Launchbury and Peyton-Jones and operational in Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury and Peyton-Jones. The semantics is explained in Sec 6. InterleaveST is first referred to in chapter 10. As far as I can tell, the construct does not have specified a formal semantics. 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 point out a subtlety in the code, admitting that they fell into the trap themselves. They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.) So, unsafeInterleaveST is really bad -- and the people who introduced it know that, all too well. I certainly do not disagree that it is bad. However, I am still not convinced that the example actually shows a violation of equational reasoning. The valid outputs, according to the informal specification in chapter 10, are the same for both expressions. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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 bad_ctx :: ((Bool,Bool) - Bool) - Bool bad_ctx body = body $ runST (do r - newSTRef False x - unsafeInterleaveST (writeSTRef r True return True) y - readSTRef r return (x,y)) t1 = bad_ctx $ \(x,y) - x == y -- True t2 = bad_ctx $ \(x,y) - y == x -- False [...] I don't understand what it does or *how* it breaks this code. Does it involve side effects being reordered in some weird way? As I understand it, unsafeInterleaveST defers the computation of x, so * if x is forced before y, then writeSTRef r True is run before readSTRef r, thus the latter yields True * if y is forced before x, then writeSTRef r True is run after readSTRef r, thus the latter yields False Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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 False 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. The function unsafeInterleaveST ought to bear the same stigma as does unsafePerformIO. After all, both masquerade side-effecting computations as pure. Potentially side-effecting computations. There are non-side-effecting uses of unsafePerformIO and unsafeInterleaveST, but verifying this is outside the reach of the type checker. If they have observable side-effects, I'd say the type system has been broken and it does not make sense to have a defined language semantics for those cases. Hopefully even lazy IO will get recommended less, and with more caveats. (Lazy IO may be superficially convenient -- so are the absence of typing discipline and the presence of unrestricted mutation, as many people in Python/Ruby/Scheme etc worlds would like to argue.) In essence, lazy IO provides unsafe constructs that are not named accordingly. (But IO is problematic in any case, partly because it depends on an ideal program being run on a real machine which is based on a less general model of computation.) The complete code: module R where 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 - newSTRef False x - unsafeInterleaveST (writeSTRef r True return True) y - readSTRef r return (x,y)) t1 = bad_ctx $ \(x,y) - x == y t2 = bad_ctx $ \(x,y) - y == x I think this context cannot be used to reliably distinguish x == y and y == x. Rather, the outcomes would be arbitrary/implementation defined/undefined in both cases. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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 - newSTRef False x - unsafeInterleaveST (writeSTRef r True return True) y - readSTRef r return (x,y)) t1 = bad_ctx $ \(x,y) - x == y -- True t2 = bad_ctx $ \(x,y) - y == x -- False If I remember correctly, one of the Griswold systems on the path between SNOBOL and Icon had a special feature for looking below the language level, called The Window into Hell. Derek Lowe has a list of Things I Won't Work With. http://pipeline.corante.com/archives/things_i_wont_work_with/ unsafeInterleaveST has just joined my Things I Won't Work With list. But since it is new to me, I don't understand what it does or *how* it breaks this code. Does it involve side effects being reordered in some weird way? I think there is a big difference between this and lazy I/O. unsafeInterleaveST *sounds* dangerous. 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unsafeInterleaveST (and IO) is really unsafe [was: meaning of referential transparency]
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. http://hackage.haskell.org/packages/archive/pipes/3.2.0/doc/html/Control-Proxy-Tutorial.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
