- Haskell - Haskell.org

recursive definitions in Haskell (inductive and coinductive)
by Graham Hutton 06 Feb '10

06 Feb '10

> Is this the right story? One of my difficulties is that I'm having > trouble grasping what coinduction might mean for terms. The following tutorial paper may be helpful: http://www.cs.nott.ac.uk/~gmh/corecursion.pdf Best wishes, Graham +-----------------------------------------------------------------+ | Dr Graham Hutton Email : gmh(a)cs.nott.ac.uk | | Functional Programming Lab | | School of Computer Science Web : www.cs.nott.ac.uk/~gmh | | University of Nottingham | | Jubilee Campus, Wollaton Road Phone : +44 (0)115 951 4220 | | Nottingham NG8 1BB, UK | +-----------------------------------------------------------------+

1 0

recursive definitions in Haskell (inductive and coinductive)
by nr＠cs.tufts.edu 03 Feb '10

03 Feb '10

I'd appreciate a word from the experts to see if my understanding of recursive definitions in Haskell is correct---I would hate to be telling my students pernicious lies. Haskell permits recursive definitions at both the type level and the term level. Here's an example definition at the type level: data Intlist = Nil | Cons Integer Intlist If my understanding is correct, Haskell takes as the definition of `Intlist` the *greatest* solution to this recursion equation. That is, in a vaguely domain-theoretic way, Intlist is the greatest fixed point of the function f(S) = {Nil} union {Cons n ns | n in Integer, ns in S} It's this 'greatest fixed point' or coinductive definition that admits of infinite lists in the `Intlist` type. Right? Contrast this situation with recursion at the term level. Suppose I define evens :: Intlist evens = 0 `Cons` intmap (2+) evens where intmap f Nil = Nil intmap f (Cons n ns) = Cons (f n) (intmap f ns) Here the solution to the recursion equation is totally different---at the term level, the definition of `evens` is taken to mean the *least* fixed point of the function \e -> 0 `Cons` intmap (2+) e. In this case its not obvious that there's any difference, but if we consider strange :: Intlist strange = intmap (2*) strange then Haskell is very definitely going to make `strange` the least defined solution to this equation, which means `undefined` and not, for example, `Nil` or `Cons 0 Nil`, both of which also solve the recursion equation. Is this the right story? One of my difficulties is that I'm having trouble grasping what coinduction might mean for terms. For types/sets/domains, I've found Andy Gordon's very nice tutorial at http://research.microsoft.com/en-us/um/people/adg/publications/fp94.ps But I'm not sure what a greatest solution to an equation involving values might be, or even if such a thing exists (aside from adding an arbitrary top element to form a lattice of values, which seems most unsatisfying). Comments, corrections, and cues about good papers are all cheerfully solicited! Norman

5 5

2nd CfP: LOPSTR 2010
by Temur Kutsia 01 Feb '10

01 Feb '10

