June 2010 - Haskell - Haskell.org

ANNOUNCE: ioctl 0.0.1
by Maciej Piechotka 13 Sep '15

13 Sep '15

A package for type-safe I/O control. Currently only ioctl is supported. Currently simply a extract from my tuntap fork TODO: - Return the integer as well as structure (will break the API) - Port for Windows Network.Socket.IOCtl (as soon as I manage to setup some sane environment on this platform) - Wrapping around DeviceIoControl Example (in hsc): data NotRead = NotRead instance NotRead Int where ioctlReq _ = #const FIONREAD notRead s = ioctlsocket' s NotRead Regards

2 1

Announcing Djinn, version 2004-12-11, a coding wizard
by Lennart Augustsson 07 Apr '11

07 Apr '11

Howdy, y'all! I've written a small program that takes a (Haskell) type and gives you back a function of that type if one exists. It's kind of fun, so I thought I'd share it. It's probably best explained with a sample session. calvin% djinn Welcome to Djinn version 2005-12-11. Type :h to get help. # Djinn is interactive if not given any arguments. # Let's see if it can find the identity function. Djinn> f ? a->a f :: a -> a f x1 = x1 # Yes, that was easy. Let's try some tuple munging. Djinn> sel ? ((a,b),(c,d)) -> (b,c) sel :: ((a, b), (c, d)) -> (b, c) sel ((_, v5), (v6, _)) = (v5, v6) # We can ask for the impossible, but then we get what we # deserve. Djinn> cast ? a->b -- cast cannot be realized. # OK, let's be bold and try some functions that are tricky to write: # return, bind, and callCC in the continuation monad Djinn> type C a = (a -> r) -> r Djinn> returnC ? a -> C a returnC :: a -> C a returnC x1 x2 = x2 x1 Djinn> bindC ? C a -> (a -> C b) -> C b bindC :: C a -> (a -> C b) -> C b bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17)) Djinn> callCC ? ((a -> C b) -> C a) -> C a callCC :: ((a -> C b) -> C a) -> C a callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11) # Well, poor Djinn has a sweaty brow after deducing the code # for callCC so we had better quit. Djinn> :q Bye. To play with Djinn do a darcs get http://darcs.augustsson.net/Darcs/Djinn or get http://darcs.augustsson.net/Darcs/Djinn/Djinn.tar.gz Then just type make. (You need a Haskell 98 implementation and some libraries.) And then start djinn. For the curious, Djinn uses a decision procedure for intuitionistic propositional calculus due to Roy Dyckhoff. It's a variation of Gentzen's LJ system. This means that (in theory) Djinn will always find a function if one exists, and if one doesn't exist Djinn will terminate telling you so. This is the very first version, so expect bugs. :) Share and enjoy. -- Lennart

8 13

ANN: scan-0.1.0.3, a Haskell style scanner
by Christian Maeder 03 Aug '10

03 Aug '10

Dear Haskell friends, I like to announce a Haskell style scanner at http://hackage.haskell.org/package/scan documented under http://projects.haskell.org/style-scanner/ It's best used in conjunction with hlint http://community.haskell.org/~ndm/hlint/ and gives many suggestions regarding the file format. Feedback is welcome. Thanks Christian (Discussions should only be posted to either haskell-cafe@ or beginners@)

1 2

Second draft of the Haskell 2010 report available
by Simon Marlow 06 Jul '10

06 Jul '10

