September 2008 - Haskell-Cafe

Re: [Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008
by Richard A. O'Keefe 15 Sep '08

15 Sep '08

On 14 Sep 2008, at 10:59 pm, Rafael Almeida wrote: > One thing have always bugged me: how do you prove that you have > correctly proven something? This really misses the point of trying to formally verify something. That point is that you almost certainly have NOT. By the time you get a theorem prover to accept your specification, you have (a) gone through a couple of rounds of redesign (before writing the code!) and now have something really clear (because the prover is too dumb to understand subtle stuff) (b) just done a lot of "testing" on the design that was finally accepted. > I mean, when I write a code I'm formaly > stating what I want to happen and bugs happen. If I try to prove some > part of the code I write more formal text (which generally isn't even > checked by a compiler); I'm sorry? What kind of half-arsed "formal" specification is NOT "checked"? None of the specification tools I've played with (I really wish there were a PVS course I could attend in NZ) can truthfully be described as "not checked". Symbolic model checking tools effectivley _are_ testing tools; what you normally get from them is not a cheery "that's fine boss" but a snarky "you forgot about this possible input didn't you, idiot!" > how can I be sure that my proof doesn't > contain bugs? You can't. What you CAN be sure of is that your previous proof attempts DID contain bugs. Lots of them. At least *those* ones are gone. Let's face it, you can't be *sure* that you aren't a brain in a jar being systematically deceived by a demon. (Read Descartes.) In fact, you can usually be CERTAIN that you haven't proved the validity of your whole system, because you usually haven't tried. Formal methods are a risk reduction tool. You pick some part of the system which has a special need for reliability, isolate it, model it, check the model for consistency, specify operations on it, prove something about them, and you learn a heck of a lot by doing so. What you can't eliminate is the possibility that something nasty is lurking in the BIOS of your computer specifically watching out for your code so it can sabotage it. Several times in my programming career I have encountered perfectly correct code that malfunctioned because of a broken compiler (well ok, in one case it was a broken assembler). > Why would it make my program less error-prone? Is there > any article that tries to compare heavy testing with FM? Lots of them. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.2475 might make a good start. The idea that the FORTEST researchers share is that formal methods can *help* testing. Indeed, QuickCheck basically _is_ an 'automatic tests from specifications' tool, one of many that have been built over the years. If you stop thinking of formal methods as "verifying finished written programs" and more as some mix of "design for checkability" (so that bugs are less likely to be written into the code in the first place) or as "testing for specifications" it may make more sense to you.

5 4

Re: Proofs and commercial code -- was Haskell Weekly News: Issue 85 - September 13, 2008
by Greg Meredith 15 Sep '08

15 Sep '08

