- Haskell-Cafe - Haskell.org

haskell blas bindings: does iomatrix gemv transposing of matrix a?
by Anatoly Yakovenko 17 Sep '08

17 Sep '08

Hey Patric, Thanks for your great work on the blas bidnings. I have a question on gemv. I thought its possible for blas to transpose the input matrix before doing the multiplication. Is it possible to do that with the haskell bindings? Or am I mistaken in how gemv is used Thanks, Anatoly

1 0

Semantic Domain, Function, and denotational model.....
by Daryoush Mehrtash 16 Sep '08

16 Sep '08

I have been told that for a Haskell/Functional programmer the process of design starts with defining Semantic Domain, Function, and denotational model of the problem. I have done some googling on the topic but haven't found a good reference on it. I would appreciate any good references on the topic. thanks, daryoush ps. I have found referneces like http://en.wikibooks.org/wiki/Haskell/Denotational_semantics which talks about semantic domain for "the Haskell programs 10, 9+1, 2*5" which doesn't do any good for me. I need something with a more real examples.

4 10

SYB with class: Bug in Derive.hs module
by Alexey Rodriguez Yakushev 16 Sep '08

16 Sep '08

Hi people (and Ralf and Alex), I found a bug in the SYB with class library when trying to implement generic equality. I am hoping that someone in the Cafe (maybe Ralf) can confirm it is a bug, or maybe show me that I am doing something wrong. I am using the "Scrap your boilerplate with class" library (http:// homepages.cwi.nl/~ralf/syb3/). More precisely, I am using the library distributed by the HAppS project, because it works with GHC 6.8 . You can get the repository as follows: darcs get http://happs.org/HAppS/syb-with-class However, the offending module (Derive.hs) produces broken instances in both distributions. The bug: ---------- Generic equality needs type safe casting when implemented in SYB3, I have tried both the gzipwith variant and using Pack datatypes (geq*.hs in the first distribution). However, both functions loop when applied to a tree value. This loop occurs when the functions try to cast one of the arguments. I have managed to reduce the error to a smaller source file that I send attached. It does the following: > main = print typeReps > > tree = (Bin (Leaf 1) (Leaf 2))::BinTree Int > > data Pack = forall x. Typeable x => Pack x > > packedChildren = gmapQ geqCtx Pack tree > > typeOfPack (Pack x) = typeOf x > > typeReps = map typeOfPack packedChildren Basically the tree is transformed into a list of Pack-ed values and then to a list of type representations. This program loops at "typeOf" when you call "main". The Data instance that Derive generates is as follows: > instance (Data ctx a, > Data ctx (BinTree a), > Sat (ctx (BinTree a))) => > Data ctx (BinTree a) where Note the recursive |Data ctx (BinTree a)| in the context. If I get rid of it (a correct manual instance is also included in the attachment) the example works. I thought of removing this from the context in the Derive source. But maybe I might break some other use cases. So I am asking for help! Should Derive be fixed? How? Cheers, Alexey

3 2

Hackage checks
by Andrea Rossato 16 Sep '08

16 Sep '08

Hi, the Hackage upload script performs some checks on the packages being uploaded. In my case, a library, I need to use the cabal generated Paths_package file to access some locale data stored in a data file directory. This requires to include in "hs-source-dirs" "dist/build/autogen", which doesn't exist in the source tree, since it's generated by cabal in the build process (the inclusion is made necessary by a bug in Cabal-1.2 which doesn't automatically search dist/build/autogen, see [1]). And so Hackage complains: I needed to manually include such an empty directory in the source code archive. Any way out? TIA Andrea [1] http://www.haskell.org/pipermail/libraries/2008-July/010078.html

3 3

Import qualified, inverse of hiding
by Mauricio 16 Sep '08

16 Sep '08

Hi, 'import' allows one to say 'hiding' to a list of names. Is it possible to do the opposite, i.e., list the names I want to import? Something like "import Module showing x"? Thanks, Maurício

4 7

Should `(flip (^^))` work?
by Mauricio 16 Sep '08

16 Sep '08

Hi, I tested the expression below and it doesn't work. Is there some way to achieve that (i.e., turning an expression inside parenthesis into an operator)? 2 `(flip (^^))` (3%4) Thanks, Maurício

5 5

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 15 Sep '08

15 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