The second draft of the Haskell 2010 report is now available in PDF and HTML formats (the PDF looks a lot nicer): http://www.haskell.org/~simonmar/haskell-2010-draft-report-2.pdf http://www.haskell.org/~simonmar/haskell-2010-draft-report-2/haskell.html relative to the first draft, which was only publicised on the haskell-prime mailing list, I have now updated the libraries too. Rather than update all the library documentation manually, I (perhaps rashly) decided to make a LaTeX backend for Haddock instead, and generate the report automatically from the library source code. Getting this to work turned out to be a lot more effort than I anticipated, but I think the results are quite attractive. Once the new Haddock backend is incorporated upstream, we'll finally have the ability to generate decent typeset API documentation. Furthermore, this should make it much easier to incorporate more libraries in future versions of the Haskell standard, should we decide to do so. Right now, the HTML version of the report is generated from the LaTeX sources, including the libraries. We could use the Haddock HTML output instead, but that would entail some difficulties with cross-references from the language part of the report to the libraries, which is why I've left it this way for now. This is why the libraries part of the report is bereft of hyperlinks in HTML; but at least it is well indexed in the PDF version. Summary of the library changes in Haskell 2010 relative to Haskell 98 and the FFI specification: * All libraries have been updated to their hierarchical names * The following library modules were dropped from the standard, due to being obsolete or superseded. Replacements are not part of the standard yet, but it is expected that they will be replaced in the future: Directory, System, Time, Locale, CPUTime, Random In the case of System, some functions have moved to the new modules System.Environment and System.Exit. * Foreign.Marshal.Error: functions on IOError moved to System.Error (this is where they've been in base for ever). * Data.List: added intercalate, subsequences, permutations, foldl', foldl1', stripPrefix (H2010 Data.List matches the current base version). * Data.Char: various additions of Unicode predicates (e.g. isLetter, isMark, isNumber), the GeneralCategory type and generalCategory. (matches the base version) * Control.Monad: added forM, forM_, (>=>), (<=<), forever, foldM_, replicateM, replicateM_ (matches the base version). * System.IO: added fixIO, hSetFileSize, hTell, hIsTerminalDevice, hSetEcho, hGetEcho, hShow. The base version has various additions: hGetBuf/hPutBuf, binary Handles, encodings, and newline support, but I erred on the side of being conservative here: these APIs need discussion, and in some cases are probably not suitable for the standard in their current state at all. * System.IO.Error: new module, providing functionality that was in Foreign.Marshal.Error in the FFI spec. * System.IO.Exit: new module, functionality moved from H98 System * System.Environment: new module, functionality moved from H98 System We expect to provide exactly these libraries in GHC 6.14, although the exact mechanism has yet to be decided; for discussion see http://www.haskell.org/pipermail/haskell-prime/2010-April/003158.html Comments on the draft report are welcome, before I finalise this and sign off on Haskell 2010. Cheers, Simon

2 1

ANNOUNCE: HaRe, the Haskell Refactorer 0.6
by Chris BROWN 28 Jun '10

28 Jun '10