Daryoush, One of the subtle points about computation is that -- via Curry-Howard -- well-typed programs are *already* proofs. They may not be the proof you were seeking (there are a lot of programs from Int -> Int), or prove the theorem you were seeking to prove (Ord a => [a] -> [a] is a lot weaker than 'this program sorts lists of ordered types'), but they are witnesses of any type they type-check against. In a system that has principal types, they are proofs of their principal type. In this sense, the utility of proofs is widespread: they are programs. There is a really subtle dance between types that are rich enough to express the theorems you would have your programs be proofs of and the termination of type-checking for that type system. That's why people often do proofs by hand -- because the theorems they need to prove require a greater degree of expressiveness than is available in the type system supported by the language in which the programs are expressed. Research has really been pushing the envelope of what's expressible in types -- from region and resource analysis to deadlock-freedom. Again, in that setting the program is a witness of a property like - won't leak URLs to unsavory agents - won't hold on to handles past their garbage-collect-by date - won't get caught in a 'deadly embrace' (A is waiting for B, B is waiting for A) Sometimes, however, and often in mission critical code, you need stronger assurances, like - this code really does implement a FIFO queue, or - this code really does implement sliding window protocol, or - this code really does implement two-phase-commit-presumed-abort It's harder -- in fact i think it's impossible for bullet item 2 above -- to squeeze these into terminating type-checks. In those cases, you have to escape out to a richer relationship between 'theorem' (aka type) and 'proof' (aka program). Proof assistants, like Coq, or Hol or... can be very helpful for automating some of the tasks, leaving the inventive bits to the humans. In my experience, a proof of a theorem about some commercial code is pursued when the cost of developing the proof is less than some multiple of the cost of errors in the program in the life-cycle of that program. Intel, and other hardware vendors, for example, can lose a lot of business when the implementation of floating point operations is buggy; and, there is a breaking point where the complexity/difficulty/cost of proving the implementation correct is sufficiently less than that of business lost that it is to their advantage to obtain the kind of quality assurance that can be had from a proof of correctness. One other place where proofs of correctness will be pursued is in mathematical proofs, themselves. To the best of my knowledge, nothing mission-critical is currently riding on the proof of the 4-color theorem. The proof -- last i checked -- required programmatic checking of many cases. Proving the program -- that implements the tedious parts of the proof -- correct is pursued because of the culture and standard of mathematical proof. Best wishes, --greg Date: Sat, 13 Sep 2008 22:24:50 -0700 From: "Daryoush Mehrtash" <dmehrtash(a)gmail.com> Subject: Re: [Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008 To: "Don Stewart" <dons(a)galois.com> Cc: Haskell Cafe <haskell-cafe(a)haskell.org> Message-ID: <e5b8e9790809132224u3d29b858j5fda8e41b34566eb(a)mail.gmail.com> Content-Type: text/plain; charset="iso-8859-1" What I am trying to figure out is that say on the code for the IRC bot that is show here http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source What would theorem proofs do for me? Daryoush -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com

3 2

Re: [Haskell-cafe] ask
by Richard A. O'Keefe 15 Sep '08

15 Sep '08

On 15 Sep 2008, at 12:51 pm, Daniel Fischer wrote: > Am Montag, 15. September 2008 02:24 schrieb Cetin Sert: >> Hi why do I get? > > Buffering. For compiled programmes, stdin and stdout are line- > buffered by > default, so the output doesn't appear until the program finishes. > Either put > hSetBuffering stdout NoBuffering > at the top of main or, better IMO, > insert a > hFlush stdout > into ask before the readLn. > And in eval, putStrLn would be better, I think. Is this the problem we've had before, where the example in the Haskell 98 Report could not possibly work unless Haskell followed the same rule as C (read from stdin *automatically* flushes stdout), and the example works in several other Haskell systems, but not in GHC? Or is this a different problem?

1 0

ask
by Cetin Sert 14 Sep '08

14 Sep '08

Hi why do I get? cetin@linux-d312:~/lab/exp/1> ./eq 23 23 3 a = b = c = n1-0.8457820374040622n2-0.1542179625959377 when I run import System.IO main :: IO () main = do a ← ask "a" b ← ask "b" c ← ask "c" eval a b c ask v = do putStr (v ++ " = ") readLn eval a b c = do case delta < 0 of True → putStr "neg" False → putStr ("n1" ++ show n1 ++ "n2" ++ show n2) where delta = b*b - 4*c*a n o = (-b `o` sqrt(delta))/(2*a) n1 = n (+) n2 = n (-)

4 4

system in forkIO
by Marco Túlio Gontijo e Silva 14 Sep '08

14 Sep '08

Hello. > import System.Cmd > import GHC.Conc > > main :: IO () > main > = forkIO > ( do > putStrLn "fork" > system "ls" > return ()) > >> getChar > >> return () When I run this code, I get fork and the result of ls only after I press a key. Does getChar blocks the other threads? Greetings. -- marcot Página: http://marcotmarcot.iaaeee.org/ Blog: http://marcotmarcot.blogspot.com/ Correio: marcot(a)riseup.net XMPP: marcot(a)jabber.org IRC: marcot(a)irc.freenode.net Telefone: 25151920 Celular: 98116720 Endereço: Rua Turfa, 639/701 Prado 30410-370 Belo Horizonte/MG Brasil

5 7

message passing style in Monad
by jinjing 14 Sep '08

14 Sep '08