========================================================================= Call for papers 20th International Symposium on Logic-Based Program Synthesis and Transformation LOPSTR 2010 http://www.risc.uni-linz.ac.at/conferences/lopstr2010/ Hagenberg, Austria, July 23-25, 2010 (co-located with PPDP 2010) ========================================================================= Objectives: The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium, so authors can incorporate the feedback in the published papers. The 20th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2010) will be held in Hagenberg, Austria; previous symposia were held in Coimbra, Valencia, Lyngby, Venice, London, Verona, Uppsala, Madrid, Paphos, London, Venice, Manchester, Leuven, Stockholm, Arnhem, Pisa, Louvain-la-Neuve, and Manchester. LOPSTR 2010 will be co- located with PPDP 2010 (12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming). Topics: Topics of interest cover all aspects of logic-based program development, all stages of the software life cycle, and issues of both programming-in- the-small and programming-in-the-large. Papers describing applications in these areas are especially welcome. Contributions are welcome on all aspects of logic-based program development, including, but not limited to: specification synthesis verification transformation analysis optimisation specialization inversion composition program/model manipulation certification security transformational techniques in SE applications and tools Survey papers that present some aspect of the above topics from a new perspective. Application papers, that describe experience with industrial applications, are also welcome. Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. Work that already appeared in unpublished or informally published workshops proceedings may be submitted. Following past editions, publication of the formal post-conference proceedings in the Springer series Lecture Notes in Computer Science (LNCS) is envisaged. IMPORTANT DATES AND SUBMISSION GUIDELINES: Paper/extended abstract submission: March 25, 2010 Notification (for pre-proceedings): May 15, 2010 Camera-ready (for pre-proceedings): June 15, 2010 Symposium: July 23-25, 2010 Submissions can either be (short) extended abstracts or (full) papers whose length should not exceed 9 and 15 pages, respectively. Submissions must be formatted in the Springer LNCS style (excluding well-marked appendices not intended for publication). Referees are not required to read the appendices, and thus papers should be intelligible without them. Short papers may describe work-in-progress or tool demonstrations. Both short and full papers can be accepted for presentation at the symposium and will then appear in the LOPSTR 2010 pre-proceedings. Full papers can also be immediately accepted for publication in the formal proceedings published by Springer-Verlag in the LNCS series. In addition, after the symposium, the programme committee will select further short or full papers presented in LOPSTR 2010 to be considered for formal publication. These authors will be invited to revise and/or extend their submissions in the light of the feedback solicited at the symposium. Then after another round of reviewing, these revised papers can also be published in the formal post-proceedings. Papers should be submitted electronically via the submission page http://www.easychair.org/conferences/?conf=lopstr2010 They should be in PDF format and interpretable by Acrobat Reader. Invited Speakers: Bruno Buchberger RISC, Johannes Kepler University Linz, Austria Olivier Danvy University of Aarhus, Denmark Johann Schumann RIACS/NASA Ames Research Center, USA Program Committee: Maria Alpuente Tech. University of Valencia (Chair), Spain Sergio Antoy Portland State University, USA Gilles Barthe IMDEA Software, Madrid Manuel Carro Tech. University of Madrid, Spain Marco Comini University of Udine, Italy Danny De Schreye K.U.Leuven, Belgium Santiago Escobar Tech. University of Valencia, Spain Moreno Falaschi University of Siena, Italy Fabio Fioravanti University of Chieti - Pescara, Italy John Gallagher Roskilde University, Denmark Michael Hanus University of Kiel, Germany Patricia M Hill University of Parma, Italy Andy King University of Kent, UK Temur Kutsia Johannes Kepler University Linz, Austria Ralf L�mmel Universit�t Koblenz-Landau, Germany Michael Leuschel University of Southampton, UK Yanhong Annie Liu State University of New York at Stony Brook, USA Julio Mari�o Tech. University of Madrid, Spain Ricardo Pe�a University Complutense of Madrid, Spain Peter Schneider-Kamp University of Southern Denmark Alicia Villanueva Tech. University of Valencia, Spain Contacts Program Chair Maria Alpuente DSIC - Technical University of Valencia Camino de Vera s/n Apdo. 22.012 E-46022 Valencia (Spain) Email: alpuente(a)dsic.upv.es Conference Chair Temur Kutsia Research Institute for Symbolic Computation Johannes Kepler University Linz Altenbergerstrasse 69 A-4040 Linz, Austria Email: kutsia(a)risc.uni-linz.ac.at

1 0

PAR 2010: First CFP
by Koen Claessen 01 Feb '10

01 Feb '10