Dear Haskellers, As part of our project on Refactoring Functional Programs http://www.cs.kent.ac.uk/projects/refactor-fp/ we are pleased to announce the availability of HaRe 0.6 (also known as HaRe 28/06/2010), a snapshot of our Haskell Refactorer prototype. Apart from bug-fixes, there are major changes since HaRe 0.5 and HaRe 0.4: A number of new refactorings have been added to HaRe. Some of these include: Adding and removing fields and constructors to data-type definitions, folding and unfolding against as-patterns, merging and splitting, converting between let and where constructs, introduce pattern matching, generative folding, and a clone detection and elimination tool. We have evolved the ongoing architecture of HaRe and derived an API (documented using Haddock) for program analysis and transformation. This allows HaRe to serve as a framework for end-users to build their own refactorings or just program transformations (or analyses). HaRe is available to download directly from here: http://www.cs.kent.ac.uk/projects/refactor-fp/hare/HaRe_28062010.tar.gz You can get HaRe 0.6 and the documentation about how to build your own refactorings via: http://www.cs.kent.ac.uk/projects/refactor-fp/hare.html Please see the README.txt for build/use instructions and known issues, and let us know about any problems, bugs, suggestions or additional platforms you can confirm as working. You will need: 1. ghc-6.12.1 2. hint-0.3.2.3 (available from cabal) 3. unix/gnu tools (or cygwin tools, if on windows) 4. vim or emacs (we've tested with gvim 6.2 and with emacs 21.4) 5. If you intend on running the test suite, HUnit-1.0. Happy Refactoring! The HaRe Team (Chris Brown, Huiqing Li, Simon Thompson) Project email: refactor-fp at kent.ac.uk<http://www.haskell.org/mailman/listinfo/haskell> Background: Refactoring is the process of changing the structure of programs without changing their functionality, i.e., refactorings are meaning-preserving program transformations that implement design changes. For more details about refactoring, about our project and for background on HaRe, see our project pages. HaRe - the Haskell Refactorer: HaRe is our prototype tool supporting a collection of refactorings for Haskell 98 (see README.txt for known issues and limitations). It is implemented as a separate refactoring engine (on top of Programatica's Haskell frontend and Strafunski's generic traversal strategy library), with small scripting frontends that call this engine from either Vim or Emacs. Currently supported refactorings: Introduce Pattern Match : place cursor over pattern variable Introduce Sub pattern : place cursor over pattern variable Introduce Case Expression : place cursor over pattern variable Generative Fold : highlight expression to fold. Must have equation in comment directly before definition of highlighted expression. Clone Analysis : select from menu Clone Extraction : highlight clone from the clone class to extract, follow step-by-step instructions. Converting Let to Where : place cursor at start of identifier whose definition is to be moved Converting Where to Let : place cursor at start of identifier whose definition is to be moved. create type signatures : select from menu remove redundant declarations : highlight definition to clean up add constructor to data type : place cursor at start of data type, you'll be prompted to add the new Constructor name, followed by any Type parameters as a complete string Split a tuple : place cursor at start of top level definition that returns a tuple. Slicing based on a subexpression : highlight sub-expression to extract. Instantiate a general pattern : select a function equation and enter the new instances for each pattern in the argument set. Extract an expression : highlight an expression within a definition Convert data type to newtype : place cursor at start of data type add definition to merge : place cursor at start of definition that is to be merged merge definitions : use "add definition for merge" for each definition to be merged. then choose merge definitions from menu. fold function definition : highlight function equation to fold against. fold constant definition : highlight constant equation to fold against. convert pattern to an as pattern : highlight pattern to convert. unfold references to as patterns : place cursor over as pattern name. remove field from a data type : place cursor at start of field to remove. add field to data type : place cursor over start of constructor. enter new field name. add debug information : add trace calls to function by placing cursor at the start of the function to trace rename : place cursor at start of identifier to be renamed, you'll be prompted for a new name Lift def to top level : place cursor at start of identifier whose definition is to be moved Lift def one level : place cursor at start of identifier whose definition is to be moved Demote : place cursor at start of identifier whose definition is to be moved Introduce new def : highlight expression to be named, you'll be prompted for a new name Unfold def : place cursor at start of identifier where its definition is to be unfolded Generalise def : place cursor at start of identifier where its definition is to be unfolded Remove def : place cursor at start of identifier whose definition is to be removed Duplicate def : place cursor at start of identifier whose definition is to be duplicated, you'll be prompted for a new name Add one parameter : place cursor at start of identifier whose definition is to be modified, you'll be prompted for a new name rm one parameter : place cursor in formal parameter which is to be removed Move def to another module : place cursor at start of the identifier whose definition is to be moved, you'll be prompted for the module name Clean imports : cursor position does not matter, just choose the command from the refactor menu Make import explicit : place cursor at the start of the module name in the import declaration Add to export : place cursor at start of the identifier which is to be added to the export Remove from export : place cursor at start of the entry to be removed in the export list From concrete to abstract data type: place cursor at start of the data type name Add field names : place cursor at start of the data type name Add discriminators : place cursor at start of the data type name Add constructors : place cursor at start of the data type name Eliminate nested patterns : place cursor at start of the data type name Eliminate patterns : place cursor at start of the data type name Create an ADT module : place cursor at start of the data type name Eliminate intermediate list: cursor position does not matter, just choose the command from the menu. Caveats (see also README.txt): Please keep in mind that this is a prototype, so we do not recommend to use it on your productions sources just yet. Just play with it to get an idea of tool-supported refactoring in Haskell, and send us your feedback and bug-reports. Our goal is to develop this into a tool that many of you will find indispensable for Haskell development. Regards, The HaRe team.

1 0

CfP ADAPT Summer School
by Ralf Laemmel 23 Jun '10

23 Jun '10

