- Haskell-Cafe - Haskell.org

CFP: Prog. Lang for Mechanized Mathematics Workshop
by Jacques Carette 12 Mar '07

12 Mar '07

Programming Languages for Mechanized Mathematics Workshop As part of Calculemus 2007 <http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/> Hagenberg, Austria [http://www.cas.mcmaster.ca/plmms07/] The intent of this workshop is to examine more closely the intersection between programming languages and mechanized mathematics systems (MMS). By MMS, we understand computer algebra systems (CAS), [automated] theorem provers (TP/ATP), all heading towards the development of fully unified systems (the MMS), sometimes also called universal mathematical assistant systems (MAS) (see Calculemus 2007 <http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/>). There are various ways in which these two subjects of /programming languages/ and /systems for mathematics/ meet: * Many systems for mathematics contain a dedicated programming language. For instance, most computer algebra systems contain a dedicated language (and are frequently built in that same language); some proof assistants (like the Ltac language for Coq) also have an embedded programming language. Note that in many instances this language captures only algorithmic content, and /declarative/ or /representational/ issues are avoided. * The /mathematical languages/ of many systems for mathematics are very close to a functional programming language. For instance the language of ACL2 is just Lisp, and the language of Coq is very close to Haskell. But even the mathematical language of the HOL system can be used as a functional programming language that is very close to ML and Haskell. On the other hand, these languages also contain very rich specification capabilities, which are rarely available in most computation-oriented programming languages. And even then, many specification languages ((B, Z, Maude, OBJ3, CASL, etc) can still teach MMSes a trick or two regarding representational power. * Conversely, functional programming languages have been getting "more mathematical" all the time. For instance, they seem to have discovered the value of dependent types rather recently. But they are still not quite ready to 'host' mathematics (the non-success of docon <http://www.haskell.org/docon/> being typical). There are some promising languages on the horizon (Epigram <http://www.e-pig.org/>, Omega <http://web.cecs.pdx.edu/%7Esheard/Omega/index.html>) as well as some hybrid systems (Agda <http://agda.sourceforge.net/>, Focal <http://focal.inria.fr/site/index.php>), although it is unclear if they are truly capable of expressing the full range of ideas present in mathematics. * Systems for mathematics are used to prove programs correct. (One method is to generate "correctness conditions" from a program that has been annotated in the style of Hoare logic and then prove those conditions in a proof assistant.) An interesting question is what improvements are needed for this both on the side of the mathematical systems and on the side of the programming languages. We are interested in all these issues. We hope that a certain synergy will develop between those issues by having them explored in parallel. These issues have a very colourful history. Many programming language innovations first appeared in either CASes or Proof Assistants, before migrating towards more mainstream languages. One can cite (in no particular order) type inference, dependent types, generics, term-rewriting, first-class types, first-class expressions, first-class modules, code extraction, and so on. However, a number of these innovations were never aggressively pursued by system builders, letting them instead be developped (slowly) by programming language researchers. Some, like type inference and generics have flourished. Others, like first-class types and first-class expressions, are not seemingly being researched by anyone. We want to critically examine what has worked, and what has not. Why are all the current ``popular'' computer algebra systems untyped? Why are the (strongly typed) proof assistants so much harder to use than a typical CAS? But also look at question like what forms of polymorphism exists in mathematics? What forms of dependent types exist in mathematics? How can MMS regain the upper hand on issues of 'genericity'? What are the biggest barriers to using a more mainstream language as a host language for a CAS or an ATP? This workshop will accept two kinds of submissions: full research papers as well as position papers. Research papers should be nore more than 15 pages in length, and positions papers no more than 3 pages. Submission will be through _EasyChair_. An informal version of the proceedings will be available at the workshop, with a more formal version to appear later. We are looking into having the best papers completed into full papers and published as a special issue of a Journal (details to follow). Important Dates April 25, 2007: Submission Deadline June 29-30, 2007: Workshop Program Committee Lennart Augustsson <http://www.cs.chalmers.se/%7Eaugustss> [Credit Suisse] Wieb Bosma <http://www.math.ru.nl/%7Ebosma/>[Radboud University Nijmegen, Netherlands] Jacques Carette <http://www.cas.mcmaster.ca/%7Ecarette> (co-Chair) [McMaster University, Canada] David Delahaye <http://cedric.cnam.fr/%7Edelahaye/> [CNAM, France] Jean-Christophe Filliâtre <http://www.lri.fr/%7Efilliatr/> [CNRS and Université de Paris-Sud, France] John Harrison <http://www.cl.cam.ac.uk/%7Ejrh13/> [Intel Corporation, USA] Markus (Makarius) Wenzel <http://www4.in.tum.de/%7Ewenzelm/> [Technische Universität München, Germany] Freek Wiedijk <http://www.cs.ru.nl/%7Efreek/> (co-Chair) [Radboud University Nijmegen, Netherlands] Wolfgang Windsteiger <http://www.risc.uni-linz.ac.at/people/wwindste/> [University of Linz, Austria] Location and Registration Location and registration information can be found on the Calculemus <http://www.risc.uni-linz.ac.at/about/conferences/Calculemus2007/> web site.

1 0

A valuable new combinator for Parsec?
by Maxime Henrion 12 Mar '07

12 Mar '07

Hello all, While using the very nice "option" combinator of Parsec recently, it seemed to me that it would be useful to have a more specific kind of combinator for optional tokens that wraps the token into a Maybe type. So, that gives: pmaybe :: GenParser tok st a -> GenParser tok st (Maybe a) pmaybe p = option Nothing (p >>= return . Just) I've been using it happily with some code of mine. Do people think that it would be generally useful to have in Parsec? Cheers, Maxime

3 2

Haskell Weekly News: March 12, 2007
by dons＠cse.unsw.edu.au 12 Mar '07

12 Mar '07

--------------------------------------------------------------------------- Haskell Weekly News http://sequence.complete.org/hwn/20070312 Issue 59 - March 12, 2007 --------------------------------------------------------------------------- Welcome to issue 59 of HWN, a weekly newsletter covering developments in the [1]Haskell community. This week we see the 2007 Haskell Workshop announcement, Haskell.org's participation in the Google Summer of Code gets underway, and of course, new libraries! 1. http://haskell.org/ Announcements Google Summer of Code and Haskell.org. Malcolm Wallace [2]announced that Haskell.org has once again applied to be a mentoring organisation for the Google Summer of Code. If you are a student who would like to earn money hacking in Haskell, or you are a non-student who has a cool idea for a coding project but no time to do it yourself, then visit the [3]SoC wiki to gather ideas, and add yourself to the list of interested people! Add new ideas for projects! 2. http://article.gmane.org/gmane.comp.lang.haskell.cafe/20232 3. http://hackage.haskell.org/trac/summer-of-code Haskell Workshop Call for Papers. Gabriele Keller [4]announced the initial call for papers for the Haskell Workshop 2007, part of the 2007 International Conference on Functional Programming (ICFP). The purpose of the Haskell Workshop is to discuss experience with Haskell, and possible future developments for the language. The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of Haskell. 4. http://article.gmane.org/gmane.comp.lang.haskell.general/14977 Data.CompactString 0.3: Unicode ByteString. Twan van Laarhoven [5]announced version 0.3 of the Data.CompactString library. Data.CompactString is a wrapper around Data.ByteString supporting Unicode strings. 5. http://article.gmane.org/gmane.comp.lang.haskell.general/14973 harchive-0.2: backup and restore software in Haskell. David Brown [6]announced release 0.2 of [7]harchive, a program for backing up and restoring data. The package is available [8]from Hackage. 6. http://article.gmane.org/gmane.comp.lang.haskell.general/14972 7. http://www.davidb.org/darcs/harchive/ 8. http://hackage.haskell.org/cgi-bin/hackage-scripts/package/harchive-0.2 New release of regex packages. Chris Kuklewicz [9]announced new versions of the regex-* packages (base,compat,dfa,parsec,pcre,posix,tdfa,tre). There is a new [10]wiki page with documentation relating to these packages. All packages are available from [11]Hackage, under the [12]Text Category. 9. http://article.gmane.org/gmane.comp.lang.haskell.cafe/20189 10. http://haskell.org/haskellwiki/Regular_expressions 11. http://hackage.haskell.org/packages/hackage.html 12. http://hackage.haskell.org/packages/archive/pkg-list.html#cat:Text StaticDTD: type safe markup combinators from DTDs. Marcel Manthe [13]announced a tool that transforms a Document Type Definition to a library. The resulting library contains combinators that assure proper nesting of elements. The plan is to add more constraints that will also take care of the order of occurrence of children. The parsing of the DTD is done with HaXml. The code is [14]available via darcs. 13. http://article.gmane.org/gmane.comp.lang.haskell.cafe/20218 14. http://m13s07.vlinux.de/darcs/StaticDTD/ IPv6 support for network package. Bryan O'Sullivan [15]announced that he'd added IPv6 support to the network package. 15. http://thread.gmane.org/gmane.comp.lang.haskell.libraries/6363 Type-level binary arithmetic library. Oleg Kiselyov and Chung-chieh Shan [16]announced a [17]new library for arbitrary precision binary arithmetic over natural kinds. The library supports addition/subtraction, predecessor/successor, multiplication/division, exp2, full comparisons, GCD, and the maximum. At the core of the library are multi-mode ternary relations Add and Mul where any two arguments determine the third. Such relations are especially suitable for specifying static arithmetic constraints on computations. The type-level numerals have no run-time representation; correspondingly, all arithmetic operations are done at compile time and have no effect on run-time. 16. http://article.gmane.org/gmane.comp.lang.haskell.general/14961 17. http://pobox.com/~oleg/ftp/Computation/resource-aware-prog/BinaryNumber.hs Haskell' This section covers the [18]Haskell' standardisation process. * [19]Deriving Functor 18. http://hackage.haskell.org/trac/haskell-prime 19. http://thread.gmane.org/gmane.comp.lang.haskell.prime/2135 Libraries This week's proposals and extensions to the [20]standard libraries. * [21]Add IPv6 support to network library * [22]Error handling conventions 20. http://haskell.org/haskellwiki/Library_submissions 21. http://thread.gmane.org/gmane.comp.lang.haskell.libraries/6377 22. http://thread.gmane.org/gmane.comp.lang.haskell.libraries/6382 Discussion Avoiding intermediate data structures. David Roundy [23]opened discussion on techniques for avoiding intermediate data structures in Haskell code 23. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/20319 Maybe a different Maybe. Joachim Breitner [24]wondered about avoiding intermediate Maybe constructs 24. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/20300 Blog noise [25]Haskell news from the blogosphere. * [26]STM, IO, and a Simple Persistence Model * [27]Dynamic programming in Haskell * [28]Collected 'good math/bad math' Haskell articles * [29]3 open questions about monads * [30]Documentation, libraries and speed matter * [31]Why monads matter * [32]Design Patterns in Haskell: bracket * [33]Practical Haskell: shell scripting with error handling and privilege separation * [34]Simple socket programming * [35]'interact' for TCP sockets * [36]Monads in C, part 3 * [37]Directory tree printing in Haskell. Part 2 * [38]Monads through Pictures * [39]Notes on hacking Haskell * [40]Wanted: Haskell Programmer * [41]Why Publish CS Papers Without Code? * [42]The 8 ways to report errors in Haskell 25. http://planet.haskell.org/ 26. http://mult.ifario.us/articles/2007/03/04/stm-and-io 27. http://sequence.complete.org/node/263 28. http://scienceblogs.com/goodmath/goodmath/programming/haskell/ 29. http://www.randomhacks.net/articles/2007/03/05/three-things-i-dont-understa… 30. http://kawagner.blogspot.com/2007/03/why-do-most-people-seem-to-use-inferio… 31. http://www.rfc1149.net/blog/2007/03/06/why-monads-matter/ 32. http://notes-on-haskell.blogspot.com/2007/03/design-patterns-in-haskell-bra… 33. http://cgi.cse.unsw.edu.au/~dons/blog/2007/03/06#programmable-semicolons 34. http://metavar.blogspot.com/2007/03/simple-socket-programming.html 35. http://stephan.walter.name/blog/computers/programming/haskell/interacttcp.h… 36. http://sigfpe.blogspot.com/2007/03/monads-in-c-pt-iii.html 37. http://blog.moertel.com/articles/2007/03/07/directory-tree-printing-in-hask… 38. http://www.bolour.com/papers/monads-through-pictures.html 39. http://metavar.blogspot.com/2007/03/haskell-hacking-notes-or-prelude-to.html 40. http://blogs.teamb.com/craigstuntz/archive/2007/03/09/WantedHaskellDevelope… 41. http://billmill.org/why_no_code 42. http://www.randomhacks.net/articles/2007/03/10/haskell-8-ways-to-report-err… Quotes of the Week * fishkandy: The problem with comparing apples to apples is that haskell has 'mango daiquiri' as a basic fruit * fax--: I wake up with a headache because of you, Haskell * norpan: I use functions, but i don't use them as arrows: I prefer silver bullets * ray: Some people claim everything is lisp. One time I was eating some spaghetti and someone came by and said: 'Hey, nice lisp dialect you're hacking in there' * roconnor: Damn it! Haskell pseudo code is indistinguishable from actual code * shapr: Today's nifty error message: *Main> thread blotttchhhkrrreeeedaaa dddinbbbdllleooofcccikkkneeeidddt eiiilnnnydddeeefffiiinnniiittteeelllyyy * stepcut: C? isn't that some low-level language that compilers output to? * wkh: Why does the haskell webpage link to 'research papers' under the 'getting started' section? Code Watch Tue Mar 6 06:31:12 PST 2007. Simon Marlow. [43]add noDuplicate#. This primop ensures that the current computation is not being duplicated, by calling threadPaused(). The idea is to use it inside unsafePerformIO/unsafeInterleaveIO (see #986). 43. http://article.gmane.org/gmane.comp.lang.haskell.cvs.ghc/19536 About the Haskell Weekly News Each week, new editions are posted to [44]the Haskell mailing list as well as to [45]the Haskell Sequence and [46]Planet Haskell. [47]RSS is also available, and headlines appear on [48]haskell.org. Headlines are available as [49]PDF. To help create new editions of this newsletter, please see the [50]contributing information. Send stories to dons at cse.unsw.edu.au. The darcs repository is available at darcs get [51]http://www.cse.unsw.edu.au/~dons/code/hwn 44. http://www.haskell.org/mailman/listinfo/haskell 45. http://sequence.complete.org/ 46. http://planet.haskell.org/ 47. http://sequence.complete.org/node/feed 48. http://haskell.org/ 49. http://www.cse.unsw.edu.au/~dons/code/hwn/archives/20070312.pdf 50. http://haskell.org/haskellwiki/HWN 51. http://www.cse.unsw.edu.au/~dons/code/hwn

1 0

State of Ignorance
by Hans van Thiel 12 Mar '07

12 Mar '07

Hello All, I have the following functions, based on Thompson's CFP example (also in Control.Monad.State documentation) of using a state monad on a tree. My functions (on a list) work, but I don't understand why. Main> getInds ["house","tree","cat","house","cat","dog","tree"] [0,1,2,0,2,3,1] Main> getTb ["house","tree","cat","house","cat","dog","tree"] ["house","tree","cat","dog"] This, from CFP, is clear enough. repl1 :: String -> [String] -> ([String], Int) repl1 x tb | elem x tb = (tb, fromJust (elemIndex x tb)) | otherwise = (tb ++ [x], length tb) then, turn this into a function to a state monad type: toMyState :: String -> MyState String Int toMyState x = MyStateC (repl1 x) where the monad is defined as: data MyState a b = MyStateC ([a] -> ([a], b)) instance Monad (MyState a) where return x = MyStateC (\tb -> (tb, x)) (MyStateC st) >>= f = MyStateC (\tb -> let (newtb, y) = st tb (MyStateC trans) = f y in trans newtb ) Now I understand this (barely) in the sense that >>= works through defining how f takes its values from st. So, f would be the function: toMystate and trans would be: (repl1 x). But then y would have to be of type String, whereas the y in the tuple would have type Int, since it is generated by st. I just don't get it. Next the book explains how to extract values from a state and again that's pretty clear: extr1 :: MyState a b -> b extr1 (MyStateC st) = snd (st []) extr2 :: MyState a b -> [a] extr2 (MyStateC st) = fst (st []) I have a list instead of a tree, so I tried: strtoMS :: [String] -> [MyState String Int] strtoMS ls = map toMyState ls and the final functions are: getInds :: [String] -> [Int] getInds = extr1 . sequence . strtoMS getTb :: [String] -> [String] getTb = extr2 . sequence . strtoMS They work, but now I don't understand sequence, defined in the Prelude. From: a Tour of the Haskell Monad Functions http://members.chello.nl/hjgtuyl/tourdemonad.html sequence :: Monad m => [m a] -> m [a] sequence = foldr mcons (return []) where mcons p q = p >>= \x -> q >>= \y -> return (x : y) This has a different bind (>>=) from the one in the MyState monad, yet is appears to perform all the state transformations. The documentation says: "sequence xs evaluates all monadic values in the list xs, from left to right, and returns a list of the "contents" of these monads, placing this list in a monad of the same type. Note, that "evaluating" can be interpreted as "performing an action", for example in the case of print." It looks to me as if sequence works here because values of MyState are themselves functions, but how? Many thanks for any pointers and clarification! Hans van Thiel

2 1

Simple benchmark of list operations?
by Bulat Ziganshin 11 Mar '07

11 Mar '07

Hello haskell-cafe, Page http://community.livejournal.com/ru_lambda/44716.html contains three very simple but long-working benchmark functions: dummy :: [Int] -> [Int] dummy [] = [] dummy (x:xs) = x:dummy (dummy xs) dummy2 :: [Int] -> [Int] dummy2 = dum [] where dum w [] = w dum w (x:xs) = dum (w++[x]) (dummy2 xs) dummy3 :: [Int] -> [Int] dummy3 = dum [] where dum w [] = reverse w dum w (x:xs) = dum (x:w) (dummy3 xs) *Main> dummy [1..21] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] (16.97 secs, 157120860 bytes) *Main> dummy2 [1..21] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] (2.42 secs, 151470452 bytes) *Main> dummy3 [1..21] [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] (1.78 secs, 84642856 bytes) *Main> Is it interesting for testing haskell compilers? -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

2 1

Program Command Line Arguments
by unknown＠example.com 11 Mar '07

11 Mar '07

My apologies if this is a question with a trivial answer. Command line args in C are accessed via argc and argv[] defined as arguments to main();. How are command line arguments to a ghc-compiled program accessed in Haskell? Or is that even possible? Thanks.

3 2

literate Haskell newbie question
by Immanuel Normann 10 Mar '07

10 Mar '07

I am a newbie to literate Haskell and these are my two simple questions: How do I compile a literate haskell file foo.lhs (using ghc-6.6)? Is there a tool that translates foo.lhs to foo.hs? Surprisingly I don't find the answer in http://haskell.org/haskellwiki/Literate_programming whereas a lot about translation into tex-files can be found. Thanks, Immanuel

4 3

Implementation of "Dynamic" datatype
by Isaac Dupree 09 Mar '07

09 Mar '07

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Currently we have data Dynamic = Dynamic TypeRep Obj where Obj is {-in GHC up to 6.6-} type Obj = forall a . a {-in GHC 6.7.something-} type Obj = Any -- Use GHC's primitive 'Any' type to hold the dynamically typed value. {-in some other compilers (like Hugs)-} data Obj = Obj ( According to this comment, it is not data Obj = Obj in GHC now because: -- In GHC's new eval/apply execution model this type must not -- look like a data type. If it did, GHC would use the -- constructor convention when evaluating it, and this will go -- wrong if the object is really a function. Using Any [or, -- earlier comments said, a polymorphic type] forces GHC to use -- a fallback convention for evaluating it that works for all -- types. ) So, my question is: why doesn't it just use an existential? : data Dynamic = forall a. Dynamic TypeRep a According to http://hackage.haskell.org/trac/haskell-prime/wiki/HaskellExtensions , all important implementations support existentials (and it will probably go into Haskell'). It seems semantically the most accurate, doesn't require an unsafeCoerce when _constructing_ a Dynamic, and doesn't require unsafeCoercing between unequal types (which had caused problems in GHC as noted above), so it seems like it could be a portable implementation. A quick copy of Dynamic.hs with these modifications seemed to work fine in ghc6.4.2, ghc6.6, and hugs20050308 (which is all haskell implementations that are working for me at the moment (nhc98 is broken for me) and that have Data.Typeable (not yhc currently, it seems)). ( Also I wonder about the performance implications of changing it to data Dynamic = forall a. Typeable a => Dynamic a or making the TypeRep be a strict field (which shouldn't have any semantic impact since typeOf always succeeds(assuming no-one defines a horrible instance of Typeable) and typeOf's result is always what is put into that field. (Separately, should seq'ing a Dynamic seq the encapsulated object, or should Dynamic act as a box as it does now?)). ) Anyway, how would I go about seriously testing this in ghc, hugs... to see if it breaks anything (and also see how it affects Dynamic's performance)? (Since I am interested in the refactoring of the base/core libraries, a little something like this seems like a good place to start learning how to test what I have.) Isaac - - Was this a good mailing list to choose for this question? (And was it a good question? what about all the little question-ideas branching off of it? I can never be sure...) -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.3 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFF6LVSHgcxvIWYTTURAoeTAKCP8XIn4pVXnJsimEX8aAgIcXLb1ACbBOw2 elKn59TdPKiAJq8VA4MOd0o= =NF4R -----END PGP SIGNATURE-----

5 10

Google summer of code
by Malcolm Wallace 09 Mar '07

09 Mar '07

Google Summer of Code As many of you will already know, Google is running its "Summer of Code" project again this year, and haskell.org is once again going to apply to be a mentoring organisation. Are you a student who would like to earn money for hacking in Haskell? Or are you a non-student who has a cool idea for a coding project but no time to do it yourself? Well, our wiki to gather ideas is now up-and-running again: http://hackage.haskell.org/trac/summer-of-code Add yourself to the list of interested people! There are some ideas still there from last year. Add new ones! Google will start accepting student applications in just over a week's time, but now is the time to start using our own wiki to match up interesting ideas with interested people. The official timeline is as follows: March 12: Mentoring organization application deadline March 14: List of accepted mentoring organizations published March 14: Student application period opens March 24: Student application deadline Interim Period: we review and rank student proposals April 9: List of accepted student applications published Interim Period: Students learn more about their project communities May 28: Students begin coding; Google begins issuing initial payments July 9: Students upload code to code.google.com/hosting; July 16: Google begins issuing mid-term payments August 20: Students upload code to code.google.com/hosting; August 31: Final evaluation deadline; Google begins issuing final payments Regards, Malcolm

6 6

auto-completion for Vim 7
by Stephan Walter 09 Mar '07

09 Mar '07

Hi, I started to write a Vim script for the new omni-completion feature of Vim 7. If you use Vim you might want to check it out: * download http://stephan.walter.name/files/haskellcomplete.vim and put it in ~/.vim/plugin * :set omnifunc=haskellcomplete#CompleteHaskell * press <c-x><c-o> to complete (The advantage of omni-completion over normal completion using <c-n> and <c-p> is that you can write you own function which does some smart guessing to offer good completions) So far the functionality is *very* limited. It will autocomplete a few functions from the prelude as well as functions in the current file that have a type declaration. If you look through the source code of the script, you'll see that I have included some function names and types from the standard libraries. Before I continue this (rather tedious) work, I wanted to know what the cafe patrons think about it. If someone knows of a simple way to generate a function/type list of the standard modules, I'd love to hear about it. Generating such a list on the fly each time is probably not an option, as it would be too slow. -Stephan

5 9