I found that as I can do xs.map(+1).sort by redefine . to be a . f = f a infixl 9 . I can also do readFile "readme.markdown" <.> lines <.> length by making a <.> b = a .liftM b infixl 9 <.> Kinda annoying, but the option is there. - jinjing

3 3

Views
by Stephan Friedrichs 14 Sep '08

14 Sep '08

Hello! List-like data structures should IMHO provide safe versions of 'head' and 'tail' (with safe I mean 'not partial', i. e. functions that don't provoke an 'error' when called with an empty collection). As far as I know, this is usually called 'view' and and has a type signature like view :: SomeDataStructure a -> View a with data View = Empty | Cons a (SomeDataStructure a) A good example for this is Data.Sequence. My question is: Why is this not expressed in terms of Maybe? view :: SomeDataStructure a -> Maybe (a, SomeDataStructure a) This would be easier to use, as there's no need for a new View type and because Maybe already provides instance declarations for a lot of useful classes (Functor, Monad, etc.) and handy helper functions (e. g. 'maybe'). Then you could, for instance, say: head xs = maybe undefined fst (view xs) tail xs = maybe undefined snd (view xs) You can of course argue that you want viewl and viewr to have different types in the case of Data.Sequence, but this is not the case for other, rather one-ended, data types, is it? Long story short, my problem is the following: I want to provide a 'view' function for Data.Heap in my heap [1] package and I don't know whether... a) ... to use Maybe b) ... to provide my own Data.Heap.View type c) ... a Data.View package with a View type should be included in the containers- or even base-package. This would prevent lots of small projects from creating totally equivalent View types. Maybe there even exists a Data.View package that I didn't find? Regards, Stephan [1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/heap-0.3.1 -- Früher hieß es ja: Ich denke, also bin ich. Heute weiß man: Es geht auch so. - Dieter Nuhr

5 7

random colors, stack space overflow, mersenne and mersenne.pure64
by Cetin Sert 14 Sep '08

14 Sep '08

Hi, The following piece of code runs just fine, if I say: instance Random RGB where random = color randomR = colorR instead of: instance Random RGB where random = color2 randomR = colorR When I use random = color2 I encounter a stack space overflow: cetin@linux-d312:~/lab/test/colors> ./var2 +RTS -K30000000 Stack space overflow: current size 30000000 bytes. Use `+RTS -Ksize' to increase it. I think I'm doing something wrong with the definition of colorR. Can anyone explain me what's wrong? import GHC.Word import Data.Word import System.Random import System.Random.Mersenne.Pure64 type RGB = (Int,Int,Int) instance Bounded RGB where minBound = minRGB maxBound = maxRGB minRGB = (0 ,0 ,0 ) maxRGB = (255,255,255) instance Random RGB where random = color2 randomR = colorR color2 :: RandomGen g ⇒ g → (RGB,g) color2 = colorR (minRGB,maxRGB) color :: RandomGen g ⇒ g → (RGB,g) color s0 = ((r,g,b),s3) where (r,s1) = q s0 (g,s2) = q s1 (b,s3) = q s2 q = randomR (0,255) colorR :: RandomGen g ⇒ (RGB,RGB) → g → (RGB,g) colorR ((a,b,c),(x,y,z)) s0 = ((r,g,b),s3) where (r,s1) = q (a,x) s0 (g,s2) = q (b,y) s1 (b,s3) = q (c,z) s2 q = randomR main :: IO () main = do mt ← newPureMT let cs = randoms mt :: [RGB] print cs ------------------------------------------ This one also just works fine: import Data.Word import System.Random.Mersenne type RGB = (Word8,Word8,Word8) instance MTRandom RGB where random m = do r ← random m :: IO Word8 g ← random m :: IO Word8 b ← random m :: IO Word8 return (r,g,b) main :: IO () main = do g ← newMTGen Nothing cs ← randoms g :: IO [RGB] print cs but I really need the range constraints colorR might provide me and would greatly appreciate any help to understand/solve the issue. Best Regards, Cetin P/s: uname -a Linux linux-d312 2.6.25.16-0.1-default #1 SMP 2008-08-21 00:34:25 +0200 x86_64 x86_64 x86_64 GNU/Linux

6 13

Heads Up: code.haskell.org is upgrading to darcs 2
by Duncan Coutts 14 Sep '08

14 Sep '08

This email is for darcs users in general and in particular for people who host a project on code.haskell.org. What we are doing ================= We are upgrading /usr/bin/darcs to version 2 on the machine that hosts code.haskell.org. That means it will be used by everyone who uses ssh to push or pull from a darcs repository on code.haskell.org. Pulling via http is completely unaffected. Do I have to do anything? ========================= No. You do not have to change anything. darcs v2 can talk to darcs v1 clients perfectly well so you do not need to upgrade your local version of darcs. You do not need to change the format of your local or server-side repositories. Darcs v2 works fine with darcs v1 format repositories. Should I change anything? ========================= We recommend that you upgrade your local darcs to version 2. This will allow you to take advantage of substantially faster push/pull operations over ssh (darcs 2 makes far fewer ssh connections). As noted above however it is not necessary for you to upgrade or for you to synchronise your upgrading with anyone else who uses the same repository. It is also possible to use a darcs "v1.5" hashed format locally and continue to use darcs v1 format on the server side. This has some performance and reliability advantages. Again this is something you can decide yourself without coordinating with other users of the repository. If your development style means that you bump into the infamous merging problems with darcs v1 format then you may consider converting your repository to the darcs v2 format. Remember that using darcs 2 with darcs v1 format repositories does not eliminate the merging issue. To banish the merging problems you have to use the darcs v2 format. This is however a more substantial change and has to be synchronised between users of the repository because it involves converting the server side repository to v2 format and all users getting the repository again. So if merging is an issue for you then you should discuss it with other users of your repository. Is this change safe? ==================== Yes. Darcs 2 has a substantial test suite. It has unit tests covering the core patch operations and also over 100 scripts doing functional testing, including network tests. The darcs build-bots run all these tests on all the popular platforms. Additionally, the code in darcs 2 for handling the v1 format is mostly the same as in darcs 1, so there are no big risks in using darcs 2 while continuing to use darcs v1 format repositories. The main change in the v1 format code is bug fixes, instrumentation code for debugging/introspection and more cunning types in the patch handling code that enforces some of the patch invariants. Furthermore, we have done real world tests using copies of all the 153 repositories on code.haskell.org which comes to around 2GB. We wanted to verify a couple things: 1. that using darcs 1 on the client and darcs 2 on the server works fine to pull and push patches. This corresponds to a project where all the users are still using darcs 1. 2. that using a mixture of darcs 1 and darcs 2 clients works when pushing and pulling patches between the clients via the server. This corresponds to a project where some users have upgraded but others have not yet. We tested with darcs 1.0.9 and 2.0.2 in three combinations: client darcs 1, server darcs 1 client darcs 1, server darcs 2 client darcs 2, server darcs 2 The test consisted of obliterating a significant number of patches from each repository and pushing them back. In a separate experiment each repository was converted to darcs v2 format which worked without problem in every case. What if I have problems? ======================== Contact support(a)community.haskell.org. We have made backups of all the repositories in case there are any critical problems. Thanks to the darcs hackers Eric Kow and Jason Dagit for doing all the hard testing work. Duncan, Ian and Malcolm (part of the community server admin team)

4 5

static linking failure -- can't find crt0
by Jason Dusek 14 Sep '08

14 Sep '08

I'm building a "really static" executable on OS X with options `-optl-static -static` and, while the libraries seem to link fine, the executable itself does not -- it can't find the C runtime. This is actually by design -- Apple "does not support" static binaries. There is a work around -- just symlink stuff till the errors go away -- but it might be better if I could statically link only those C libraries that I knew were not on stock Macs. Are there GHC options for that? I assume this all works fine on Linux and Windows, but I'll know soon enough... -- _jsn |...can't find the C runtime.| ld_classic: can't locate file for: -lcrt0.o collect2: ld returned 1 exit status |"does not support"| http://developer.apple.com/qa/qa2001/qa1118.html

1 0