Dear Haskellers, this summer school contains bits of formal methods and language design that typically intersect very well with interests on this list. Looking forward to meet some of you in Koblenz. Ralf 8< - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - CALL FOR PARTICIPATION : ADAPT 2010 1st ADAPT Summer School September 26 - October 2, 2010, Koblenz, Germany http://adapt.uni-koblenz.de/summerschool2010 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Software adaptation is a topic that crosscuts much of software engineering, programming languages, information systems, formal methods, and other major areas of computer science. The CS department at the University of Koblenz-Landau engages in a research focus on software adaptation, and thereby connects scientists and teams in classical areas of computer science as much as application areas such as web-based systems, SOA, mobile systems, and robotics. ADAPT 2010 is the first edition in a series of summer schools on software adaptation. The program of ADAPT 2010 appeals to PhD students and possibly specialized Master's students in computer science. 8< - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

1 0

Call for Participation: SICSA Summer School on Formal Reasoning & Representation of Complex Systems
by Gudmund Grov 23 Jun '10

23 Jun '10

*** Apologies for multiple copies *** Call for Participation ----------------------- SSFRR 2010 SICSA Summer School on Formal Reasoning & Representation of Complex Systems 14-15 August 2010 -- Heriot-Watt University campus -- Edinburgh Satellite summer school of VSTTE 2010 http://dream.inf.ed.ac.uk/events/ssfrr-2010/ ---------------------- ABOUT --------- The summer school will give a broad overview of software verification techniques, addressing both bottom-up and top-down approaches with a strong focus on the formal representation and reasoning themes. The school consists of eight introductory lectures, each concentrating on an unique aspect of one or both of the overall themes. The topics of the lectures include inductive theorem proving; SAT and SMT solving; proof planning and rippling; rely/guarantee conditions; separation logic; operating system verification; process algebras and formal analysis of security. The school is intended for PhD students and researchers working within one or both of these themes, however familiarity with any of the techniques is not a prerequisite. All lectures are meant to be introductory. PRESENTERS --------- The following will present at the summer school: * Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University) * Alan Bundy & Lucas Dixon (University of Edinburgh) * Jane Hillston (University of Edinburgh) * Cliff Jones (University of Newcastle) * Gerwin Klein (National ICT Australia) * J Strother Moore (University of Texas at Austin) * Natarajan Shankar (SRI) * Graham Steel (INRIA) REGISTRATION --------- Registration is available from: http://www.macs.hw.ac.uk/vstte10_reg/Registration.php The registration fee is £110, which also covers materials and lunches. Accommodation at the Heriot-Watt campus (£42.50 per night incl. VAT and breakfast) can be including with your booking when you register. This is highly recommended since the summer school will coincide with several of the famous Edinburgh festivals -- where hotel prices in town tend to be very inflated. SICSA will cover registration and two nights campus accommodation for SICSA students (students from most Scottish Universities -- see http://www.sicsa.ac.uk/ to check if you are eligible). The number of SICSA students is limited, and a decision on ranking if this number is exceeded will only be taken if necessary. PRELIMINARY PROGRAM --------- The summer school has the following preliminary program (timing and titles may still change): Saturday: * 09:00: Registration * 09:30: J Moore -- Machines Reasoning about Machines - 39 Years and Counting * 11:00: Coffee break * 11:30: Gerwin Klein -- Specification and Refinement in Operating System Verification * 13:00: Lunch * 14:00: Bob Atkey/Ewen Maclean -- Amortised Resource Analysis and Functional Correctness with Separation Logic * 15:30: Coffee break * 16:00: Alan Bundy/Lucas Dixon -- Proof-planning, inductive reasoning, and beyond * 17:30: End Sunday: * 09:30: Natarajan Shankar -- Verification using SAT and SMT solvers * 11:00: Coffee break * 11:30: Graham Steel -- Formal Analysis of Key Management APIs * 13:00: Lunch * 14:00: Cliff Jones -- Tackling concurrency by reasoning explicitly about inference * 15:30: Coffee break * 16:00: Jane Hillston -- From Milner to Markov and Back: Stochastic process algebras and their equivalence relations * 17:30: End VENUE --------- The summer school is a satellite event of VSSTE 2010 (see http://www.macs.hw.ac.uk/vstte10/) and will be held the two days before the main event: Saturday 14th and Sunday 15th August 2010. Like VSTTE 2010, it will be held at the Edinburgh campus of Heriot-Watt University. ORGANISERS --------- The summer school is jointly organised by The School of Informatics at Edinburgh University and The School of Mathematical and Computer Sciences at Heriot-Watt University by: * Lucas Dixon (Edinburgh) * Gudmund Grov (Edinburgh) * Ewen Maclean (Heriot-Watt) CONTACT --------- The organisers can be contacted at the following email address: ssfrr-2010(a)inf.ed.ac.uk. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.

