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] On the purity of Haskell
A perhaps acceptable notion of the property we want (purity etc.) is that all the extensions of the purely functional core language of Haskell (say the lazy lambda calculus extended with data constructors, etc) are _conservative_, that is all the equations that hold in the pure core language still hold in the extended language. For a part of Concurrent Haskell such a conservativity result is shown in D.Sabel , M. Schmidt-Schauß. On conservativity of Concurrent Haskell. Frank report 47, 2011. http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-47.pdf It also shows that with arbitrary use of unsafeInterleaveIO conservativity does not hold. And of course the result does not capture any IO-operation (only takeMVar, putMVar and spawning threads are considered), but it may be extended to more operations ... Just my two cents, David On 30.12.2011 02:07, Conal Elliott wrote: I wrote that post to point out the fuzziness that fuels many discussion threads like this one. See also http://conal.net/blog/posts/notions-of-purity-in-haskell/ and the comments. I almost never find value in discussion about whether language X is functional, pure, or even referentially transparent, mainly because those terms are used so imprecisely. In the notions-of-purity post, I suggest another framing, as whether or not a language and/or collection of data types is/are denotative, to use Peter Landin's recommended replacement for functional, declarative, etc. I included some quotes and a link in that post. so people can track down what denotative means. In my understanding, Haskell-with-IO is not denotative, simply because we do not have a (precise/mathematical) model for IO. And this lack is by design, as explained in the toxic avenger remarks in a comment on that post. I often hear explanations of what IO means (world-passing etc), but I don't hear any consistent with Haskell's actual IO, which includes nondeterministic concurrency. Perhaps the difficulties could be addressed, but I doubt it, and I haven't seen claims pursued far enough to find out. - Conal On Thu, Dec 29, 2011 at 4:42 PM, Steve Horne sh006d3...@blueyonder.co.uk mailto:sh006d3...@blueyonder.co.uk wrote: On 30/12/2011 00:16, Sebastien Zany wrote: Steve Horne wrote: I haven't seen this view explicitly articulated anywhere before See Conal Elliott's blog post The C language is purely functional http://conal.net/blog/posts/the-c-language-is-purely-functional. Thanks - yes, that's basically the same point. More concise - so clearer, but not going into all the same issues - but still the same theme. ___ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Lambda Calculus: Bound and Free formal definitions
Hi, the definition in the book is a syntactic one, you are not allowed to beta-reduce when applying the definition. In particular E = E1 E2 = (\x.xy)(\z.z) The definition speaks about the term (\x.xy)(\z.z) and not about (\z.z)y and the definition does not speak about occurences of variables, it implicitely defines the _set_ of bound variables and the _set_ of free variables of term. Both sets needn't be disjoint, for example In (\x.x) x x is a free as well as a bound variable. Regards, David Am 30.12.2010 04:50, schrieb Mark Spezzano: Hi all, Thanks for your comments Maybe I should clarify... For example, 5.2 FREE: If E1 = \y.xy then x is free If E2 = \z.z then x is not even mentioned So E = E1 E2 = x (\z.z) and x is free as expected So E = E2 E1 = \y.xy and x is free as expected 5.3 BOUND: = If E1 = \x.xy then x is bound If E2 = \z.z then is not even mentioned So E = E1 E2 = (\x.xy)(\z.z) = (\z.z)y -- Error: x is not bound but should be by the rule of 5.3 So E = E2 E1 = (\z.z)(\x.xy) = (\x.xy) then x is bound. Where's my mistake in the second-to-last example? Shouldn't x be bound (somewhere/somehow)? Thanks, Mark On 30/12/2010, at 1:52 PM, Mark Spezzano wrote: Duh, Sorry. Yes, there was a typo the second one should read If E is a combination E1 E2 then X is bound in E if and only if X is bound in E1 or is bound in E2. Apologies for that oversight! Mark On 30/12/2010, at 1:21 PM, Antoine Latter wrote: Was there a typo in your email? Because those two definitions appear identical. I could be missing something - I haven't read that book. Antoine On Wed, Dec 29, 2010 at 9:05 PM, Mark Spezzano mark.spezz...@chariot.net.au wrote: Hi, Presently I am going through AJT Davie's text An Introduction to Functional Programming Systems Using Haskell. On page 84, regarding formal definitions of FREE and BOUND variables he gives Defn 5.2 as The variable X is free in the expression E in the following cases a)omitted b) If E is a combination E1 E2 then X is free in E if and only if X is free in E1 or X is free in E2 c)omitted Then in Defn 5.3 he states The variable X is bound in the expression E in the following cases a)omitted b) If E is a combination E1 E2 then X is free in E if and only if X is free in E1 or X is free in E2. c)omitted Now, are these definitions correct? They seem to contradict each otherand they don't make much sense on their own either (try every combination of E1 and E2 for bound and free and you'll see what I mean). If it is correct then please give some examples of E1 and E2 showing exactly why. Personally I think that there's an error in the book. You can see the full text on Google Books (page 84) Thanks for reading! Mark Spezzano ___ 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 ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Papers discussing interpreters for call by need?
As a starting point I would suggest Peter Sestoft : Deriving a lazy abstract machine, Journal of Functional Programming 7(3), 1997 ( http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4314 ) Different abstract machines for call-by-need evaluation are built starting from Launchburys natural semantics, the alpha renaming problem is discussed and solved by using environments and at the end by using a nameless representation for variables. Regards, David Am 17.11.2010 22:02, schrieb David Sankel: I'm writing an interpreter for a call by need language and have been doing a direct implementation of the Launchbury semantics. My problem is that in the variable rule, an alpha conversion is done that, as far as I understand, is going to hinder any tail call optimization. I realize that the intent of Launchbury's paper is to come up with a theoretical framework for call by need, not to guide an implementation per say. Is anyone aware of any papers out there that go into detail on the construction of an actual interpreter? TIA, David -- David Sankel Sankel Software www.sankelsoftware.com http://www.sankelsoftware.com 585 617 4748 (Office) ___ 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] Monad laws
Hi, thanks for all the comments. In ghc 6.12.1 the behavior is strange: If f is defined in the interpreter via let, then the seq-expression converges GHCi, version 6.12.1: http://www.haskell.org/ghc/ :? for help let f = \x - (undefined::IO Bool) seq (f True) True True but if you build a let-expression then it diverges let f = \x - (undefined::IO Bool) in seq (f True) True *** Exception: Prelude.undefined for the first way: if you use another type, then it diverges: let f = \x - (undefined::Bool) seq (f True) True *** Exception: Prelude.undefined Regards, David Andrés Sicard-Ramírez schrieb: On 2 March 2010 15:44, Luke Palmer lrpal...@gmail.com mailto:lrpal...@gmail.com wrote: On Tue, Mar 2, 2010 at 1:17 PM, David Sabel sa...@ki.informatik.uni-frankfurt.de mailto:sa...@ki.informatik.uni-frankfurt.de wrote: Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a = f ≡ f a I figured out that there is the distinguishing context (seq [] True) which falsifies the law for a and f defined below let a = True let f = \x - (undefined::IO Bool) seq (return a = f) True True seq (f a) True *** Exception: Prelude.undefined Is there a side-condition of the law I missed? No, IO just doesn't obey the laws. However, I believe it does in the seq-free variant of Haskell, which is nicer for reasoning. In fact, this difference is precisely what you have observed: the distinguishing characteristic of seq-free Haskell is that (\x - undefined) == undefined, whereas in Haskell + seq, (\x - undefined) is defined. In GHC 6.12.1 both expressions reduce to True, but it doesn't happen in GHC 6.10.4. Any ideas why the behaviour is different? -- Andrés ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Monad laws
Hi, when checking the first monad law (left unit) for the IO-monad (and also for the ST monad): return a = f ≡ f a I figured out that there is the distinguishing context (seq [] True) which falsifies the law for a and f defined below let a = True let f = \x - (undefined::IO Bool) seq (return a = f) True True seq (f a) True *** Exception: Prelude.undefined Is there a side-condition of the law I missed? Regards, David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] beginner's problem about lists
Malcolm Wallace wrote: Matthias Fischmann [EMAIL PROTECTED] wrote: No, your Fin type can also hold infinite values. let q = FinCons 3 q in case q of FinCons i _ - i == _|_ does that contradict, or did i just not understand what you are saying? That may be the result in ghc, but nhc98 gives the answer 3. It is not entirely clear which implementation is correct. The Language Report has little enough to say about strict components of data structures - a single paragraph in 4.2.1. It defines them in terms of the strict application operator ($!), thus ultimately in terms of seq, and as far as I can see, nhc98 is perfectly compliant here. The definition of seq is seq _|_ b = _|_ seq a b = b, if a/= _|_ In the circular expression let q = FinCons 3 q in q it is clear that the second component of the FinCons constructor is not _|_ (it has at least a FinCons constructor), and therefore it does not matter what its full unfolding is. The translation given in the language report says this expression is equivalent to let q = (\x1 x2 - (( FinCons' $ x1) $! x2) ) 3 q in q (where FinCons' is a lazy constructor) in terms of seq let q = (\x1 x2 - x2 `seq` ( FinCons' x1 x2 ) ) 3 q in q this evaluates to let q = (q `seq` ( FinCons' 3) ) in q hence on top-level q is rather a seq-expression than a constructor-expression ;-) Regards, David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Defining show for a function type.
Hi, you can make every function being an instance of class Show, this works for me: instance Show (a - b) where show _ = FUNCTION data Element = Int Int | Float Float | Func (Machine - Machine) deriving Show David Johan Grönqvist wrote: I am a haskell-beginner and I wish to write a Forth-like interpreter. (Only for practice, no usefulness.) I would like use a list (as stack) that can contain several kinds of values. data Element = Int Int | Float Float | Func : Machine - Machine | ... Now I would like to have this type be an instance of the class Show, so that I can see what the stack contains in ghci. deriving Show is impossible as Func is not instance of Show. Can I make it instance of Show? I just want to define something like show (Func _) = Function, cannot show and I am not interested in actually displaying any information about the function, but I am interested in getting information about elements of other kinds. So far I have just guessed, but failed to produce anything that does not give an error stating that my function is not of the form (T a b c) where T is not an alias and a b c are simple type variables (or so). Any help appreciated! Johan ___ 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] lazy readFile
Hi! I'm also interested, how to get this example working: http://www.haskell.org/pipermail/haskell/2001-November/008336.html This seems to be an old discussion: http://www.haskell.org/pipermail/libraries/2001-April/000358.html Was a strictReadFile implemented in the meantime? Here's my implementation of strictReadFile: import System.IO strictReadFile path = do handle - openFile path ReadMode strictReadFromHandle handle strictReadFromHandle handle = do eof - hIsEOF handle if eof then do hClose handle return [] else do c - hGetChar handle y - strictReadFromHandle handle return (c:y) Cheers, David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: tracing Haskell programs
Hi, Maybe Hat - The Haskell Tracer can help: http://haskell.org/hat/ - Original Message - From: [EMAIL PROTECTED] To: [EMAIL PROTECTED] Sent: Sunday, October 19, 2003 10:25 AM Subject: tracing Haskell programs Hi folk Is there a way to follow the execution of a Haskell program? What I mean here is a way to see which function definition is being used at any moment, and how the execution control moves around a script file. If this is a preposterous question, just tell me nicely and I will go away! Oh, and if this has been discussed before, please tell me where and I will chase it up. Thanks! -- Wamberto Vasconcelos, PhD [EMAIL PROTECTED] Department of Computing Sciencehttp://www.csd.abdn.ac.uk/~wvasconc University of Aberdeen, Aberdeen AB24 3UE, Scotland, UK Phone +44 (0)1224 272283 Fax +44 (0)1224 273422 ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
