Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Jonathan Cast jonathancc...@fastmail.fm writes: Couldn't you just substitute catch exceptions with unsafePerformIO here, and make the same argument? This puzzled me, until I realized you meant `unsafeInterleaveIO'. Aargh, yes of course! Sorry about that. Assuming you mean unsafeInterleaveIO, not quite. GHC's scheduler is fair, so you are guaranteed after forkIO $ a that a's side effects will happen eventually. Ah, I hadn't thought of that. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
What does this mean again? I'm working on the assumption that `context-sensitive' means `under some (not necessarily compositional and/or continuous and/or monotonic) equivalence relation/ I'm using contexts as expressions with holes, as used for evaluation contexts in operational semantics, where both contexts and expressions tend to be specified by grammars (in that form usually attributed to Felleisen, I think, though structural operational semantics often just group their rules into local reduction and congruence/embedding of reduction in subprograms) and rewrite rules and term relations can abstract over both expressions and contexts. For instance, if we have lambda calculus expressions E := v | \v.E | E E we can write arbitrary one-hole contexts as (where [ ] denotes the hole to be filled, and hole-filling is naive, not capture-avoiding) C[ ] := [ ] | \v.C[ ] | C[ ] E | E C[ ] and since we'd expect (using E1[E2/v] for capture-avoiding substitution of E2 for v in E1) beta-equivalence to hold in all contexts forall C v E1 E2. C[ (\v.E1) E2 ] =beta= C[ E1[E2/v] ] we usually abbreviate that as forall v E1 E2. (\v.E1) E2 =beta= E1[E2/v] So context-free rules are the subset of context-sensitive rules that neither limits, nor uses, nor changes the contexts in which the rule is applicable. A perfect match for purely functional evaluation. When we add IO, however, we add the ability for an expression to interact with the context it is running in, and that calls for the full range of context-sensitive rules. For instance, using monadic program contexts M[ ] := [ ] | M[ ] = E and some representation of context state, we can model monadic IO similar to communication in process calculi, with the functional program and its runtime context as parallel processes M[ getIO ] || Context[ char ] -getIO- M[ return char ] || Context[ char ] and so on (see the Awkward Squad [0], Concurrent Haskell [1] and imprecise Exception papers [2] for Haskell-related examples; [0,1] use evaluation contexts, [2] uses separate structural and reduction rules). The IO monad is still a part of Haskell's denotational semantics, right? I believe you could make it so. But I suspect that a denotational semantics that covers both IO and functional evaluation would be more cumbersome to use than a hybrid semantics that treats functional evaluation denotationally and IO execution operationally. Which is why I'm with those who prefer the hybrid here. But then I'm definitely biased towards operational semantics in general, so others may offer different preferences on the same topic!-) Which reminds me of a useful encounter I once had with a non-functional, but thoughtful programming language person: I was going on about the greatness of purely functional programming and being able to replace equals with equals. He said something like this: of course you can replace equals with equals - if you can't replace them, they can't be equal, right?-) So, the real question is how useful the equality is, and the contexts in which you can do that replacing - after all, one can give denotational semantics for imperative languages as well. Otherwise, I don't think we can really claim Haskell, as a language that includes IO in its specification, is truly `purely functional'. It's a language that integrates two sub-languages, one purely functional and one side-effectful and imperative. Which is a nice accomplishment, but less that what Haskell originally aimed to achieve. [hobby-horse warning: see chapter 3 of [3], at least references in 3.6:-] Personally, I do indeed think that we should be talking about a pure, functional interactive language, not a purely functional one. There are two qualitatively different aspects of imperative functional programming languages, and trying to make one look like the other is obscuring the essential differences without being able to hide them completely. The early stream-based IO approaches were cumbersome, Clean's uniqueness-typed world passing approach is fairly clean, but at the cost of restricting functional code involved in IO (also, one still needs to interpret main :: *World - *World as generating a _sequence of observable intermediate states_, unlike a real function applied to a single world, but similar to what a non-hybrid denotational semantics would have to do). I find Haskell's approach both simple (functional programs compute values, these values can include dialogues with the runtime context, dialogue values that reach the boundary between program and runtime context get interpreted as interactions between the two) and practical (there are lots of things from Clean that would be nice to have in Haskell, including uniqueness-typed environment passing as a safe basis for IO, but I'd still use monadic IO as an interface to that basis). Where does it say that Haskell aimed for anything else, btw? I still don't understand what
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Tue, 2009-03-17 at 12:59 +0100, Ketil Malde wrote: Duncan Coutts duncan.cou...@worc.ox.ac.uk writes: [..] I have a sneaking suspicion [exceptions] actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. Couldn't you just substitute catch exceptions with unsafePerformIO here, and make the same argument? This puzzled me, until I realized you meant `unsafeInterleaveIO'. That's pretty much the argument that is made for unsafeInterleaveIO. Similarly, can't you emulate unsafePerformIO with concurrency? Assuming you mean unsafeInterleaveIO, not quite. GHC's scheduler is fair, so you are guaranteed after forkIO $ a that a's side effects will happen eventually. On the other hand, after unsafeInterleaveIO $ a you have basically no guarantee the RTS will ever get around to scheduling a. (In fact, if you write it just like that in a do block, rather than saying x - unsafeInterleaveIO $ a you are pretty much guaranteed that the RTS won't ever feel like scheduling a. It'll even garbage collect a without ever executing it.) Further, couldn't you, from IO, FFI into a function that examines the source code of some pure function, thus being able to differentiate funcitions that are normally indistinguishable? Regular IO is good enough for this. I've tried to follow this discussion, but I don't quite understand what's so bad about unsafeInterleaveIO - or rather, what's so uniquely bad about it. It seems the same issues can be found in every corner of IO. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Duncan Coutts duncan.cou...@worc.ox.ac.uk writes: [..] I have a sneaking suspicion [exceptions] actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. Couldn't you just substitute catch exceptions with unsafePerformIO here, and make the same argument? Similarly, can't you emulate unsafePerformIO with concurrency? Further, couldn't you, from IO, FFI into a function that examines the source code of some pure function, thus being able to differentiate funcitions that are normally indistinguishable? I've tried to follow this discussion, but I don't quite understand what's so bad about unsafeInterleaveIO - or rather, what's so uniquely bad about it. It seems the same issues can be found in every corner of IO. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
So that first step already relies on IO (where the two are equivalent). Come again? The first step in your implication chain was (without the return) throw (ErrorCall urk!) = 1 == evaluate (throw (ErrorCall urk!)) = evaluate 1 but, using evaluation only (no context-sensitive IO), we have throw (ErrorCall urk) = evaluate (throw (ErrorCall urk)) Sure enough. meaning that first step replaced a smaller with a bigger item on the smaller side of the inequation. Unless the reasoning includes context- sensitive IO rules, in which case the IO rule for evaluate brings the throw to the top (evaluate (throw ..) - (throw ..)), making the two terms equivalent (modulo IO), and hence the step valid (modulo IO). Unless you just rely on But throwIO (ErrorCall urk) /= _|_: Control.Exception throwIO (ErrorCall urk!) `seq` () () in which case that step relies on not invoking IO, so it can't be mixed with the later step involving IO for catch (I think). This is very delicate territory. For instance, one might think that this 'f' seems to define a negation function of information content f x = Control.Exception.catch (evaluate x let x = x in x) (\(ErrorCall _)-return 0) = print and hence violates monotonicity (_|_ = ()) = (f _|_ = f ()) since *Main f undefined 0 *Main f () Interrupted. But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules. Could you elaborate on this? It sounds suspiciously like you're saying Haskell's axiomatic semantics is unsound :: IO. Not really unsound, if the separation is observed. One could probably construct a non-separated semantics (everything denotational), but at the cost of mapping everything to computations rather than values. Then computations like that 'f' above would, eg, take an extra context argument (representing the world, or at least aspects of the machine running the computation), and the missing information needed to take 'f _|_'[world] to '()'[world'] would come from that context parameter (somewhere in the computational context, there is a representation of the computation, which allows the context to read certain kinds of '_|_' as exceptions; the IO rule for 'catch' takes that external information and injects it back from the computational context into the functional program, as data structure representations of exceptions). That price is too high, though, as we'd now have to do all reasoning in context-sensitive terms which, while more accurate, would bury us in irrelevant details. Hence we usually try to use context-free reasoning whenever we can get away with it (the non-IO portions of Haskell program runs), resorting to context-sensitive reasoning only when necessary (the IO steps of Haskell program runs). This gives us convenience when the context is irrelevant as well as accuracy when the context does matter - we just have to be careful when combining the two kinds of reasoning. For instance, without execution *Main f () `seq` () () *Main f undefined `seq` () () but if we include execution (and the context-sensitive equivalence that implies, lets call it ~), So a ~ b = `The observable effects of $(x) and $(y) are equal' ? Observational equivalence is one possibility, there are various forms of equivalences/bi-similarities, with different ratios of convenience and discriminatory powers (the folks studying concurrent languages and process calculi have been fighting with this kind of situation for a long time, and have built up a wealth of experience in terms of reasoning). The main distinction I wanted to make here was that '=' was a context-free equivalence (valid in all contexts, involving only context-free evaluation rules) while '~' was a context-sensitive equivalence (valid only in IO contexts, involving both context-free and context-sensitive rules). we have f () ~ _|_ = return 0 ~ f _|_ so 'f' shows that wrapping both sides of an inequality in 'catch' need not preserve the ordering (modulo ~) If f _|_ = f (), then it seems that (=) is not a (pre-) order w.r.t. (~). So taking the quotient of IO Int over (~) gives you a set on which (=) is not an ordering (and may not be a relation). As I said, mixing '=' and '~', without accounting for the special nature of the latter, is dangerous. If we want to mix the two, we have to shift all reasoning into the context-sensitive domain, so we'd have something like f () [world] ~ _|_ [world''] = return 0 [world'] ~ f _|_ [world] (assuming that '=' is lifted to compare values in contexts). And now the issue goes away, because 'f' doesn't look at the '_|_', but at the representation of '_|_' in the 'world' (the representation of '_|_' in GHC's runtime system, say). - its whole purpose is to
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Tue, 2009-03-17 at 12:40 +, Claus Reinke wrote: So that first step already relies on IO (where the two are equivalent). Come again? The first step in your implication chain was (without the return) throw (ErrorCall urk!) = 1 == evaluate (throw (ErrorCall urk!)) = evaluate 1 but, using evaluation only (no context-sensitive IO), we have throw (ErrorCall urk) = evaluate (throw (ErrorCall urk)) Sure enough. meaning that first step replaced a smaller with a bigger item on the smaller side of the inequation. And the larger side! I'm trying to determine whether there can exist a denotational semantics for IO, which treats it as a functor from (D)CPOs to (D)CPOs, for which the corresponding denotational semantics for the IO operations satisfies the requirement that they are both monotone and continuous. So I assumed monotonicity of evaluate. Unless the reasoning includes context- sensitive IO rules, What does this mean again? I'm working on the assumption that `context-sensitive' means `under some (not necessarily compositional and/or continuous and/or monotonic) equivalence relation/ in which case the IO rule for evaluate brings the throw to the top (evaluate (throw ..) - (throw ..)), making the two terms equivalent (modulo IO), and hence the step valid (modulo IO). Unless you just rely on But throwIO (ErrorCall urk) /= _|_: Control.Exception throwIO (ErrorCall urk!) `seq` () () in which case that step relies on not invoking IO, so it can't be mixed with the later step involving IO for catch (I think). The IO monad is still a part of Haskell's denotational semantics, right? Otherwise, I don't think we can really claim Haskell, as a language that includes IO in its specification, is truly `purely functional'. It's a language that integrates two sub-languages, one purely functional and one side-effectful and imperative. Which is a nice accomplishment, but less that what Haskell originally aimed to achieve. This is very delicate territory. For instance, one might think that this 'f' seems to define a negation function of information content f x = Control.Exception.catch (evaluate x let x = x in x) (\(ErrorCall _)-return 0) = print and hence violates monotonicity (_|_ = ()) = (f _|_ = f ()) since *Main f undefined 0 *Main f () Interrupted. But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules. Could you elaborate on this? It sounds suspiciously like you're saying Haskell's axiomatic semantics is unsound :: IO. Not really unsound, if the separation is observed. I still don't understand what you're separating. Are you saying the semantics of terms of type IO need to be separated from the semantics of terms of non-IO type? One could probably construct a non-separated semantics (everything denotational), but at the cost of mapping everything to computations rather than values. So as long as Haskell is no longer pure (modulo lifting everything) it works? Then computations like that 'f' above would, eg, take an extra context argument (representing the world, or at least aspects of the machine running the computation), and the missing information needed to take 'f _|_'[world] to '()'[world'] would come from that context parameter (somewhere in the computational context, there is a representation of the computation, which allows the context to read certain kinds of '_|_' as exceptions; the IO rule for 'catch' takes that external information and injects it back from the computational context into the functional program, as data structure representations of exceptions). That price is too high, though, as we'd now have to do all reasoning in context-sensitive terms which, while more accurate, would bury us in irrelevant details. Hence we usually try to use context-free reasoning whenever we can get away with it (the non-IO portions of Haskell program runs), resorting to context-sensitive reasoning only when necessary (the IO steps of Haskell program runs). So I can't use normal Haskell semantics to reason about IO. That's *precisely* what I'm trying to problematize. This gives us convenience when the context is irrelevant as well as accuracy when the context does matter - we just have to be careful when combining the two kinds of reasoning. For instance, without execution *Main f () `seq` () () *Main f undefined `seq` () () but if we include execution (and the context-sensitive equivalence that implies, lets call it ~), So a ~ b = `The observable effects of $(x) and $(y) are equal' ? Observational equivalence is one possibility, there are various forms of
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Hi, On 2009/03/16, at 10:04, wren ng thornton wrote: next r = do n - readIORef r writeIORef r (n+1) return n Now, if I use unsafeInterleaveIO: main = do r - newIORef 0 x - do a - unsafeInterleaveIO (next r) b - unsafeInterleaveIO (next r) return (a,b) ... The values of a and b in x are entirely arbitrary, and are only set at the point when they are first accessed. They're not just arbitrary between which is 0 and which is 1, they could be *any* pair of values (other than equal) since the reference r is still in scope and other code in the ... could affect it before we access a and b, or between the two accesses. OK, the values of a and b depend how to deconstruct x. Moreover, let's have two pure implementations, f and g, of the same mathematical function. Even if f and g are close enough to correctly give the same output for inputs with _|_ in them, we may be able to observe the fact that they arrive at those answers differently by passing in our x. Given that such observations are possible, it is no longer safe to exchange f and g for one another, despite the fact that they are pure and give the same output for all (meaningful) inputs. Hm, Does it means that in optimization, a compiler may replace implementation of a pure function that have different order of evaluation, so order of actions would be different in some environments? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On 2009 Mar 16, at 8:48, Yusaku Hashimoto wrote: On 2009/03/16, at 10:04, wren ng thornton wrote: Moreover, let's have two pure implementations, f and g, of the same mathematical function. Even if f and g are close enough to correctly give the same output for inputs with _|_ in them, we may be able to observe the fact that they arrive at those answers differently by passing in our x. Given that such observations are possible, it is no longer safe to exchange f and g for one another, despite the fact that they are pure and give the same output for all (meaningful) inputs. Hm, Does it means that in optimization, a compiler may replace implementation of a pure function that have different order of evaluation, so order of actions would be different in some environments? order of actions is meaningless in pure functions, so yes. And that's why unsafeInterleaveIO is unsafe: your pure function can have side effects which are observable, so there is an order of actions to worry about. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Yusaku Hashimoto wrote: | I was studying about what unsafeInterleaveIO is.I understood | unsafeInterleaveIO takes an IO action, and delays it. But I couldn't | find any reason why unsafeInterleaveIO is unsafe. I think it depends on what we want to take unsafe to mean. In my opinion, the word unsafe should really only be used in cases where using the function can case an otherwise well-typed program to not be well-typed. I'm pretty sure I haven't yet seen a case where this applies to unsafeInterleaveIO. The biggest problem with unsafeInterleaveIO is that it complicates the semantics of the IO monad. - - Jake -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkm+aH8ACgkQye5hVyvIUKkOygCghyHD90TdvCBR5V815fxmQbIy mKsAnjnAgtZ5jV1p1P2St5NB2li587lU =PzqF -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, Mar 16, 2009 at 7:55 AM, Jake McArthur j...@pikewerks.com wrote: I think it depends on what we want to take unsafe to mean. In my opinion, the word unsafe should really only be used in cases where using the function can case an otherwise well-typed program to not be well-typed. I'm pretty sure I haven't yet seen a case where this applies to unsafeInterleaveIO. I don't think unsafeInterleaveIO on its own can do this. However, I disagree with your description of what unsafe should be used for. unsafe calls out the need for the programmer to prove that what they are doing is safe semantically, instead of the compiler providing those proofs for you. Whether that is due to type safety (unsafeCoerce) or breaking the assumptions of the compiler (unsafePerformIO, unsafeInterleaveIO, unsafeIOToST), depends on the situation. For example, unsafePerformIO can make your program not type-safe, but it's convoluted to do so; in fact, at monomorphic types it can't break type safety. That's not what makes it unsafe at all. It's unsafe because it breaks the rule that pure values don't have side effects, so that the effects inside the unsafePerformIO might get executed more than once, or not at all, depending on how the compiler decides to evaluate the pure value returned. And what happens could depend on the optimization settings of the compiler, the timing of the machine you are running on, or the phase of the moon. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Monday 16 March 2009 2:11:10 pm Ryan Ingram wrote: However, I disagree with your description of what unsafe should be used for. unsafe calls out the need for the programmer to prove that what they are doing is safe semantically, instead of the compiler providing those proofs for you. Whether that is due to type safety (unsafeCoerce) or breaking the assumptions of the compiler (unsafePerformIO, unsafeInterleaveIO, unsafeIOToST), depends on the situation. Of course, unsafeIOToST can also break the type system, because you can write: unsafePerformIO m = runST (unsafeIOToST m) For example, unsafePerformIO can make your program not type-safe, but it's convoluted to do so; in fact, at monomorphic types it can't break type safety. That's not what makes it unsafe at all. It's unsafe because it breaks the rule that pure values don't have side effects, so that the effects inside the unsafePerformIO might get executed more than once, or not at all, depending on how the compiler decides to evaluate the pure value returned. And what happens could depend on the optimization settings of the compiler, the timing of the machine you are running on, or the phase of the moon. In practice, 'unsafe' can mean any number of things depending on the context. unsafeRead/Write on mutable arrays can (attempt to) read/write arbitrary memory locations. An index into a data structure that just calls error instead of returning a Maybe result might be called unsafe. In a similar vein, some people think head and tail should be called unsafeHead and unsafeTail. :) Technically, one can probably lay down a semantics of IO such that unsafeInterleaveIO maintains the purity of the language by the usual definitions. However, such a semantics is necessarily too vague to explain why you might want to use it in the first place, because the only real reason you'd want to do so is to have side effects triggered in response to evaluation of otherwise pure terms. At the very least, using unsafeInterleaveIO adds significant complications to reasoning about the behavior of otherwise ordinary IO, which might well justify its name. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 15 Mar 2009, Ryan Ingram wrote: unsafeInterleaveIO allows embedding side effects into a pure computation. This means you can potentially observe if some pure value has been evaluated or not; the result of your code could change depending how lazy/strict it is, which is very hard to predict! For example: -- given f :: Integer - Integer main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 x - case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y -- a couple of examples: f x = 0 -- program prints 0 -- f x = x -- program prints 1 Interesting example. I have implemented the lazyio package. It asserts that unsafely interleaved IO actions are performed in order. This should prevent such problems, does it? However, they are only avoided within the LazyIO monad. Running the LazyIO monad in IO allows the same corruptions as shown above. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/lazyio ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 15 Mar 2009, Claus Reinke wrote: import Data.IORef import Control.Exception main = do r - newIORef 0 let v = undefined handle (\(ErrorCall _)-print hireturn 42) $ case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y I don't see what this has to do with strictness. It's just the hacky exception handling which allows to catch programming errors. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote: On Sun, 15 Mar 2009, Claus Reinke wrote: import Data.IORef import Control.Exception main = do r - newIORef 0 let v = undefined handle (\(ErrorCall _)-print hireturn 42) $ case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y I don't see what this has to do with strictness. It's just the hacky exception handling which allows to catch programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote: On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote: On Sun, 15 Mar 2009, Claus Reinke wrote: import Data.IORef import Control.Exception main = do r - newIORef 0 let v = undefined handle (\(ErrorCall _)-print hireturn 42) $ case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y I don't see what this has to do with strictness. It's just the hacky exception handling which allows to catch programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. See this paper: A semantics for imprecise exceptions http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, 2009-03-16 at 22:01 +, Duncan Coutts wrote: On Mon, 2009-03-16 at 14:17 -0700, Jonathan Cast wrote: On Mon, 2009-03-16 at 22:12 +0100, Henning Thielemann wrote: On Sun, 15 Mar 2009, Claus Reinke wrote: import Data.IORef import Control.Exception main = do r - newIORef 0 let v = undefined handle (\(ErrorCall _)-print hireturn 42) $ case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y I don't see what this has to do with strictness. It's just the hacky exception handling which allows to catch programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. See this paper: A semantics for imprecise exceptions http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. I'm not sure that helps much. Given the following inequalities (in the domain ordering) and equations: throw urk! = 1 evaluate . throw = throwIO evaluate x = return x -- x total catch (throwIO a) h = h a catch (return x) h = return x we expect to be able to reason as follows: throw urk! = return 1 == evaluate (throw urk!) = evaluate 1 == catch (evaluate (throw urk!)) (const $ return 2) = catch (evaluate 1) (const $ return 2) while catch (evaluate (throw urk!)) (const $ return 2) = catch (throwIO urk!) (const $ return 2) = const (return 2) urk! = return 2 and catch (evaluate 1) (const $ return 2) = catch (return 1) (const $ return 2) = return 1 So return 2 = return 1, in the domain ordering? That doesn't seem right. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
exception handling which allows to catch programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. A semantics for imprecise exceptions http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. I'm not sure that helps much. Given the following inequalities (in the domain ordering) and equations: throw urk! = return 1 == evaluate (throw urk!) = evaluate 1 throw (ErrorCall urk) = evaluate (throw (ErrorCall urk)) as demonstrated here *Main throw (ErrorCall urk) `seq` () *** Exception: urk *Main evaluate (throw (ErrorCall urk)) `seq` () () So that first step already relies on IO (where the two are equivalent). This is very delicate territory. For instance, one might think that this 'f' seems to define a negation function of information content f x = Control.Exception.catch (evaluate x let x = x in x) (\(ErrorCall _)-return 0) = print and hence violates monotonicity (_|_ = ()) = (f _|_ = f ()) since *Main f undefined 0 *Main f () Interrupted. But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules. For instance, without execution *Main f () `seq` () () *Main f undefined `seq` () () but if we include execution (and the context-sensitive equivalence that implies, lets call it ~), we have f () ~ _|_ = return 0 ~ f _|_ so 'f' shows that wrapping both sides of an inequality in 'catch' need not preserve the ordering (modulo ~) - its whole purpose is to recover from failure, making something more defined (modulo ~) by translating _|_ to something else. Which affects your second implication. If the odd properties of 'f' capture the essence of your concerns, I think the answer is to keep =, =, and ~ clearly separate, ideally without losing any of the context-free equivalences while limiting the amount of context-sensitive reasoning required. If = and ~ are mixed up, however, monotonicity seems lost. The semantics in the imprecise exceptions paper combines a denotational approach for the context-free part with an operational semantics for the context-sensitive part. This tends to use the good properties of both, with a clear separation between them, but a systematic treatment of the resulting identities was left for future work. Claus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Tue, 2009-03-17 at 01:16 +, Claus Reinke wrote: exception handling which allows to catch programming errors. And which I have a sneaking suspicion actually *is* `unsafe'. Or, at least, incapable of being given a compositional, continuous semantics. A semantics for imprecise exceptions http://research.microsoft.com/en-us/um/people/simonpj/papers/imprecise-exn.htm Basically if we can only catch exceptions in IO then it doesn't matter, it's just a little extra non-determinism and IO has plenty of that already. I'm not sure that helps much. Given the following inequalities (in the domain ordering) and equations: throw urk! = return 1 Oops, left a superfluous return in there. I meant throw urk! = 1 (The inequality is at Int). == evaluate (throw urk!) = evaluate 1 throw (ErrorCall urk) = evaluate (throw (ErrorCall urk)) Sure enough. But throwIO (ErrorCall urk) /= _|_: Control.Exception throwIO (ErrorCall urk!) `seq` () () So that first step already relies on IO (where the two are equivalent). Come again? This is very delicate territory. For instance, one might think that this 'f' seems to define a negation function of information content f x = Control.Exception.catch (evaluate x let x = x in x) (\(ErrorCall _)-return 0) = print and hence violates monotonicity (_|_ = ()) = (f _|_ = f ()) since *Main f undefined 0 *Main f () Interrupted. But that is really mixing context-free expression evaluation and context-sensitive execution of io operations. Most of our favourite context-free equivalences only hold within the expression evaluation part, while IO operations are subject to additional, context-sensitive rules. Could you elaborate on this? It sounds suspiciously like you're saying Haskell's axiomatic semantics is unsound :: IO. For instance, without execution *Main f () `seq` () () *Main f undefined `seq` () () but if we include execution (and the context-sensitive equivalence that implies, lets call it ~), So a ~ b = `The observable effects of $(x) and $(y) are equal' ? we have f () ~ _|_ = return 0 ~ f _|_ so 'f' shows that wrapping both sides of an inequality in 'catch' need not preserve the ordering (modulo ~) If f _|_ = f (), then it seems that (=) is not a (pre-) order w.r.t. (~). So taking the quotient of IO Int over (~) gives you a set on which (=) is not an ordering (and may not be a relation). - its whole purpose is to recover from failure, making something more defined (modulo ~) by translating _|_ to something else. Which affects your second implication. If the odd properties of 'f' capture the essence of your concerns, I think the answer is to keep =, =, and ~ clearly separate, ideally without losing any of the context-free equivalences while limiting the amount of context-sensitive reasoning required. If = and ~ are mixed up, however, monotonicity seems lost. So catch (throwIO e) h ~ h e but it is not the case that catch (throwIO e) h = h e ? That must be correct, actually: Control.Exception let x = Control.Exception.catch (throwIO (ErrorCall urk!)) (\ (ErrorCall _) - undefined) in x `seq` () () So catch is total (even if one or both arguments is erroneous), but the IO executor (a beast totally distinct from the Haskell interpreter, even if they happen to live in the same body) when executing it feels free to examine bits of the Haskell program's state it's not safe for a normal program to inspect. I'll have to think about what that means a bit more. The semantics in the imprecise exceptions paper combines a denotational approach for the context-free part with an operational semantics [Totally OT tangent: How did operational semantics come to get its noun? The more I think about it, the more it seems like a precís of the implementation, rather than a truly semantic part of a language specification.] for the context-sensitive part. This tends to use the good properties of both, with a clear separation between them, but a systematic treatment of the resulting identities was left for future work. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
unsafeInterleaveIO allows embedding side effects into a pure computation. This means you can potentially observe if some pure value has been evaluated or not; the result of your code could change depending how lazy/strict it is, which is very hard to predict! For example: -- given f :: Integer - Integer main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 x - case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y -- a couple of examples: f x = 0 -- program prints 0 -- f x = x -- program prints 1 f is pure. But if f is nonstrict, this program prints 0, and if it's strict, it prints 1. The strictness of a pure function can change the observable behavior of your program! Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. Also, the compiller might notice that x is never used, and that f is total. So it could just optimize out the evaluation of f v completely, at which point the program always prints 0 again; changing optimization settings modifies the result of the program. This is why unsafeInterleaveIO is unsafe. -- ryan On Sun, Mar 15, 2009 at 11:31 AM, Yusaku Hashimoto nonow...@gmail.com wrote: Hello, I was studying about what unsafeInterleaveIO is.I understood unsafeInterleaveIO takes an IO action, and delays it. But I couldn't find any reason why unsafeInterleaveIO is unsafe. I have already read an example in http://www.haskell.org/pipermail/haskell-cafe/2009-March/057101.html says lazy IO may break purity, but I think real matter in this example are wrong use of seq. did I misread? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote: unsafeInterleaveIO allows embedding side effects into a pure computation. This means you can potentially observe if some pure value has been evaluated or not; the result of your code could change depending how lazy/strict it is, which is very hard to predict! For example: -- given f :: Integer - Integer main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 x - case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y -- a couple of examples: f x = 0 -- program prints 0 -- f x = x -- program prints 1 f is pure. But if f is nonstrict, this program prints 0, and if it's strict, it prints 1. The strictness of a pure function can change the observable behavior of your program! Right. If the compiler feels like changing the way it implements your program based on that factor. But `semantics' that the compiler doesn't preserve are kind of useless... Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. I'm confused. I though if f was strict, then my program *always* printed 1? Also, the compiller might notice that x is never used, and that f is total. So it could just optimize out the evaluation of f v completely, at which point the program always prints 0 again; changing optimization settings modifies the result of the program. This is why unsafeInterleaveIO is unsafe. Well, unsafeInterleaveIO or reasoning based on overly specific assumptions about how things must be implemented, anyway. I'm not sure you've narrowed it down to usafeInterleaveIO, though. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast: On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote: Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. I'm confused. I though if f was strict, then my program *always* printed 1? But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast: On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote: Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. I'm confused. I though if f was strict, then my program *always* printed 1? But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. But if the compiler is free to do this itself, what guarantee do I have that it won't? jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Am Sonntag, 15. März 2009 21:56 schrieb Jonathan Cast: On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast: On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote: Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. I'm confused. I though if f was strict, then my program *always* printed 1? But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. But if the compiler is free to do this itself, what guarantee do I have that it won't? None? Wasn't that Ryan's point, that without the unsafeInterleaveIO, that reordering wouldn't matter, but with it, it does? jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 2009-03-15 at 22:09 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 21:56 schrieb Jonathan Cast: On Sun, 2009-03-15 at 21:43 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 21:25 schrieb Jonathan Cast: On Sun, 2009-03-15 at 13:02 -0700, Ryan Ingram wrote: Furthermore, due to the monad laws, if f is total, then reordering the (x - ...) and (y - ...) parts of the program should have no effect. But if you switch them, the program will *always* print 0. I'm confused. I though if f was strict, then my program *always* printed 1? But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. But if the compiler is free to do this itself, what guarantee do I have that it won't? None? Wasn't that Ryan's point, that without the unsafeInterleaveIO, that reordering wouldn't matter, but with it, it does? Sure. But *that point is wrong*. Given the two programs main0 = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y main1 = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 x - case f v of 0 - return 0 n - return (n - 1) y - readIORef r print y There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast: There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter. Hum. Whether the programme prints 0 or 1 depends on whether writeIORef r 1 is done before readIORef r. That depends of course on the semantics of IO and unsafeInterleaveIO. In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. (report, section 7) restricts the freedom considerably. However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. as explicitly allowing the programmer to say do it if and when the result is needed, not before. So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it. In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1, but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast: There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter. Hum. Whether the programme prints 0 or 1 depends on whether writeIORef r 1 is done before readIORef r. That depends of course on the semantics of IO and unsafeInterleaveIO. In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. (report, section 7) restricts the freedom considerably. Why not read that line as prohibiting concurrency (forkIO) as well? However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. Where is this taken from? If GHC's library docs try to imply that the programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted). as explicitly allowing the programmer to say do it if and when the result is needed, not before. Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much. So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it. In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1, Although as Ryan pointed out, the compiler may decide to omit the case statement entirely, if it can statically prove that f v is undefined. but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast: On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast: There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter. Hum. Whether the programme prints 0 or 1 depends on whether writeIORef r 1 is done before readIORef r. That depends of course on the semantics of IO and unsafeInterleaveIO. In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. (report, section 7) restricts the freedom considerably. Why not read that line as prohibiting concurrency (forkIO) as well? Good question. Because forkIO is a way to explicitly say one doesn't want the one thing necessarily done before the other, I'd say. However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. Where is this taken from? If GHC's library docs try to imply that the From the documentation of System.IO.Unsafe. programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted). Maybe. as explicitly allowing the programmer to say do it if and when the result is needed, not before. Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much. The full paragraph from the report: The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. I read it as saying that IO *does* allow the programmer to control when the effects are performed. So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it. In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1, Although as Ryan pointed out, the compiler may decide to omit the case statement entirely, if it can statically prove that f v is undefined. I suppose that's a typo and should be unneeded. But can it prove that f v is unneeded? After all, it may influence whether 0 or 1 is printed. but if f is lazy, v is not needed for that decision, so by the documentation, the unsafeInterleaveIOed action will not be performed, and the programme prints 0. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
main = do
r - newIORef 0
v - unsafeInterleaveIO $ do
writeIORef r 1
return 1
x - case f v of
0 - return 0
n - return (n - 1)
y - readIORef r
print y
-- a couple of examples:
f x = 0 -- program prints 0
-- f x = x -- program prints 1
f is pure. But if f is nonstrict, this program prints 0, and if
it's strict, it prints 1. The strictness of a pure function can
change the observable behavior of your program!
Strictness is an effect, even if it isn't recorded in Haskell's types.
Replacing 'v - ..' by 'let v = undefined' provides similar choices.
'unsafeInterleaveIO' explicitly uses the implicit effects of
strictness to drive the explicit effects of IO, which is why it
is unsafe (moving IO effects from explicit to implicit). But even
if 'unsafeInterleaveIO' where eliminated, strictness/evaluation
would still remain as an implicit effect in Haskell. Here's a
variation without 'unsafeInterleaveIO':
import Data.IORef
import Control.Exception
main = do
r - newIORef 0
let v = undefined
handle (\(ErrorCall _)-print hireturn 42) $ case f v of
0 - return 0
n - return (n - 1)
y - readIORef r
print y
-- a couple of examples:
f x = 0 -- program prints '0'
f x = x -- program prints 'hi0'
(sideline: I often interpret '_|_::t' not so much as an element of 't'
but as failure to produce information at type 't'; the type tells us
what information we can have, evaluation not only provides the
details, but also decides whether or not we have any of that info,
and how much of it)
Furthermore, due to the monad laws, if f is total, then reordering the
(x - ...) and (y - ...) parts of the program should have no effect.
case f v of { 0 - return 0; n - return (n - 1) }
=
return $! case f v of { 0 - 0; n - (n - 1) }
=/=
return $ case f v of { 0 - 0; n - (n - 1) }
Monad laws apply to the latter, so how is reordering justified?
It doesn't matter if 'f' is total, the context requires to know whether
'f v' is '0' or not. Since the only thing used from the result is its
successful evaluation, the case could be eliminated, but that still
leaves
return $! f v
=/=
return $ f v
But if you switch them, the program will *always* print 0.
In my copy of the docs, the only things known about 'unsafeInterleaveIO'
are its module, its type, and that is is unsafe. If we assume, from the name,
that evaluation of its parameter will be interleaved unsafely with the main IO
thread, there is no knowing when or if that evaluation will happen. Unless
there is a dependency on the result of that evaluation, in which case we have
an upper bound on when the evaluation must happen, but still no lower
bound. From the comments in the source code, it appears that lower
and upper bound are intended to be identical, ie. evaluation is supposed
to happen at the latest possible point permitted by dependencies.
Changing dependencies changes the program.
Also, the compiller might notice that x is never used, and that f is
total. So it could just optimize out the evaluation of f v
completely, at which point the program always prints 0 again; changing
optimization settings modifies the result of the program.
It doesn't matter whether or not 'x' is used. It matters whether 'f v'
needs to be evaluated to get at the 'return' action. Even if 'f' is total,
that evaluation cannot be skipped. Eta-expansion changes strictness,
which changes the program (eg, '\p-(fst p,snd p)' =/= 'id::(a,b)-(a,b)',
even though these functions only apply to pairs, so we know that
whatever 'p' is, it ought to be a pair - only we don't; and neither do
we know that 'f v' is a number, even if 'f' itself is total).
None of this means that lazy IO and monadic IO ought to be mixed
freely. If a program depends on strictness/non-strictness, that needs
to be taken into account, which can be troublesome, which is why
lazy IO hasn't been the default IO mechanism in Haskell for many
years. It is still available because when it is applicable, it can be
quite elegant and simple. But we need to decide whether or not
that is the case for each use case, even without the explicit 'unsafe'.
Hth?
Claus
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 23:30 schrieb Jonathan Cast: On Sun, 2009-03-15 at 23:18 +0100, Daniel Fischer wrote: Am Sonntag, 15. März 2009 22:20 schrieb Jonathan Cast: There is *no* guarantee that main0 prints 0, while main1 prints 1, as claimed. The compiler is in fact free to produce either output given either program, at its option. Since the two programs do in fact have exactly the same set of possible implementations, they *are* equivalent. So the ordering in fact *doesn't* matter. Hum. Whether the programme prints 0 or 1 depends on whether writeIORef r 1 is done before readIORef r. That depends of course on the semantics of IO and unsafeInterleaveIO. In so far as the compiler is free to choose there, it can indeed produce either result with either programme. But I think Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. (report, section 7) restricts the freedom considerably. Why not read that line as prohibiting concurrency (forkIO) as well? Good question. Because forkIO is a way to explicitly say one doesn't want the one thing necessarily done before the other, I'd say. As is unsafeInterleaveIO. (And as is unsafePerformIO, as per the docs: If the I/O computation wrapped in unsafePerformIO performs side effects, then the relative order in which those side effects take place (relative to the main I/O trunk, or other calls to unsafePerformIO) is indeterminate. ) However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. Where is this taken from? If GHC's library docs try to imply that the From the documentation of System.IO.Unsafe. This version of those docs: http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.html leaves unsafeInterleaveIO completely un-documented. So I'm still not sure what you're quoting from. programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted). Maybe. as explicitly allowing the programmer to say do it if and when the result is needed, not before. Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much. The full paragraph from the report: The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. I read it as saying that IO *does* allow the programmer to control when the effects are performed. Right. But by using forkIO or unsafeInterleaveIO you waive that ability. So I think main0 *must* print 0, because the ordering of the statements puts the reading of the IORef before the result of the unsafeInterleaveIOed action may be needed, so an implementation is obliged to read it before writing to it. In main1 however, v may be needed to decide what action's result x is bound to, before the reading of the IORef in the written order, so if f is strict, the unsafeInterleaveIOed action must be performed before the IORef is read and the programme must print 1, Although as Ryan pointed out, the compiler may decide to omit the case statement entirely, if it can statically prove that f v is undefined. I suppose that's a typo and should be unneeded. But can it prove that f v is unneeded? After all, it may influence whether 0 or 1 is printed. [Ignored: begging the question] jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast: On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote: However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. Where is this taken from? If GHC's library docs try to imply that the From the documentation of System.IO.Unsafe. This version of those docs: http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.htm l leaves unsafeInterleaveIO completely un-documented. So I'm still not sure what you're quoting from. The documentation haddock-0.9 built when I compiled ghc-6.8.3 last year. programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted). Maybe. as explicitly allowing the programmer to say do it if and when the result is needed, not before. Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much. The full paragraph from the report: The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. I read it as saying that IO *does* allow the programmer to control when the effects are performed. Right. But by using forkIO or unsafeInterleaveIO you waive that ability. That depends on the specification of unsafeInterleaveIO. If it is unspecified order of evaluation, then yes, if it is do when needed, not before, as my local documentation can be interpreted, then unsafeInterleaveIO reduces that ability, but doesn't completely remove it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Mon, 2009-03-16 at 01:04 +0100, Daniel Fischer wrote: Am Montag, 16. März 2009 00:47 schrieb Jonathan Cast: On Mon, 2009-03-16 at 00:14 +0100, Daniel Fischer wrote: However, I understand unsafeInterleaveIO allows IO computation to be deferred lazily. When passed a value of type IO a, the IO will only be performed when the value of the a is demanded. Where is this taken from? If GHC's library docs try to imply that the From the documentation of System.IO.Unsafe. This version of those docs: http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.htm l leaves unsafeInterleaveIO completely un-documented. So I'm still not sure what you're quoting from. The documentation haddock-0.9 built when I compiled ghc-6.8.3 last year. So it's a GHC (and base) major version out of date. programmer can predict when an unsafeInterleaveIO'd operation takes place --- well, then they shouldn't. I'm starting to suspect that not starting from a proper denotational theory of IO was a major mistake for GHC's IO system (which Haskell 1.3 in part adopted). Maybe. as explicitly allowing the programmer to say do it if and when the result is needed, not before. Haskell's order of evaluation is undefined, so this doesn't really allow the programmer to constrain when the effects are performed much. The full paragraph from the report: The I/O monad used by Haskell mediates between the values natural to a functional language and the actions that characterize I/O operations and imperative programming in general. The order of evaluation of expressions in Haskell is constrained only by data dependencies; an implementation has a great deal of freedom in choosing this order. Actions, however, must be ordered in a well-defined manner for program execution -- and I/O in particular -- to be meaningful. Haskell 's I/O monad provides the user with a way to specify the sequential chaining of actions, and an implementation is obliged to preserve this order. I read it as saying that IO *does* allow the programmer to control when the effects are performed. Right. But by using forkIO or unsafeInterleaveIO you waive that ability. That depends on the specification of unsafeInterleaveIO. If it is unspecified order of evaluation, then yes, if it is do when needed, not before, Note that `when needed' is still dependent on the (still unspecified) (non-IO) Haskell evaluation order. Also note that, to demonstrate any strong claims about unsafeInterleaveIO, you need to show that the compiler *must* perform in such-and-such a way, not simply that it *will* or that it *may*. as my local documentation can be interpreted, then unsafeInterleaveIO reduces that ability, but doesn't completely remove it. Sure. The question is whether the compiler has still enough options for re-ordering the program that transforming a program according to the standard equational axiomatic semantics for Haskell doesn't change the set of options the compiler has for the behavior of its generated code. jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
Yusaku Hashimoto wrote: Hello, I was studying about what unsafeInterleaveIO is.I understood unsafeInterleaveIO takes an IO action, and delays it. But I couldn't find any reason why unsafeInterleaveIO is unsafe. I have already read an example in http://www.haskell.org/pipermail/haskell-cafe/2009-March/057101.html says lazy IO may break purity, but I think real matter in this example are wrong use of seq. did I misread? For example: I have some universal state in IO. We'll call it an IORef, but it could be anything, like reading lines from a file. And I have some method for accessing and updating that state. next r = do n - readIORef r writeIORef r (n+1) return n Now, if I use unsafeInterleaveIO: main = do r - newIORef 0 x - do a - unsafeInterleaveIO (next r) b - unsafeInterleaveIO (next r) return (a,b) ... The values of a and b in x are entirely arbitrary, and are only set at the point when they are first accessed. They're not just arbitrary between which is 0 and which is 1, they could be *any* pair of values (other than equal) since the reference r is still in scope and other code in the ... could affect it before we access a and b, or between the two accesses. The arbitrariness is not random in the statistical sense, but rather is an oracle for determining the order in which evaluation has occurred. Consider, as an illustration these two alternatives for the ...: fst x `seq` snd x `seq` return x vs snd x `seq` fst x `seq` return x In this example, main will return (0,1) or (1,0) depending on which was chosen. You are right in that the issue lies in seq, but that's a red herring. Having made x, we can pass it along to any function, ignore the output of that function, and inspect x in order to know the order of strictness in that function. Moreover, let's have two pure implementations, f and g, of the same mathematical function. Even if f and g are close enough to correctly give the same output for inputs with _|_ in them, we may be able to observe the fact that they arrive at those answers differently by passing in our x. Given that such observations are possible, it is no longer safe to exchange f and g for one another, despite the fact that they are pure and give the same output for all (meaningful) inputs. This example is somewhat artificial because we set up x to use unsafeInterleaveIO in the bad way. For the intended use cases where it is indeed (arguably) safe, we would need to be sure to manually thread the state through the pure value (e.g. x) such that the final value is sane. For instance, in lazy I/O where we're constructing a list of lines/bytes/whatever, we need to ensure that any access to the Nth element of the list will first force the (N-1)th element, so that we ensure that the list comes out in the same order as if we forced all of them at construction time. For things like arbitrary symbol generation, unsafeInterleaveIO is perfectly fine because the order and identity of the symbols generated is irrelevant, but more importantly it is safe because the IO that's going on is not actually I/O. For arbitrary symbol generation, we could use unsafeInterleaveST instead, and that would be better because it accurately describes the effects. For any IO value which has real I/O effects, unsafeInterleaveIO is almost never correct because the ordering of effects on the real world (or whether the effects occur at all) depends entirely on the evaluation behavior of the program, which can vary by compiler, by compiler version, or even between different runs of the same compiled binary. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, Mar 15, 2009 at 1:56 PM, Jonathan Cast jonathancc...@fastmail.fm wrote: But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. But if the compiler is free to do this itself, what guarantee do I have that it won't? You don't really have any guarantee; the compiler is free to assume that v is a pure integer and that f is a pure function from integers to integers. Therefore, it can assume that the only observable affect of calling f v is non-termination. Note that unsafeInterleaveIO *breaks* this assumption; that is why it is unsafe. I erred previously in saying that this was allowed if f is total; it does still evaluate f v either way. But I can correct my argument as follows: the only observable effect from the (x - ...) line is non-termination. And the compiler can prove that there *no* observable effect of readIORef until the value is used or the reference is written by another function. So it is free to make this reordering anyways, as the only observable effect could have been non-termination which will be observed immediately after. When you use unsafeInterleaveIO or unsafePerformIO, you are required prove that its use does not break these invariants; that, for example, you don't read or write from IORefs that could be accessed elsewhere in the program. These are proofs that the compiler can and does make in some situations; it can reorder sequential readIORef calls if it thinks one or the other might be more efficient. It can evaluate foldl as if it was foldl' if it proves the arguments strict enough that non-termination behavior is identical (ghc -O2 does this, for example). The language has them as escape hatches that allow you to write code that would not otherwise be possible, by shifting more of a proof obligation on to the programmer. -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What unsafeInterleaveIO is unsafe
On Sun, 2009-03-15 at 18:11 -0700, Ryan Ingram wrote: On Sun, Mar 15, 2009 at 1:56 PM, Jonathan Cast jonathancc...@fastmail.fm wrote: But not if you switch the (x - ...) and (y - ...) parts: main = do r - newIORef 0 v - unsafeInterleaveIO $ do writeIORef r 1 return 1 y - readIORef r x - case f v of 0 - return 0 n - return (n - 1) print y Now the IORef is read before the case has a chance to trigger the writing. But if the compiler is free to do this itself, what guarantee do I have that it won't? You don't really have any guarantee; the compiler is free to assume that v is a pure integer and that f is a pure function from integers to integers. Therefore, it can assume that the only observable affect of calling f v is non-termination. Note that unsafeInterleaveIO *breaks* this assumption; [Ignored; begging the question] jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