1 0

Announce: revamped free theorems generator
by Janis Voigtländer 23 Jun '10

23 Jun '10

The online free theorems generator, previously announced here: http://www.haskell.org/pipermail/haskell/2007-October/019917.html now runs at: http://www-ps.iai.uni-bonn.de/ft Thanks to Matthias Bartsch, there are now additional features in the online tool. In particular, one can declare one's own algebraic data types, type synonyms, type renamings, and type classes, and then generate free theorems for types involving those. Also, the tool now outputs inline graphics with nicely typeset theorems. (Plain text output, as well as .pdf and corresponding .tex, are still possible.) Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de

4 13

Re: [Haskell] Announce: revamped free theorems generator
by Janis Voigtländer 18 Jun '10

18 Jun '10

rossberg(a)mpi-sws.org schrieb: >> The online free theorems generator, previously announced here: >> >> http://www.haskell.org/pipermail/haskell/2007-October/019917.html >> >> now runs at: >> >> http://www-ps.iai.uni-bonn.de/ft > > I don't quite understand. Isn't that tool basically just giving you the > (unfolded) definition of logical relatedness at the type you enter? Although > pretty "free", that is not yet a "free theorem", at least not as I am used > to see this term used. For example, a free theorem for type a -> a would be > the property forall f :: a -> a, forall e, f e = e. I wouldn't say that statements of this form, completely determining the function definition from the function's type, are what it needs to qualify as a free theorem. For one thing, that's only possible for very simple types. For example, what would you say is a "not just unfolding the definition of the logical relation"-style free theorem for the type [a] -> [a]? For the type a -> a you mention, the generator gives the property forall f :: a -> a, forall g, forall x, g (f x) = f (g x). I wouldn't say that this is just unfolding the definition of logical relatedness. But maybe more interestingly, consider type (a -> Bool) -> [a] -> [a]. The generator answers: forall f :: (a -> Bool) -> [a] -> [a], forall g, forall p, forall q, (forall x, p x = q (g x)) => (forall y, map g (f p y) = f q (map g y)) I'd say that this *is* typically referred to as the free theorem corresponding to filter's type, namely that the property map g . filter (q . g) = filter q . map g holds for all like-wise typed functions. In any case, I would be very interested in learning more about for what and where you are used to see the term "free theorems" used, as I am always interested in new applications of parametricity. I can just say that myself I am very used to calling statements like the one about filter above "free theorems". Ciao, Janis. -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:jv@iai.uni-bonn.de

1 0

Fully-funded PhD in programming languages at Oxford
by Jeremy.Gibbons＠comlab.ox.ac.uk 17 Jun '10

17 Jun '10

FULLY-FUNDED DOCTORAL STUDENTSHIP IN PROGRAMMING LANGUAGES AT OXFORD I have just obtained funding for a DPhil studentship at Oxford. The studentship is open in terms of topic; I would welcome applications for research in any of my areas of interest. These include: functional programming generic programming dependent types design patterns model-driven development For more information about topics, please visit my web page http://web.comlab.ox.ac.uk/people/Jeremy.Gibbons/ or discuss with me. The successful candidate will have a good bachelor's or master's degree in CS, and a strong background in the principles of programming languages. The funding covers stipend, fees (at the home/EU rate), equipment, and travel, and is for three and a half years from October 2010 (or as soon as possible after that). Please do contact me with any questions, and in any case before applying. Please also pass this note on to anyone who might be interested. Jeremy.Gibbons(a)comlab.ox.ac.uk, Deputy Director Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 283531 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html

1 0