(I am sending this on behalf of a colleague) [Papers dealing with partiality and termination using monadic programming or other functional programming techniques are welcome] Please distribute to those you might think are interested. ======================================================================== 1st Call for Papers PAR 2010 Workshop on Partiality And Recursion in Interactive Theorem Provers Edinburgh, UK, 15 July 2010 (satellite workshop of ITP'10) a mid-FLoC 2010 workshop <http://www.cs.st-andrews.ac.uk/~ek/PAR-10/> ======================================================================== PAR'10 workshop is a venue for researchers working on new approaches to cope with partial functions and terminating general (co)recursion in theorem provers. Theorem provers with inductive types provide a restricted programming language together with a formal meta-theory for reasoning about the language. When propositions are represented as types and proofs as programs, non-terminating proofs are disallowed for consistency and decidability of type checking. As a result, there is no trivial way to represent partial functions, and termination is syntactically ensured by imposing that the recursive calls must be made on structurally smaller arguments. Similar issues exist for productivity of functions on infinite objects where syntactic methods are used to ensure an infinite flow of data. The workshop aims to address these issues and various approaches for dealing with them. We invite submissions on all aspects of partiality and termination of general (co)recursive functions in a logical framework. The topics of this workshop include but are not limited to: * partial functions and functions over partial objects in theorem provers; * specialised type systems for general (co)recursion; * syntactical tests to guarantee termination of general recursive functions; * syntactical tests to guarantee productivity of functions on infinite objects; * methods to ensure termination of special classes of recursion definitions, eg nested recursion, simultaneous inductive-recursive data types and functions; * semantic approaches to termination and productivity, eg based on domain theory and topology; * categorical approaches to termination and productivity; * algebra of programming with partial functions and general (co)recursion. Description of software tools and case studies for dealing with the issues in the scope of the workshop are welcome. Submissions ----------- The articles will be evaluated by the PC for publication in the proceedings of the workshop. The final proceedings will be published after the workshop as a special issue of EPTCS and a preliminary version will be available during the workshop. The articles must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Submissions should preferably not exceed 16 pages (excluding bibliography). Submissions must be prepared in LaTeX using the EPTCS macro package <http://style.eptcs.org/>. The web-based system EasyChair will be used for submission (<http://www.easychair.org/conferences/?conf=par10>). Important dates --------------- * 29 March 2010: Submission deadline * 29 April 2010: Notification of acceptance * 24 May 2010: Final version of accepted papers * 15 July 2010: the workshop Invited Speakers ---------------- * Conor McBride (University of Strathclyde) * TBA Programme Committee ------------------- Andreas Abel (Ludwig Maximilians University Munich, D) Yves Bertot (INRIA Sophia-Antipolis, FR) Ana Bove (Chalmers University of Technology, SE) Ekaterina Komendantskaya (University of St Andrews, UK) Ralph Matthes (IRIT Toulouse, FR) Milad Niqui (CWI, NL) Anton Setzer (Swansea University, UK) Organisers ---------- Ana Bove Ekaterina Komendantskaya Milad Niqui

1 0

HWN Issue 148 -- unicode error
by Joe Fredette 31 Jan '10

31 Jan '10

Indeed, the Unicode only made it through my system, and not the mailer itself. In fact, the name should look something like "Ćwikłowski", and not the garbled mess that made it through. Apologies again, Bartek! /Joe

1 0

Haskell Weekly News: Issue 148 - January 31, 2010
by jfredett＠gmail.com 31 Jan '10

31 Jan '10

--------------------------------------------------------------------------- Haskell Weekly News http://sequence.complete.org/hwn/20100131 Issue 148 - January 31, 2010 --------------------------------------------------------------------------- Welcome to issue 148 of HWN, a newsletter covering developments in the [1]Haskell community. Hello Haskellers, this week begins with a correction. Last week, I noted a blogpost from one 'Bartek Paczesiowa', I was rapidly informed of the complete wrongness of this citation. In fact, Bartek's last name is, and I hope the Unicode makes it through here, 'wikowsk,' and Paczesiowa is his nickname. Apologies to Bartek, as penance I've reread your [2]excellent post on your blog. That said, this week's HWN if packed full of awesome potential naming errors, so I'll let you get to it. Thus, Haskellers, Your Haskell Weekly News! Announcements haskell-src-exts-1.8.0. Niklas Broberg [3]announced a new release of haskell-src-exts. Elerea 1.2.3 with some enhancements. Patai Gergely [4]announced his addition of some new features to the experimental branch of his FRP library, Elerea. hakyll-1.3. Jasper Van der Jeugt [5]announced the release of hakyll 1.3, including several new improvments and changes. ThreadScope 0.1. Satnam Singh [6]announced the release of Threadscope 0.1, the premier graphical thread profiler. The Monad.Reader Issue 15. Brent Yorgey [7]announced the most recent issue of the Monad.Reader, a monthly publication of Haskell Related expostition and discusson articles. afv-0.1.0. Tom Hawkins [8]announced a afv-0.1.0, an infinite state model checker for verifying assertions about embedded C programs. adaptive-tuple 0.1.0. John Lato [9]announced the initial release of adaptive-tuple, his library for combining the space-efficient properties of tuples with the utility of lists. Job opportunities at Citrix Systems (Cambridge, UK). Matthias Goergens [10]announced a opportunity available at Citrix Systems in Cambridge, UK. Discussion OT: Literature on translation of lambda calculus to combinators. Dusan Kolar [11]asked about texts regarding translating the untyped lambda calculus to a combinator calculus such as SKI or BCKW. Linguistic hair-splitting. Andrew Coppin [12]asked an interesting offtopic linguistic question about what we call a number, a field, an element, and a monad. Adopting hpodder? John Goerzen [13]asked if there were any interested adoptive maintainers for his hpodder project. This is an excellent opportunity for a Haskell Neophyte to help the community and learn about project management hopefully we can find hpodder a new maintainer! Blog noise [14]Haskell news from the [15]blogosphere. Blog posts from people new to the Haskell community are marked with >>>, be sure to welcome them! * Holumbus: [16]HolHac at FH-Wedel. * ++Arch Haskell Team++: [17]Arch Linux updates to GHC 6.12. * Neil Brown: [18]Exploring a Communicating Sequential Processes EDSL. * The GHC Team: [19]Yielding more improvements in parallel performance. Quotes of the Week * Berengal: I'm going to write a module Hmm with a (.) operator in it, so I can go 'Hmm..' in my code * clarkb,: in CS they dont teach you to program...You learn Data Structures, Algorithms, Logic, Discrete Math, Language theory, etc and happen to pick up programming on the way * dons: hey i love core. i dream about unboxes * cale: Differential geometry is the study of manifolds under change of notation. * kmc: the irony being, the abstraction that gets the most complaining and general noise [from imperative programmers] is the one that captures imperative programming * kmc: i am Jack's monad operator * arw: ...and a basic law of haskell is, 50% of all documentation has to be monad tutorials :) * Cale: Here [#haskell], we feed trolls until they explode. * bartek: It took me 2 years of studying teachings of Oleg Kiselyov (who was raised among types, where he learned to speak their language), but finally, I have the solution. * kmc: I think 250 milliolegs is enough to kill an elephant olsner: ... to kill an elephant - in the type system! * syntaxglitch: every time I have a cool idea about something that might work in Haskell, I go check Oleg's stuff and find that 1) he already did it 2) thought it out better 3) did it incidentally while working on something way more interesting * DRMacIver:: I dread to think what category theory would look like after the software engineering world had got their grubby paws on it. Enterprise variant functors. Commutative UML diagrams. About the Haskell Weekly News New editions are posted to [20]the Haskell mailing list as well as to [21]the Haskell Sequence and [22]Planet Haskell. [23]RSS is also available, and headlines appear on [24]haskell.org. To help create new editions of this newsletter, please see the information on [25]how to contribute. Send stories to jfredett . at . gmail . dot . com. The darcs repository is available at darcs get [26]http://patch-tag.com/r/jfredett/HWN2/pullrepo HWN2 . References 1. http://haskell.org/ 2. http://paczesiowa.blogspot.com/2010/01/pure-extensible-exceptions-and-self.… 3. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69749 4. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69745 5. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69731 6. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69612 7. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69535 8. http://article.gmane.org/gmane.comp.lang.haskell.cafe/69517 9. http://article.gmane.org/gmane.comp.lang.haskell.general/17764 10. http://article.gmane.org/gmane.comp.lang.haskell.general/17763 11. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/69643 12. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/69620 13. http://thread.gmane.org/gmane.comp.lang.haskell.cafe/69528 14. http://planet.haskell.org/ 15. http://haskell.org/haskellwiki/Blog_articles 16. http://holumbus.fh-wedel.de/blog/?p=32 17. http://archhaskell.wordpress.com/2010/01/31/arch-linux-updates-to-ghc-6-12/ 18. http://chplib.wordpress.com/2010/01/27/exploring-a-communicating-sequential… 19. http://ghcmutterings.wordpress.com/2010/01/25/yielding-more-improvements-in… 20. http://www.haskell.org/mailman/listinfo/haskell 21. http://sequence.complete.org/ 22. http://planet.haskell.org/ 23. http://sequence.complete.org/node/feed 24. http://haskell.org/ 25. http://haskell.org/haskellwiki/HWN 26. http://patch-tag.com/r/jfredett/HWN2/pullrepo%20HWN2

1 0

ANN: haskell-src-exts-1.8.0
by Niklas Broberg 31 Jan '10

31 Jan '10

Fellow Haskelleers, I'm pleased to announce the release of haskell-src-exts-1.8.0! * On hackage: http://hackage.haskell.org/package/haskell-src-exts * Via cabal: cabal install haskell-src-exts * Darcs repo: http://code.haskell.org/haskell-src-exts For users of hsx, the latest version 0.6.1 works unchanged with this release. 1.7.2 --> 1.8.0 =============== * Add an instance Show Fixity (derived). * Support for the new ANN and INLINE_CONLIKE pragmas. * Remove support for CFILES and INCLUDE pragmas. The support wasn't correct anyway, as it assumed the pragmas appeared at the top of files. As CFILES/INCLUDE pragmas can (and do) appear anywhere, there's no hope to support them in the AST. Better to remove the support altogether. Files with CFILES/INCLUDE pragmas can still be parsed of course, but those pragmas will be handled as comments. * Parsing with ignoreLinePragmas = False now correctly updates the file name. * Allow the whole SPECIALISE/INLINE family of pragmas in instance declarations. The InsInline constructor is removed, and is now represented by 'InsDecl (InlineSig ...)'. * Fix a bug with line numbering and quasi quotes, and a similar one with line numbering and CDATA. * Fix a few minor bugs in the exactPrinter. * Fix the strange handling of so called strings in LINE pragmas. Cheers, /Niklas

1 1

Announce: adaptive-tuple 0.1.0
by John Lato 27 Jan '10

27 Jan '10

Hello, I am pleased to announce the initial release of adaptive-tuple, a library that aims to combine the variable-length convenience of lists with the smaller space requirements of tuples. Using the AdaptiveTuple class, computations can be constructed in a manner very similar to the ZipList Applicative instance. The final computation is passed to a reification function with an initial input to generate an output. adaptive-tuple is similar in conception to adaptive-containers. Where adaptive-containers uses specialized data types based upon the type of the elements, adaptive-tuple uses specialized containers based upon the number of elements. Using adaptive-tuple is similar to using a type-sized vector library such as parameterized-data, but with much lower runtime space requirements. Adaptive tuples are designed to be used when a very large number of small variable-sized containers are needed and using lists degrades performance. Available on hackage at http://hackage.haskell.org/package/adaptive-tuple. Comments, patches, and bug reports are welcome. In addition to Don Stewart, Alfonso Acosta, and others responsible for the type-level and adaptive-containers libraries, this package would not have been possible with Bulat Ziganshin's excellent Template Haskell tutorials. Cheers, John

1 0

Job opportunities at Citrix Systems (Cambridge, UK)
by Matthias Görgens 26 Jan '10

26 Jan '10

Hi folks, I just posted this job advert on the Haskell Cafe mailing list --- and someone suggested I crosspost here, too. Please pardon me if this double posting is too spammy. I have recently started working for Citrix in Cambridge. We are working on the open source software in Ocaml. Admittedly Ocaml is only a second best compared to Haskell ;o) and I hope my post does not count as too off-topic here. But Ocaml is still a decent language. My experience was primarily with Haskell and I only started working with Ocaml in earnest at Citrix. (So I hope that showing a way to transplant Haskell skills to the real world --- via the roundabout route of Ocaml --- justifies my posting.) So --- if you are looking for a job in Cambridge that involves functional programming, free software [1] and free beer [2], please feel free to drop me a line. I have included our original advert to the Ocaml mailing list for those who want more information first. Cheers, Matthias. [1] As in free speech. LGPL [2] As in free beer. We also get other perks, like snacks and a pool table. ---------- Forwarded message ---------- From: Dave Scott <Dave.Scott(a)eu.citrix.com> Date: 2010/1/18 Subject: [Caml-list] [jobs] Citrix Systems (Cambridge, UK) To: "caml-list(a)yquem.inria.fr" <caml-list(a)yquem.inria.fr>, "ocaml-jobs(a)inria.fr" <ocaml-jobs(a)inria.fr> Dear fellow OCaml users, Summary: We (Citrix Systems) are looking for OCaml programmers to join our team in Cambridge, UK. We use OCaml extensively in the "xapi tool-stack": the control-plane used in the Xen Cloud Platform[1] on which the widely used XenServer server virtualisation product[2] is based. XCP aims to provide a complete open-source cloud infrastructure platform with a powerful management stack based on standards-based APIs, support for multi-tenancy, SLA guarantees and detailed metrics for consumption based charging. We are looking to recruit top-class engineers to work on the tool-stack; applicants must have a good knowledge of data structures and algorithms, experience of programming in the context of large systems and general aesthetic good taste when it comes to code and architecture. Our code base is significant and varied: over 130,000 lines of OCaml, solving problems ranging from the low-level (Xen hypercalls) to the high-level (resource pool management), to the compiler-driven (generating language bindings for our Xen datamodel). Our ideal candidate will have: * significant experience of applications programming in high-level languages (such as OCaml :-) * an aptitude for implementing (and reasoning about) complex concurrent, distributed systems * the skills required to contribute to both the architectural design and day-to-day development of a large code-base * strong communication skills and problem solving ability * a determination to deliver great products that perform brilliantly and meet our customers' needs So if you want to tackle interesting and challenging programming problems and contribute to an innovative, fast-growing product that is already used by tens of thousands of customers across the world, please don't hesitate to send me your CV. [1] http://www.xen.org/products/cloudxen.html [2] http://www.citrix.com/English/ps2/products/feature.asp?contentID=1686939 Thanks, -- Dave Scott <dave.scott(a)eu.citrix.com>

1 0

ANN: The Monad.Reader Issue 15
by Brent Yorgey 26 Jan '10

26 Jan '10

I am very pleased to announce that Issue 15 of The Monad.Reader is now available for your reading pleasure [1]. Issue 15 consists of the following four articles: * "The hp2any project" by Gergely Patai * "Adventures in Three Monads" by Edward Z. Yang * "The Operational Monad Tutorial" by Heinrich Apfelmus * "Implementing STM in pure Haskell" by Andrew Coppin Feel free to browse the source files. You can check out the entire repository using darcs: darcs get http://code.haskell.org/~byorgey/TMR/Issue15 If you'd like to write something for Issue 16, please get in touch. The deadline will likely be sometime in mid-late April; more details will be forthcoming. -Brent [1] http://themonadreader.files.wordpress.com/2010/01/issue15.pdf

1 0