[Haskell] Postdoctoral Research Assistant position at University of Edinburgh
The School of Informatics, University of Edinburgh invites applications for a postdoctoral research assistant on the SAGE project (Scoped and Gradual Effects), funded by Huawei. The post will be for eighteen months. We seek applicants at an international level of excellence. The School of Informatics at Edinburgh is among the strongest in the world, and Edinburgh is known as a cultural centre providing a high quality of life. If interested, please contact Prof. Philip Wadler . Full details are here <https://elxw.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_1001/job/2929/?utm_medium=jobshare>. Applications close at 5pm on 14 January 2021. The Opportunity: In the early 2000s, Plotkin and Power introduced an approach to computational effects in programming languages known as *algebraic effects*. This approach has attracted a great deal of interest and further development, including the introduction by Plotkin and Pretnar of *effect handlers*. Several research languages, such as Eff, Frank, Koka, and Links, support the use of algebraic effects. A few languages, including Multicore O'Caml and WebAssembly, support specific algebraic effects, and we may see general algebraic effects make their way into mainstream languages in the future. The proposed research has two focusses: (a) a simpler version of static scoping for algebraic effect handlers, and (b) gradual types for algebraic effect systems. The former is a question of how to match an effect with its corresponding handler. This issue arises when two effects have the same name, and you expect the handler for one but invoke the handler for the other. Some current solutions, like tunnelling and instance variables, are based on lexical scoping. However, despite this insight, tunnelling and instance variables are more complex than lexical binding of a variable to a value. In particular, the type system needs to track that an effect does not escape the scope of its surrounding handler (reminiscent of the funarg problem with dynamic variable binding). Can we do better? The latter is a question of how to integrate legacy code that lacks typed effects with new code that supports typed effects. Usually, integration of dynamically and statically typed languages is best explored in the context of gradual types, which support running legacy code and new code in tandem. To date there is only a tiny amount of work in the area of gradual types for effects, and important aspects of algebraic effects, such as effect handlers, have yet to be addressed. Overall, work to date on effect handlers is often complex, and attention is required to where ideas can be simplified, which is the ultimate objective of this project. Your skills and attributes for success: Essential • PhD (or close to completion) in programming languages or a related discipline. • Expertise and experience in relevant areas, including lambda calculus, type systems, and compilation. • Ability to implement prototype language processors in O’Caml, Haskell, or a related language. • Excellence in written and oral communication, analytical, and time management skills. • Ability to collaborate with a team. Desirable • Published research in programming languages or a related field, preferably in top-tier conferences. • Experience in presenting at conferences or seminars. • Knowledge of effect systems or gradual type systems. • Experience with a proof assistant, such as Agda or Coq. • Strong programming and software engineering skills. . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
Re: [Haskell] Haskell tutors required!
Yes, you've located last year's syllabus! Go well, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ On Tue, 8 Sep 2020 at 21:20, Howard B. Golden wrote: > Hi, I am intrigued by the opportunity, but I wonder if I am up to the > task. To help me decide, I have this question: Is the syllabus for the > course similar to the most recent presentation ( > https://www.learn.ed.ac.uk/webapps/blackboard/content/listContent.jsp?course_id=_73477_1_id=_3873901_1 > )? > > Best regards, > Howard > The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
[Haskell] Haskell tutors required!
Edinburgh is one of a few places in the world that teaches functional programming to first-year students, specifically Haskell. This year, our Haskell course for first-year's will be delivered remotely. Last year's class was 400 students, this year we expect more. In the past we've had trouble locating enough high-quality tutors. The unique situation offers us a new possibility: recruit tutors from elsewhere. Please get in touch if: (a) You might yourself be interested. (b) You know of folk who might be interested or could forward an announcement to a suitable mailing list. Informatics 1 - Introduction to Computation (INF1A/FP) Role: Tutor Description: Tutors required from week 1 to week 11 (Monday 21 September -- Friday 4 December) to assist in weekly one-hour ten-person tutorial sessions to review and mark solutions to exercises prepared by students in advance of the tutorial, to facilitate group work, and to answer questions about the material covered in the course. Tutors will be paid for 3 hours/week: 1 for preparation, 1 for marking, and 1 for the online tutorial session (£15.52/hour * 3 hours * 11 weeks). In the past, we have had trouble recruiting a sufficient number of capable tutors. This year, we will take advantage of remote delivery to recruit tutors from both within and without Edinburgh. Tutorials are expected to be on Thursdays and Fridays each week. Wadler will monitor tutorials, and expects to be in a position to write letters of recommendation after the course, if required. Skills: Good knowledge of functional programming, preferably in Haskell, and of basic finite state machines and propositional logic; such as might be had by a 3rd or 4th year undergraduate or a postgraduate student. Ability to communicate enthusiasm for the subject and encourage students new to university to engage in and contribute to tutorials. Tutors need to supply appropriate encouragement and support for all students, from those who are struggling to those who are coping easily and want to learn more. To apply: Send email to wad...@inf.ed.ac.uk. Include one paragraph on your background and why you would do a good job teaching the course. Please include any relevant documentation, such as a copy of your transcript. I look forward to hearing from you! Go well, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
[Haskell] Haskell, Then and Now. Got Questions? Ask them here!
IOHK Cardano Virtual Summit continues. Today's sessions include: *16.00 (UK time) Fri 3 Jul* *Haskell, then and now: What is the future for **functional programming languages?* Prof Simon Peyton-Jones, Prof John Hughes, Prof Philip Wadler, Dr Kevin Hammond, Dr Duncan Coutts. You can submit questions via Reddit <https://www.reddit.com/r/cardano/comments/hkf5ki/got_questions_for_the_summit_session_on_haskell/>. Register for the summit here <https://cardanosummit.iohk.io/>. You can log in with your registered username and password here <https://www.ubivent.com/start/cardanovirtualsummit>. See you there! Go well, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
[Haskell] Cardano Virtual Summit 2020
Cardano Virtual Summit 2020 takes place today and tomorrow. Some talks that may be of interest: *16.00 Thu 2 Jul* *An overview of IOHK research* Prof Aggelos Kiayias, Prof Elias Koutsoupias, Prof Alexander Russell, Prof Phil Wadler. *18.30 Thu 2 Jul* *Architecting the internet: what I would have done * *differently... *Vint Cerf, Internet pioneer and Google internet evangelist, Prof Aggelos Kiayias, panel moderated by Prof Philip Wadler. *20.00 Thu 2 Jul* *Functional smart contracts on Cardano* Prof Philip Wadler, Dr Manuel Chakravarty, Prof Simon Thompson. *16.00 Fri 3 Jul* *Haskell, then and now: What is the future for **functional programming languages?* Prof Simon Peyton-Jones, Prof John Hughes, Prof Philip Wadler, Dr Kevin Hammond, Dr Duncan Coutts. You need register in advance. You can do so here: https://cardanosummit.iohk.io/ . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
[Haskell] Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy Systems in Edinburgh LFCS
Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy Systems in Edinburgh LFCS https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobspec?p_id=050700 The University of Edinburgh seeks to appoint a Lecturer/Senior Lecturer/Reader in Programming Languages for Trustworthy Systems. An ideal candidate will be able to contribute and complement the expertise of the Programming Languages & Foundations Group which is part of the Laboratory for Foundations of Computer Science (LFCS). The successful candidate will have a PhD, an established research agenda and the enthusiasm and ability to undertake original research, to lead a research group, and to engage with teaching and academic supervision, with expertise in at least one of the following: - Practical systems verification: e.g. for operating systems, databases, compilers, distributed systems - Language-based verification: static analysis, verified systems / smart contract programming, types, SAT/SMT solving - Engineering trustworthy software: automated/property-based testing, bug finding, dynamic instrumentation, runtime verification We are seeking current and future leaders in the field. Applications from individuals from underrepresented groups in Computer Science are encouraged. Appointment will be full-time and open-ended. The post is situated in the Laboratory for Foundations of Computer Science, the Institute in which the School's expertise in functional programming, logic and semantics, and theoretical computer science is concentrated. Collaboration relating to PL across the School is encouraged and supported by the School's Programming Languages Research Programme, to which the successful applicant will be encouraged to contribute. Applicants whose PL-related research aligns well with particular strengths of the School, such as machine learning, AI, robotics, compilers, systems, and security, are encouraged to apply and highlight these areas of alignment. All applications must contain the following supporting documents: • Teaching statement outlining teaching philosophy, interests and plans • Research statement outlining the candidate’s research vision and future plans • Full CV (resume) and publication list The University job posting and submission site, including detailed application instructions, is at this link: https://www.vacancies.ed.ac.uk/pls/corehrrecruit/erq_jobspec_version_4.jobspec?p_id=050700 Applications close at 5pm GMT on January 31, 2020. This deadline is firm, so applicants are exhorted to begin their applications in advance. Shortlisting for this post is due early February with interview dates for this post expected to fall in early April 2020. Feedback will only be provided to interviewed candidates. References will be sought for all shortlisted candidates. Please indicate on your application form if you are happy for your referees to be contacted. Informal enquiries may be addressed to Prof Philip Wadler ( wad...@inf.ed.ac.uk). Lecturer Grade: UE08 (£41,526 - £49,553) Senior Lecturer or Reader Grade: UE09 (£52,559 - £59,135) The School is advertising a number of positions, including this one, as described here: https://www.ed.ac.uk/informatics/about/work-with-us/vacancies/academic-recruitment About the Laboratory for Foundations of Computer Science As one of the largest Institutes in the School of Informatics, and one of the largest theory research groups in the world, the Laboratory for Foundations of Computer Science combines expertise in all aspects of theoretical computer science, including algorithms and complexity, cryptography, database theory, logic and semantics, and quantum computing. The Programming Languages and Foundations group includes over 25 students, researchers and academic staff, working on functional programming, types, verification, semantics, software engineering, language-based security and new programming models. Past contributions to programming languages research originating at LFCS include Standard ML, the Edinburgh Logical Framework, models of concurrency such as the pi-calculus, and foundational semantic models of effects in programming languages, based on monads and more recently algebraic effects and handlers. About the School of Informatics and University of Edinburgh The School of Informatics at the University of Edinburgh is one of the largest in Europe, with more than 120 academic staff and a total of over 500 post-doctoral researchers, research students and support staff. Informatics at Edinburgh rated highest on Research Power in the most recent Research Excellence Framework. The School has strong links with industry, with dedicated business incubator space and well-established enterprise and business development programmes. The School of Informatics has recently established the Bayes Centre for Data Technology, which provide a locus for fruitful multi-disciplinary work, including a range of compa
[Haskell] University of Edinburgh Chancellor's Fellowships
Dear All, The University of Edinburgh is offering a variety of Chancellor's Fellowships. These are essentially lectureships with an initial fellowship period of five years. Some fellowships may be in Programming Languages as part of the Digital Technologies area, and suitable candidates are strongly encouraged to apply. The deadline is March 12th, please see: https://www.ed.ac.uk/informatics/about/work-with-us/vacancies/chancellor-fellowship-digital-technologies for further information. Feel free to contact me if you have questions. Yours, -- P . \ Philip Wadler, Professor of Theoretical Computer Science, . /\ School of Informatics, University of Edinburgh . / \ and Senior Research Fellow, IOHK . http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
Re: Two Proposals
Yes... not quite so well with the “by” variants. What would we say? then group initsBy by x This problem occurs independent of group, does it not? then sortBy by x The solution is to rename sort -- sortByDefault sortBy -- sort but that's hardly appealing. Might be better to live with the problem. Any ideas? I don’t think we can steal “group” as a keyword -- it’s a function exported by Data.List, and I don’t think the benefit justifies the cost. So you are saying you prefer then group to group? Yours, -- P -- .\ Philip Wadler, Professor of Theoretical Computer Science ./\ School of Informatics, University of Edinburgh / \ http://homepages.inf.ed.ac.uk/wadler/ The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Fwd: Two Proposals
George, Thanks very much for this. I like your suggestion, which fits the logical structure perfectly; and you've suggested a neat way around the ugliness of 'group groupBy'. I also note that if we aren't so worried about not introducing new keywords, that 'then group' could become 'group'. Yours, -- P On Mon, Oct 10, 2011 at 11:21 PM, George Giorgidze giorgi...@gmail.com wrote: A quick thought that came to me after hoogling [a] - [[a]]. The first four functions in the search result are named after what they return (noun in plural) rather than what they do (verb). I am talking about inits, permutations, subsequence and tails. So I thought the following syntax might work as well if (as it is already common) grouping functions are named after what they return. then f then f by e then group f then group f by e For example the following code fragments read well: then group inits then group permutations then group subsequences then group tails Here we use the special identifier group as a verb. I have not told you about the fifth result of the hoogling, the groupWith function. The following really looks ugly: then group groupWith by e But following the aforementioned naming convention the groupWith function could as well be named as equals. Now this reads well: then group equals by e Cheers, George -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell] elementary tracing for Haskell
Are there any tools for beginning programmers that give traces of Haskell programs? I want something like the following. Given the defintion sum [] = 0 sum (x:xs) = x + sum xs typing sum [1,2,3] should yield this trace sum [1,2,3] 1 + sum [2,3] 1 + 2 + sum [3] 1 + 2 + 3 + sum [] 1 + 2 + 3 + 0 1 + 2 + 3 1 + 5 6 I know there are advanced tools like Hat, but (unless I'm missing something) they don't yield anything as naive as the above, and it's naive users I'm trying to help here. -- P PS. Google search on Haskell trace yields lots on Hat, plus the following. The Mystery of Brigadier General Harry L. Haskell ... we have developed a short biography of General Haskell and been able to trace the locations where he lived, and, possibly, how the medal came into my family. ... family.phelpsinc.com/branches/haskell/ - 28k - Cached - Similar pages Philip Wadler, Professor of Theoretical Computer Science School of Informatics, University of Edinburgh JCMB, Mayfield Road, Edinburgh EH9 3JZ SCOTLAND +44 131 650 5174 http://homepages.inf.ed.ac.uk/wadler/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: HaskellDoc?
Volker suggests using SGML/DSSSL for documentation. If one were to take this route, I think XML/XSLT would be a more sensible combination. See http://www.cs.bell-labs.com/~wadler/xml for a quick intro to XML. Runciman and Wallace at York have a nice XML library for Haskell. Volker (or anyone else reading this), can you tell me where to find a user manual for DSSSL? I've never been able to locate one. I'd also like an article for SIGPLAN or JFP (or both) describing DSSSL, if you think you can write one please let me know. (For those of you who don't know, DSSSL is based on Scheme.) Cheers, -- P
ICFP 2000: new submission deadline
In order to maintain the same deadline as our sister conference PPDP, we are postponing our submission deadline by two weeks. Our apologies for the change. ICFP 2000: International Conference on Functional Programming Montreal, Canada; 18--20 September 2000 (associated with PLI 2000/PPDP 2000) NEW SUBMISSION DEADLINE: 13.00 EST (18.00 UTC), 15 MARCH 2000 (previously 13.00 EST, 1 March 2000) http://www.cs.bell-labs.com/~wadler/icfp2000 Call and submission details online
ICFP 2000
/sigs/pubs/proceed/template.html. Papers must be submitted in PDF format, or as PostScript documents that are interpretable by Ghostscript, and they must be printable on both USLetter and A4 paper. Individuals for which this requirement is a hardship should contact the program chair. Submitted papers must have content that has not previously been published in other conferences or refereed venues, and simultaneous submission to other conferences or refereed venues is unacceptable. Each paper should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, saying why it is significant, and comparing it with previous work. Authors should strive to make the technical content of their papers understandable to a broad audience. Important dates and submission details ~~ Submission Deadline 13.00 EST (18.00 UTC), 1 March 2000 Submission Length 12 pages in ACM conference format Notification of Acceptance or Rejection8 May 2000 Final Paper Due 12 June 2000 ICFP '00 in Montreal 18--20 September 2000 The submission deadline and length above are firm. Submit electronically via the Web at: http://oopsla.acm.org/icfpservlets/login You will be asked to create and bookmark a personal page. (All information you give will be kept private.) You may submit at any time, and once you have submitted, you may update your submission at any time before the deadline. ICFP thanks OOPSLA and Bjorn Freeman-Benson for providing the submission software and server. Application letters and functional pearls should be labeled as such on the first page. They may be any length up to the full twelve pages, though shorter submissions are welcome. Authors of accepted papers will be required to sign ACM copyright release forms. Program Committee ~ Program Chair Program Committee ~~ ~~ Philip Wadler Richard Bird, Oxford Bell Labs, Lucent Technologies Craig Chambers, Washington 600 Mountain Ave, room 2T-402 Charles Consel, IRISA Murray Hill, NJ 07974-0636, USA Susan Eisenbach, Imperial phone: +1 908 582 4004 Fergus Henderson, Melbourne http://www.cs.bell-labs.com/~wadler Ralf Hinze, Bonn [EMAIL PROTECTED] Shriram Krishnamurthi, Rice Xavier Leroy, INRIA/Trusted Logic General Chair Eugenio Moggi, Genova ~ Greg Morisset, Cornell Martin Odersky Atsushi Ohori, Kyoto Ecole Polytechnique Federale de LausanneCatuscia Palamidessi, Penn State Andrew Wright, Intertrust
Re: drop take [was: fixing typos in Haskell-98]
Chris, I admit your argument about symmetry is attractive. If you could put forward a concrete application, on a par with the `break into blocks' application given earlier, you would likely sway me. -- P
Re: Contexts on data type declarations
So doesn't my proposal give you precisely what you want, and no more? Because my interest is as much in documentation as in constraints on how the program executes (I admit your method achieves the latter). If I write, say, data Eq a = Assoc a b then I'd like the signatures to ensure that the first argument of Assoc is a member of class Eq wherever it appears. Your technique guarantees this is Assoc is used in a constructor, but not if used in a destructor. But when you take a constructor *apart*, the invariant must hold by construction: you couldn't have built the thing you are taking apart unless invariant held. So enforcing the invariant again is redundant; and in addition it pollutes the type of selectors. Your `redundant pollution' is exactly the effect I want to achieve! Clearly, tastes differ. Hope this clarifies, -- P
Re: Market Penetration of FP and Haskell
"S. Alexander Jacobson" [EMAIL PROTECTED] writes: So, if they are making sure that all platforms have a scheme interpreter, why not make the spec language agnostic. i.e. allow the user to use any language that can be compiled/translated into scheme (by code written in scheme?). Your assumption is incorrect. There is no Scheme interpreter in XSL. I should have been clearer in my earlier comment: XSL is a special purpose language with a highly specialised structure (as Alexander notes, it is a little like production rules). It is not as general as either Haskell or Scheme. DSSSL, unlike XSL, was embedded in Scheme and provided both the specialised structure and general-purpose Scheme computation. I'd be very happy if XSL was as nice as Scheme! So the user would be able to say: transformation language=http://www.haskell.org/haskell2scheme /transformation There is an extension mechanism in XSL to allow part of the transformation to be done in another language, roughly similar to the above. -- P
Re: Market Penetration of FP and Haskell
"S. Alexander Jacobson" [EMAIL PROTECTED] writes: There is a campaign going on to separate XSL (eXtensible style language) into two separate languages 1. a transformation language 2. a style language I suggest that now is the opportunity to make a convincing case that the transformational language should be a functional programming language. HoF, Laziness and statelessness are ideal properties for such a language. The existing XSL spec was somewhat influenced by scheme, but a transformational language has stronger consistency requirements and should be typechecked so Haskell seems like a good choice. I have bad news, good news, bad news, and good news. Bad news: The proposal to split XSL refers to the current working draft, which already contains a transformation language (Section 2) and a style language (Section 3). Preliminary versions of the transformation language are already in wide use (including Internet Explorer 5 by Microsoft; LotusXSL by IBM Alphaworks; and xt, by James Clark, editor of the XSL document). So it's way too late, there is no chance of getting the W3C to switch to Haskell. Good news: The charter requires that XSL be `a declarative language', and in fact the transformation part of XSL is a functional language. It is largely based on DSSSL, the stylesheet language for SGML, an ISO standard based on Scheme. (I was gobsmacked when I first discovered Scheme was part of an ISO standard for document production!) Bad news: XSL is not nearly as nice as Haskell. Sigh. Good news: Malcolm Wallace and Colin Runciman at York are working on a Haskell library for manipulating XML. If the transformation and style languages are separated (which seems likely to happen), then that will make it easier for users to substitute Haskell for the transformation part of XSL, if they choose. -- Phil Wadler (member of the XSL working group) PS. If anyone has any suggestions about *small and reasonable* changes to the XSL working draft that would be an improvement, please let me know. XSL working draft: http://www.w3.org/TR/WD-xsl XSL W3C home page: http://www.w3.org/Style/XSL/ ------- Philip Wadler [EMAIL PROTECTED] Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler 600 Mountain Ave, room 2T-402 office: +1 908 582 4004 Murray Hill, NJ 07974-0636 fax: +1 908 582 5857 USA home: +1 908 626 9252 ---
Re: MonadZero (concluded)
class Monad m where return :: m a (=) :: m a - (a - m b) - m b () :: m a - m b - m b fail :: String - m a fail s = error s IO.fail becomes IO.ioError Looks good. class Monad m = MonadPlus m where mzero :: m a mplus :: m a - m a - m a Why is this here? It doesn't need to be in the prelude. Just leave it for the user to define (and then the user may pick better names, like Ringad, zero, and +). -- P
mfail - fail
Here's an even better idea: replace mfail with fail. It is, after all, the fail of the IO monad! Option 4'': Monad ((=), return, fail) -- P
Re: mfail - fail
Ralph writes, Unfortunately not, fail of IO fame has type IOError - IO a and not String - m a as Monad's new member. Here's my suggestion: o Monad ((=), return, fail) o throw (thanks Frank) instead of fail for the IO operation o raise for Haskell-2's exception mechanism (raise and handle)? Oops, good point. `throw' in IO works fine; or if we don't want to steal such a general name, `ioerror' seems sensible. -- P
Re: Default Default
John Peterson writes Int is really not a nice datatype and we shouldn't be allowing it to crop up unexpectedly. Yes, but if we believed that, we should use Integer, not Int, for length. You are right, beginners may stub their toe on factorial. On the other hand, with the default set to Integer, beginners may stub their toe on bad performance. Anyone familiar with, say, C, will be unsurprised by the need to switch Int to Integer to get factorial to work, but will be very surprised by the need to switch Integer to Int to get decent performance. -- P
Re: Haskell 98 progress
- The simple-context restriction. My difficulty here is that there is just no good place to stop. The 'type variable in head position' option is attractive, but it's unimplemented, untested, and it's neither the status quo nor a final destination. On the other hand, we *believe* it's technically ok and restores principal types. It seems to me restoring principal types is worth it. Didn't we vote for this change at ICFP? I thought the `slippery slope' argument you give here was applied to something else, namely, allowing more general types in instance declarations. I argued for that change too, but you and some others were unconvinced. -- P
Re: MonadZero (concluded?)
There is no need to have both `mzero' and `mfail' in every monad. Just have `mfail'. Leave `zero' and `plus' to MonadPlus. This should make Eric partially happy. It also means one can simply write instance Monad [] where ...return, =, as before... mfail s = [] rather than instance Monad [] where ...return, =, as before... mfail s = mzero mzero = [] The names `mzero' and `mfail' are horrible. I like Ralph's suggestion to change `fail' to `raise' in the IO monad, and use `fail' for `mfail'. If that doesn't work, try something else, but please pick names that have a simple meaning in English (as with `return') not monsters like `mzero' and `mfail'. -- P
Re: MonadZero
Simon says,
Here are the two proposals I suggested in
http://research.microsoft.com/Users/simonpj
1.Fix up the current version.
use MonadZero for do expressions with *irrefutable* patterns
(instead of *unfailable* patterns as now)
2.Nuke MonadZero altogether.
add mfail :: m a to Monad instead
Sorry, I don't understand option 2, can you please explain?
Simon also says,
But (1) really sticks in my craw. How can we explain this:
f :: Monad m = m (a,b) - m a
f m1 = do { x - m1; return (fst x) }
g :: MonadZero m = m (a,b) - m a
g m1 = do { (a,b) - m1; return a }
h :: Monad m = m (a,b) - m a
h m1 = do { ~(a,b) - m1; return a }
... the type differences between g and f,h are really hard to justify.
Yes. But these subtle differences exist independent of MonadZero.
f x = [fst x]
g (a,b) = [a]
h ~(a,b) = [a]
Here it turns out f and h are equivalent and g differs, just as above.
All that differs with MonadZero is that the type is affected, as well
as the semantics. Eric and others point out that this may be a good
thing: better to find out about the difference at compile-time than
at run-time.
I want to make a different plea: keep the language design consistent!
Yes, the difference between f, g, h is a wart, but let's have one wart
repeated, rather than two different warts.
-- P
Re: MonadZero
Simon says, Sorry, I don't understand option 2, can you please explain? * Eliminate MonadZero * Add 'mfail :: m a' to Monad, with a suitable default decl * Every do expression has a type in Monad I must be dense this morning, as I'm still in the dark. What is the intended meaning of `mfail'? If `mfail' is `mzero', why change the name? What is the suitable default declaration? What, if anything, does `mfail' have to do with `do' expressions? -- P
Re: MonadZero
Thanks for the further explanation. On reflection there probably shouldn't be a default declaration for mzero. Any compiler for Haskell must do *something* if a method is called for which there is neither an explicit declaration in the instance, nor a default method. ... Leaving out the default method would let a compiler halt execution reporting "Pattern match failure in `do' expression at line 39 of Foo.hs" which is what we want. Well, you can't always give such a message, because the monad might be unresolved at the point the `do' appears (as in all your examples where MonadZero had to appear in the scope). And you message looks odd, since the problem is that mzero is undefined. But these are implementation issues. I see the attraction of adding `mzero' to Monad. The chief disadvantage is that it makes the class hierarchy less expressive. Is there anyone out there who values the separation of Monad and MonadZero for purposes other than `do' notation? If not, then I don't oppose this option. I like Ralph's suggestion to use `fail' instead of `mzero', and to change `fail' in IO to `raise', if that doesn't break too many existing programs. -- P
Re: Haskell 98
Consider the function t :: T a = T a - T a I think that it's far from clear what each of the T's mean! Worse, in Haskell 2 we'll also have t :: T T = T a - T a In (T T) one is class and the other is a type constructor. Let's leave the language as it is: class names and type names must be distinct. Rationale: the above examples show that a change might have questionable consequences. Recall that the change requires adding the label `class' to signatures, but not adding the label `type'; it feels more like a convenient hack than a well-rounded design. Rather than make a questionable change now, let's leave it for Haskell 2 and get it right there. -- P
Re: Functional DSP
I was planning to try similar things you have mentioned on your page, such as interfacing to "the fastest FFT in the West" (FFTW) via GreenCard, ... By the way, FFTW although written in C, was generated by a functional program written in Caml. You can find more details on the web page Functional Programming in the Real World http://www.cs.bell-labs.com/~wadler/realword/ -- P
Int vs. Integer
Hi Simon, This really seems to have touched off a firestorm! I think the meta-argument made by Simon T (and by you) is sensible, so I don't object to maintaining the status quo. But you implied that changing the libraries led to `a ball of spaghetti', and I don't see that, can you please explain? I'm not arguing to change the decision, I just want to know what problems (if any) you spotted. Cheers, -- P
Re: Int vs Integer
Simon proposes not to change the prelude to support Integer, giving this argument: The more this topic gets discussed the more I that it's like other Prelude things: you pull on one thing and the plate of spaghetti ends up in your lap. I'm confused. I thought at the ICFP Haskell meeting we agreed on the following types: length :: Integral i = [a] - i take, drop :: Integeral i = i - [a] - [a] showsPrec :: (Show a, Integral i) = i - a - ShowS and so on. These have the advantage that they work with either Int or Integer. If Haskell implicitly imposes `default (Integer,Double)' then the old efficiency level can be recalled by simply adding the line `default (Int,Float)' to your program. The only problem I recall was what types to give to member of class Floating, and that looked so odd that it looked to need changing regardless of what we did with Int and Integer. Simon argues that it is not so bad to retain Int over Integer, saying I don't think Chris's "plain ordinary punters" will notice. They don't write programs with lists longer than 2^31. I think this argument is misleading. The key to the above proposal is that it makes it easy to write programs that use either Int or Integer uniformly. With Simon's proposal, if you wish to use Integer then you will need to introduce coercions from Int to Integer. This makes life hard for any punter who wishes to use Integer as a default, or for any punter who uses Int as a default and gets overflow (admittedly, the overflow is likely to be on something other than a list length, but so what?). I'm not against adopting a conservative design if there is a problem, but then Simon ought to explain what the problem is. Cheers, -- P
Re: Int vs Integer
Simon PJ writes: I think we should - generalise length, splitAt, drop, take, replicate - generalise toEnum, fromEnum - leave (!!) alone (arrays must fit in an address space) I don't know what to do about RealFloat. Sigh If the goal is to make life easy for beginners (and to make it easy to avoid overflow errors), shouldn't we generalise *all* uses of Int, so that a beginner can use Integer uniformly everywhere, and need never know about Int? Even given this principle, it's not clear what to do about RealFloat, which has both Int and Integer: generalize both to the same type variable, generalize each separately, generalize Int only, or replace Int by Integer? -- my guess is the first is correct. Uniformly generalizing Int strikes me as the right thing to do, although I hope before we commit to it someone will test it in advance, say on a subset of the Nofib suite. -- P
Re: type errors
You're right. The restriction is excessive. Thanks for pointing this out. Probably we should only require that at least one of the class variables is constrained. Why even require this? (All x) = x - x uses the class `All' which restricts its argument not one whit. -- P
Re: Teaching Haskell
Speaking of this, when is someone going to write an fp book that teaches all the interesting stuff? Monads, advanced use of classes, advanced types in general, exceptions, etc... [here's an idea: after comprehending the book, the student should be able to follow the discussion on this mailing list without difficulty] In my opinion, such a book should assume the reader has already been through Bird and Wadler or whatever, is familiar with the lambda calculus, and has written substantial programs. Please, no more "introduction to fp" books! How about second editions of `Intro to FP'? Richard has revised Bird and Wadler, which is now just Bird. It includes type classes and monads, and should be in your bookstore round about now. -- P ------- Philip Wadler [EMAIL PROTECTED] Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler 600 Mountain Ave, room 2T-402 office: +1 908 582 4004 Murray Hill, NJ 07974-0636 fax: +1 908 582 5857 USA home: +1 908 626 9252 --- ``There may, indeed, be other applications of the system than its use as a logic.'' -- A. Church, 1932 ---
Re: Wadler's prettier printer
Rossberg writes,
thinking about whether the pretty printer proposed by Wadler requires
some changes to be efficient in a strict language, I stumbled over the
the last case defining `flatten':
flatten (x :| y) = flatten x
I wonder why it is necessary here to recurse on x. The only point were a
doc (x:|y) is constructed is in the function `group':
group z = flatten z :| z
So the x above is always flat already. Wouldn't the equation
flatten (x :| y) = x
suffice? Doing recursion here seems to be unnecessary overhead. In
particular, it prevents structure sharing between alternatives when
grouping, because flatten rebuilds the whole doc tree (which might be
more of a problem without laziness).
Am I missing something?
You're not the one who missed something. I didn't spot this
optimization because I had in mind the case where the user might use
| directly. If we disallow this, your tricky optimisation is quite
sensible. As it happens, it doesn't seem to improve time or space by
much, at least for the lazy version. I include modified code below.
It's wonderful to have clever people reading and commenting on
my code. Thanks! -- P
---
Philip Wadler [EMAIL PROTECTED]
Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler
600 Mountain Ave, room 2T-402 office: +1 908 582 4004
Murray Hill, NJ 07974-0636 fax: +1 908 582 5857
USA home: +1 908 626 9252
---
-- Pretty printer based on grouping
-- as in March 1998 version of `A prettier printer'
-- Philip Wadler, March 1998
-- Modified version based on suggestion of Andreas Rossberg
-- Philip Wadler, May 1998
-- Two optimized lines, marked below, exploit the invariant that
-- the left hand argument of :| must be result of applying flatten.
infixr 5 :|
infixr 6 :
infixr 6
data DOC= NIL
| DOC : DOC
| NEST Int DOC
| TEXT String
| LINE
| DOC :| DOC
data Doc= Nil
| String `Text` Doc
| Int `Line` Doc
nil = NIL
x y = x : y
nest i x = NEST i x
text s = TEXT s
line = LINE
group (x :| y) = x :| y-- *** remove line for unoptimized
group x = flatten x :| x
flatten NIL = NIL
flatten (x : y)= flatten x : flatten y
flatten (NEST i x) = NEST i (flatten x)
flatten (TEXT s) = TEXT s
flatten LINE = TEXT " "
flatten (x :| y) = x -- *** replace by (flatten x) for unoptimized
layout Nil = ""
layout (s `Text` x) = s ++ layout x
layout (i `Line` x) = '\n' : copy i ' ' ++ layout x
copy i x = [ x | _ - [1..i] ]
best w k x = be w k [(0,x)]
be w k []= Nil
be w k ((i,NIL):z) = be w k z
be w k ((i,x : y):z) = be w k ((i,x):(i,y):z)
be w k ((i,NEST j x):z) = be w k ((i+j,x):z)
be w k ((i,TEXT s):z)= s `Text` be w (k+length s) z
be w k ((i,LINE):z) = i `Line` be w i z
be w k ((i,x :| y):z) = better w k (be w k ((i,x):z)) (be w k ((i,y):z))
better w k x y = if fits (w-k) x then x else y
fits w x | w 0 = False
fits w Nil = True
fits w (s `Text` x) = fits (w - length s) x
fits w (i `Line` x) = True
pretty w x = layout (best w 0 x)
-- Utilities
space = text " "
x / y = x line y
x + y = x space y
par x = text "(" x text ")"
stack = foldr1 (/)
strip = foldr1 (+)
-- Testing
dataTerm= Term String [Term]
prTerm (Term n []) = text n
prTerm (Term n ts) = par (group (nest 2 (stack (text n : map prTerm ts
szTerm (Term n ts) = length n + length ts + sum (map szTerm ts)
mkTerm 0 i = Term (mkName i) []
mkTerm (d+1) i = Term (mkName i) (map (mkTerm d) (randoms i))
mkName i= [ 'x' | j - [1..i] ]
randoms i
Re: Design Methodologies
What I am looking for are the formal design methods and tools supporting those methods that lead one through the task of decomposing a problem (possibly specified in a requirements document) into a design that can be used as the starting point for coding with a functional language. The documentation should not only cover the engineering task of (using generic terms) top-level-design, intermediate-design, detailed-design, unit-codingtest, testintegration, requirements-testingsell-off, etc, but also how one manages such a project. Good question. Both Erlang and Natural Expert have been widely used in industry, and both have training courses that cover at least some of what you want. For a quick intro to these, see www.cs.bell-labs.com/~wadler/topics/recent.html#angry and follow the pointers from there. (This paper also contains just what you don't want, a list of serious applications of FP. :-) Your quote represents what I suspect is a widely held view. "... functional approaches do not permit you to create an abstract notion of system state that can be modeled. Functional languages are great for people to think about problems (especially recursion), but they are no good for large software systems. It's not that people haven't looked at them in this context; they don't work." This claim is belied by the success of Erlang and Natural Expert. Also, there are scores of functional programs containing over 50K lines. While not large in software engineering terms, these go well beyond merely being used to `think about problems (especially recursion)'. If the quote is not confidential, I'd appreciate if you could give a source for it. Yours, -- P ------- Philip Wadler [EMAIL PROTECTED] Bell Laboratories http://www.cs.bell-labs.com/~wadler Lucent Technologies office: +1 908 582 4004 600 Mountain Ave, room 2T-402 fax: +1 908 582 5857 Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252 ---
Dave MacQueen: POPL call for participation
Phil, Could you send the following POPL 98 Call for Participation message to
the Haskell mailing list for me? Thanks, Dave
---
ACM PRINCIPLES OF PROGRAMMING LANGUAGES (POPL '98)
**
Twenty-fifth Annual ACM Symposium
January 19 - 21, 1998, San Diego, California
ADVANCE PROGRAM AND CALL FOR PARTICIPATION
==
POPL '98 is the 25th in the series that started in Boston in 1973. In
honor of this anniversary, we will have special invited talks from
John Reynolds (CMU), Gerard Berry (Ecole des Mines/INRIA), and
Mark Wegman (IBM), as well as a regular invited talk by Peter Lee (CMU).
The Fifth International Workshop on Foundations of Object Oriented
Languages (FOOL 5) will be held in conjunction with POPL '98 on
January 17 - 18, 1998.
**
Important Dates
===
December 17, 1997 - expiration of special POPL hotel rates
December 31, 1997 - deadline for advance registration discount
Important URLs
==
http://cm.bell-labs.com/cm/cs/who/dbm/popl98/
General POPL '98 information, including the advance program,
registration and hotel.
http://www.cs.williams.edu/~kim/FOOL/FOOL5.html
Information about FOOL 5.
www.reg-master.com/popl98.html
Online conference registration form.
http://www.marriott.com/marriott/SANMV/
San Diego Marriott Mission Valley Hotel web page. Information
on travel and facilities.
**
POPL'98 PROGRAM
===
MONDAY 19 JANUARY
Invited Talk: 9:00-10:00
Where Theory and Practice Meet: POPL Past and Future
John Reynolds, Carnegie Mellon University.
Session 1: 10:30-12:30.
Chaired by Neil Jones, University of Copenhagen.
Higher-Order UnCurrying
John Hannan and Patrick Hicks
Alias Analysis of Executable Code
Samya Debray, Robert Muth and Matthew Weippert
Escape Analysis: Correctness Proof, Implementation and Experimental
Results
Bruno Blanchet
Data Flow Analysis is Model Checking of Abstract Interpretations
David A. Schmidt
Session 2: 14:00-16:00.
Chaired by Atsushi Ohori, Kyoto University.
Bridging the Gulf: a Common Intermediate Language for ML and Haskell
Simon Peyton Jones, John Launchbury, Mark Shields and Andrew Tolmach
Correctness of Monadic State: An Imperative Call-by-Need Calculus
Zena M. Ariola and Amr Sabry
Functional Representation of Data Structures with a Hole
Yasuhiko Minamide
From System F to Typed Assembly Language
Greg Morrisett, David Walker, Karl Crary, and Neal Glew
Session 3: 16:30-18:30.
Chaired by Jeanne Ferrante, University of California, San Diego.
Maximal Static Expansion
Denis Barthou, Albert Cohen and Jean-Franccedil;ois Collard
Array SSA Form and its Use in Parallelization
Kathleen Knobe and Vivek Sarkar
Putting Pointer Analysis to Work
Rakesh Ghiya and Laurie J. Hendren
Edge Profiling versus Path Profiling: The Showdown
Thomas Ball, Peter Mataga and Mooly Sagiv
TUESDAY, JANUARY 20, 1998
Invited Talk: 9:00-10:00.
Global Trends in Flow Analysis
Mark Wegman, IBM.
Session 4: 10:30-12:30.
Chaired by Martin Odersky, University of South Australia.
A Type System for Java Bytecode Subroutines
Raymie Stata and Martiacute;n Abadi
Java-light is Type-Safe -- Definitely
Tobias Nipkow and David von Oheimb
Classes and Mixins
Matthew Flatt, Shriram Krishnamurthi and Matthias Felleisen
Manufacturing Cheap, Resilient, and Stealthy Opaque Constructs
Christian Collberg, Clark Thomborson and Douglas Low
Session 5: 14:00-16:00.
Chaired by Nevin Heintze, Bell Laboratories, Lucent Technologies.
From Polyvariant Flow Information to Intersection and Union Types
Jens Palsberg and Christina Pavlopoulou
Inference of Polymorphic and Conditional Strictness Properties
Thomas P. Jensen
Fast Interprocedural Class Analysis
Greg DeFouw, David Grove and Craig Chambers
Path-Sensitive Value-Flow Analysis
Rastislav Bod\'{i}k and Sadun Anik
Session 6: 16:30-18:30.
Chaired by Xavier Leroy, INRIA, Rocquencourt.
Local Type Inference
Benjamin C. Pierce and David N. Turner
Static Typing for Dynamic Messages
Susumu Nishimura
Second-order Unification and Type Inference for Church-style Polymorphism
Aleksy Schubert
Dynamic Typing as Staged Type Inference
Mark Shields, Tim Sheard and Simon Peyton Jones
Invited Talk: 20:30-21:30.
From Principles to Programming Languages
G\'{e}rard Berry, \'{E}cole des Mines and INRIA, Sophia-Antipolis.
WEDNESDAY, JANUARY 21, 1998
Re: Damas-Milner, Hindley-Milner, ...
Briefly, what is the difference between Damas-Milner and Hindley-Milner typing? None. They are different names for the same thing. The actual algorithm was discovered a number of times. Hindley wrote a history of it, which I don't have to hand. He notes that it had already been implemented on a computer in the 1950s! I believe he attributes it to Curry. It was also rediscovered by a number of others, including Jim Morris, then a PhD student at MIT. Hindley wrote down a concise description, based on logic. Milner, independently, rediscovered the algorithm, apparently not based on logic. Later, Milner and his PhD student Damas reformulated the algorithm in a much more accessible way, with the connection to logic restored. Milner's key contribution -- and very important it was, too -- was to add the syntactic form `let x=e0 in e1'. Without this, the algorithm infers principle types, but does not seriously exploit polymorphism. -- P
Re: Monads and Linear Logic
In general laymen's terms, what are the performance and expressiveness issues in comparing monads with linear objects? You may want to glance at the latest version of `How to Declare an Imperative' (Computing Surveys, to appear), which explicitly makes this comparison. It's available via my home page. -- P --- Philip Wadler [EMAIL PROTECTED] Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/ Lucent Technologies office: +1 908 582 4004 600 Mountain Ave, Room 2T-304 fax: +1 908 582 5857 Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252 ---
Re: Evaluating Haskell
I have not followed the Pizza mailing list (how do you get Pizza in the mail?). You can find out about Pizza (and join the mailing list) at any of the web sites. If you are interested in functional programming and Java, please have a gander! -- P Pizza Sites More information on Pizza is available at the following web sites (which mirror each other): http://www.cis.unisa.edu.au/~pizza University of South Australia http://cm.bell-labs.com/cm/cs/who/wadler/pizza/welcome.html Bell Labs, Lucent Technologies http://www.math.luc.edu/pizza/ Loyola University, Chicago ftp://ftp.eecs.tulane.edu/pub/maraist/pizza/welcome.html Tulane University, New Orleans http://wwwipd.ira.uka.de/~pizza University of Karlsruhe Philip Wadler [EMAIL PROTECTED] Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/ Lucent Technologies office: +1 908 582 4004 700 Mountain Ave, Room 2T-304 fax: +1 908 582 5857 Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252 ---
Re: Evaluating Haskell
I have not followed the Pizza mailing list (how do you get Pizza in the mail?). You can find out about Pizza (and join the mailing list) at any of the web sites. If you are interested in functional programming and Java, please have a gander! -- P Pizza Sites More information on Pizza is available at the following web sites (which mirror each other): http://www.cis.unisa.edu.au/~pizza University of South Australia http://cm.bell-labs.com/cm/cs/who/wadler/pizza/welcome.html Bell Labs, Lucent Technologies http://www.math.luc.edu/pizza/ Loyola University, Chicago ftp://ftp.eecs.tulane.edu/pub/maraist/pizza/welcome.html Tulane University, New Orleans http://wwwipd.ira.uka.de/~pizza University of Karlsruhe Philip Wadler [EMAIL PROTECTED] Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/ Lucent Technologies office: +1 908 582 4004 700 Mountain Ave, Room 2T-304 fax: +1 908 582 5857 Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252 ---
GC (was: Stumped without mutation... )
I think that Java might be slow, just because of this automatic garbage collection. I can't let this chestnut go unchallenged. Let's not bandy about claims without evidence. GC is perfectly fine for building into phone switches (via Erlang) so it can't be all that slow. -- P
Re: pattern guards + monads
Now, for monads, Phil Wadler writes a law: m = \x - k x ++ h x = m = k ++ n = k in which 'h' appears on the lhs but not the rhs, and 'n' on the rhs but not the lhs. ... perhaps the equation should read as follows? m = \x - k x ++ h x = m = k ++ m = h Yes, of course it should. Thanks for the correction. -- P
Re: Monads, Functors and typeclasses
Maybe we should do it as follows: At the moment you make an instance of a class that has default definitions for one of its superclasses, and there is no corresponding instance for that class, we implicitly insert the specified default instance. If there are more instances to choose from at that point, we report an error. If I read this properly, the intent is to make the meaning of the program depend on the order in which it is compiled. A good design will make the meaning of a program depend only on the program text. -- P
Journal of Functional Programming
Below are the contents of recent issues of the Journal of Functional Programming. Contents for all issues, and abstracts for the last three years, can be found at: http://www.dcs.gla.ac.uk/jfp/ The site also contains information on how to submit, and how you or your library can subscribe. -- Philip Wadler, Editor-in-Chief, JFP JFP 6.4 July 1996 = Representing demand by partial projections John Launchbury and Gebreselassie Baraki New dimensions in heap profiling Colin Runciman and Nicklas Rojemo Benchmarking implementations of functional languages with 'Pseudoknot', a float-intensive benchmark Pieter Hartel et al Functional Pearl: The third homomorphism theorem Jeremy Gibbons JFP 6.5 September 1996 == A syntactic theory of type generativity and sharing Xavier Leroy LambdaV, a calculus of explicit substitutions which preserves strong normalisation Zine-el-Abidine Benaissa, Daniel Briaud, Pierre Lescanne and Jocelyne Rouyer-Degli Pi-Red+ An interactive compiling graph reduction system for an applied Lambda-calculus Dietmar Gartner and Werner E. Kluge A simple proof of the undecidability of inhabitation in Lambda-P Marc Bezem and Jan Springintveld JFP 6.6 November 1996 = The Bologna Optimal Higher-order machine Andrea Asperti, Cecilia Giovannetti and Andrea Naletto A positive supercompiler M. H. Sorensen, R. Gluck and N. D. Jones Optimal purely functional priority queues Gerth Stolting Brodal and Chris Okasaki JFP 7.1 January 1997 A foundation for actor computation Gul A. Agha, Ian A. Mason, Scott F. Smith and Carolyn L. Talcott First-order functional languages and intensional logic R.Rondogiannis and W.W. Wadge On the effectiveness of functional language features: NAS benchmark FT J. Hammes, S. Sur and W. Bohm Call for papers: Special issue on Theorem Provers and Functional Programming. --- Philip Wadler [EMAIL PROTECTED] Bell Laboratories http://cm.bell-labs.com/cm/cs/who/wadler/ Lucent Technologies office: +1 908 582 4004 700 Mountain Ave, Room 2T-304 fax: +1 908 582 5857 Murray Hill, NJ 07974-0636 USA home: +1 908 626 9252 ---
Re: pattern guards and guarded patterns
Tommy Thorn writes: My only worry is that Haskell (if not already) is turning into the C++ of functional languages, ie. feature upon feature. Haskell is already quite a mouthfull to learn. This worries me too. Not least is the problem that - is not a particularly natural syntax for this feature, as others have noted. (Though I admit the connection with qualifiers is tempting.) Simon PJ writes: Re (b) we write f (x:xs) [] = e1 f (x:xs) (y:ys) = e2 when you might think we should find a syntax to allow f (x:xs) [] = e1 (y:ys) = e2 But we write out the common prefix and expect the compiler to spot the common pattern. Similarly I think we should rely on the compiler to spot common prefixes of guards. f x y | (x:xs) - xs, [] - ys = e1 | (x:xs) - xs, (y:ys) - ys = e2 The only extra difficulty is that the RHS of the pattern guard can be an expression. I have to say, this looks pretty ugly to me, and I'm not sure I would be happy trusting it to an optimiser. It is arguably a mistake that Haskell does not allow some way of capturing commonality in pattern matching. As I recall, we very nearly added the syntax f (x:xs) [] = e1 ' ' (y:ys) = e2 and refrained only because we wanted a conservative design. Simon's suggestion strikes me as far from conservative, so perhaps it is worth revisiting more general issues of pattern matching. -- P
Re: global type inference
I think the report has it about right. * A conforming implementation of Haskell 1.4 must support mutually recursive modules. That is, a collection of individually legal mutually recursive modules is a legal Haskell program. * The Report recognises that implementations available in the forseeeable future are likely to require the programmer to supply extra type information to support separate compilation of mutually recursive modules. For example, the implementation may require exported functions to be equipped with type signatures. Why muddle implementation with language design? Pick a design that we know everyone can implement -- e.g., exported functions must have type declarations -- and stick to that. When the state of implementations improve, the specification for Haskell 1.5 can change accordingly. -- P
Re: global type inference
This isn't muddling implemenation with language design. The language design says mutual recursion is OK. A particular implementation supporting separate compilation will typically require a variety of "help", such as a Makefile with accurate dependencies. Requiring type signatures, or interface files, or whatever is just another implementation specific thing to support separate compilation. The language design should at least say what is a legal Haskell file, and what is not. As much as possible, it should lay out exactly what I need to do to write a program that will work on any Haskell compiler that conforms to the definition. It seems to me that the language definition should go further than it does on this point, though perhaps reasonable people may disagree. -- P
Re: Haskell 1.3
It looks ugly, but we could say that a data declaration does not have to have any constructors: data Empty = -- Lennart I agree that the best way to fix this is to have a form of data declaration with no constructors, but I'm not keen on the syntax you propose. How about if we allow the rhs of a data declaration to be just `empty', where `empty' is a keyword? data Empty = empty -- P
Haskell 1.3
Congratulations to all involved on Haskell 1.3! I especially like the introduction of qualified names and the attendant simplifications. Here are some small suggestions for further improvement. Interfaces ~~ Suggestion: the introduction should draw attention to the fact that interface files are no longer part of the language. Such a wondrous improvement should not go unremarked! ISO Character Set ~ Suggestion: Add a one-page appendix, giving the mapping between characters and character codes. Fields and records ~~ Suggestion: Use = to bind fields in a record, rather than -. I concur with Thomas Hallgren's argument that - should be reserved for comprehensions and for `do'. SML has already popularised the = syntax. Suggestion: Use the SML syntax, `#field' to denote the function that extracts a field. Then there is no possibility of accidentally shadowing a field name with a local variable. Just as it is a great aid to the readability of Haskell for constructors to be lexically distinguished from functions, I predict it will also a great aid for field extractors to be lexically distinguished from functions. (Alternative suggestion: Make field names lexically like constructor names rather than like variable names. This again makes shadowing impossible, and still distinguished fields from functions, though now field extractors and constructors would look alike.) The empty type ~~ Suggestion: Include among the basic types of Haskell a type `Empty' that contains no value except bottom. It was a dreadful oversight to omit the empty type from Haskell, though it took me a long time to recognise this. One day, I bumped into the following example. I needed the familiar type data Tree a = Null | Leaf !a | Branch (Tree a) (Tree a) instantiated to the unfamiliar case `Tree Empty', which has `Null' and `Branch' as the only possible constructors. One can simulate the empty type by declaring data Empty = Impossible and then vowing never to use the constructor `Impossible'. But by including `Empty' in the language, we support a useful idiom and (perhaps more importantly) educate our users about the possibility of an algebraic type with no constructors. It would be folly to allow only non-empty lists. So why do we allow only non-empty algebraic types? The infamous (n+1) patterns ~~~ Suggestion: Retain (n+1) patterns. If Haskell was a language for seasoned programmers only, I would concede that the disadvantages of (n+1) patterns outweigh the advantages. But Haskell is also intended to be a language for teaching. The idea of primitive recursion is powerful but subtle. I believe that the notation of (n+1) patterns is a great aid in helping students to grasp this paradigm. The paradigm is obscured when recursion over naturals appears profoundly different than recursion over any other structure. For instance, I believe student benefit greatly by first seeing power x 0 = 1 power x (n+1) = x * power x n and shortly thereafter seeing product [] = 1 product (x:xs) = x * product xs which has an identical structure. By comparison, the definition power x 0 = 1 power x n | n 0 = x * power x (n-1) completely obscures the similarity between `power' and `product'. As a case in point, I cannot see a way to rewrite the Bird and Wadler text without (n+1) patterns. This is profoundly disappointing, because now that Haskell 1.3 is coming out, it seems like a perfect time to do a new edition aimed at Haskell. The best trick I know is to define data Natural = Zero | Succ Natural but that doesn't work because one must teach recursion on naturals and lists before one introduces algebraic data types. Bird and Wadler introduces recursion and induction at the same time, and that is one of its most praised features; but to try to introduce recursion, induction, and algebraic data types all three at the same time would be fatal. Now, perhaps (n+1) patterns introduce a horrible hole in the language that has escaped me; if so, please point it out. Or perhaps no one else believes that teaching primitive recursion is important; if so, please say. Or perhaps you know a trick that will solve the problem of how to rewrite Bird and Wadler without (n+1) patterns; if so, please reveal it immediately! Otherwise, I plead, reinstate (n+1) patterns. Yours, -- P --- Professor Philip Wadler[EMAIL PROTECTED] Department of Computing Sciencehttp://www.dcs.glasgow.ac.uk/~wadler University of Glasgow office: +44 141 330 4966 Glasgow G12 8QQ fax: +44 141 330 4913 SCOTLAND home: +44 141 357 0782
Re: 1.3 PreludeList _____By functions' restricted type
Alistair, I agree with Mike Gunter on this one. -- P Mike Gunter writes: The By functions in the 1.3 PreludeList (elemBy, deleteBy, etc.) all take ``equality'' predicates with type a - a - Bool. Most of these functions (with no change in definition that I see in a quick check) could take predicates with type a - b Bool (with a corresponding change in the type of the other arguments). For example, I find myself wanting to use elemBy :: (a - b - Bool) - a - [b] - Bool elemBy = any (eq x) while the draft prelude has elemBy :: (a - a - Bool) - a - [a] - Bool elemBy = any (eq x) The one downside that I can see (I've not thought about this long) of such a generalization is a few problems (caught during type-checking) when one forgets which predicate argument comes from the key and which from the list. What are the others? I thought briefly of doing this but decided against it for several reasons. These are weak and somewhat interconnected - so they may well yield to a few minutes intelligent thought (sadly, I'm incapable of intelligent thought at the moment - I can't get to the coffee shop for the snow and Yale coffee is undrinkable). 1) The less general signature makes it a simple generalisation of the existing functions. In particular, if Haskell allowed these type synonyms, we could have: type Eq a = a - a - Bool -- illegal: can't use same name for type Ord a = a - a - Bool -- type and class elem :: Eq a = a - [a] - Bool elemBy :: Eq a - a - [a] - Bool 2) The semantics of these functions is somewhat subtle (ie tedious to informally state/remember) if the predicate is not an equivalence. Allowing the more general signatures encourages use of non-equivalences. 3) Where an equivalence is not being used (eg every time the predicate has most general type "a - b - Bool"), a name like "elemBy" doesn't really capture what is going on. The obvious fix is of course to come up with better names - but what?? And, once we've provided the more general versions with different names, should we throw in the elemBy, deleteBy, etc anyway for consistency with nubBy and friends? [Incidentally, the current mood of the Haskell committee seems to be to put these in libraries as part of an (often ignored) effort to slim Haskell down - or at least reduce its rate of growth.] Alastair Reid Yale Haskell Project
Re: Multiple parameters to classes
| I am part of a group working on a new language for Microwave hardware
| design (MHDL). As it turns out, we are incorporating almost all of
| Haskell 1.2 into it.
If there is anything written about this language, please send a pointer
to this mailing list; and please keep us appraised of your progress.
It's always good to know of applications of functional programming.
| We cannot do this in Haskell, and we cannot do this in Gofer either
| because all type variables in the class signature have to be mentioned
| in all the method signatures.
The restriction you mention in Gofer ("all type variables in the class
signature have to be mentioned in all the method signatures") might be
avoided by simply using a separate class to define each operator.
| | Aside:
| | The fact that ti _must_ mention u1, but may or may not mention u2,
| | ..., uk is the significant change from Gofer (and Haskell, which
| | only allows one type variable in the class declaration). We think
| | that this would allow disambiguation with the "ease" of Haskell, but
| | still allow us the power of multiple class parameters in class
| | declarations.
This will allow easy disambiguation if you require that each instance
of the class differs in the first parameter. But if you allow
instance DemoClass Int Char where ...
instance DemoClass Int Bool where ...
then disambiguation will not be so easy.
| Our question to the gurus is the following: is this too much to ask?
| Are we going to mess up the typing philosophy of Haskell with this?
The only way to get a sure answer to these questions is to write a
formal specification of your system, and to convince yourself that
you have a type inference algorithm that is sound and complete with
respect to this system (e.g., yields principle types). I strongly
urge you complete some sort of formal specification before you begin
implementation.
The GRASP team at Glasgow is putting the finishing touches on a paper
that formally describes type classes as implemented in Haskell, which
you may find helpful. We will post a pointer to this paper when it's
done. I hope Mark Jones and Martin Odersky will also post pointers to
their recent work in this area.
Cheers, -- P
Re: Expressiveness of functional language I/O
Evan writes: | Consider a polymorphic continuation request such as the following: | | someRequest :: T a - (U a - Dialogue) and then shows this does not work in the stream model, unless one has existential types. Quite true, but note that there are *no* polymorphic IO functions! At least, not for any `true' polymorphic function satisfying Reynold's parametricity theorem. See Reynolds' classic 1984 paper, or my `Theorems for Free'. On the other hand, something like someRequest :: (Text a) = T a - (U a - Dialogue) certainly is reasonable. Colin Runciman has noted that this makes existential types doubly desirable in the presence of type classes, and Odersky and Laufer have argued something similar. Cheers, -- P
Re: Array Indexing
! It is the responsibility of the programmer to enforce bounds ! checking when required in non-derived instances of class @Ix@. ! An implementation is not required to check that an index ! lies within the bounds of an array when accessing that array. The above is fine by me, but here is a more concise wording, which may do as well. ! It is the responsibility of the programmer to enforce bounds ! checking in non-derived instances of class @Ix@, if it is desired. Cheers, -- P
Re: The Great Integer Division Controversy
I gather the change you propose makes `div` consistent with SML and Miranda, and uses `quo` for what Scheme calls `quotient`. Sounds good to me. -- P
exit in PreludeIO
The function "exit" in PreludeIO would suit its purpose better if: (a) It wrote to "stderr" rather than "stdout", (b) It followed the error message with a newline. Easy and quick to change! What do people think? (Especially Paul and Joe.) -- P
functional language implementations
Here is my current list of Haskell implementations. If anyone has corrections or additions, please send them to me. Cheers, -- P HASKELL, Sun-3 and Sun-4 Glasgow Haskell by Cordy Hall, Kevin Hammond, Will Partain, Simon Peyton Jones, Phil Wadler compiler, implemented in Haskell, runs stand-alone Contact: Will Partain, University of Glasgow [EMAIL PROTECTED] Haskell Compiler Distribution Attn: Will Partain Department of Computing Science University of Glasgow Glasgow G12 8QQ SCOTLAND HASKELL, Sun-3, Sun-4, and Apollo Yale Haskell by Paul Hudak, John Peterson, and others compiler, implemented in T, a dialect of Scheme; runs on top of T Contact: John Perterson, Yale University [EMAIL PROTECTED] John Peterson Yale University Department of Computer Science New Haven, CT 06520 HASKELL, Sun-3, Sun-4, and others Chalmers Haskell-B compiler by Lennart Augustsson Contact: Lennart Augustsson, Chalmers University [EMAIL PROTECTED] GOFER, Sun-3, Sun-4, and PC's Gofer is a dialect of Haskell by Mark Jones interpreter, implemented in C Contact: Mark Jones, Oxford University [EMAIL PROTECTED] Mark Jones Programming Research Group 11 Keble Road Oxford, OX1 3QD UK
(n+k)
(n+k) patterns are still causing difficulties in the syntax.
I would be happy with the following:
On a lhs, only allow (n+k) patterns in arguments.
Thus
n+1 = ...
is ALWAYS a definition of (+), but
f (n+1) =
case m of {n+1 - ...}
are still allowed. Would that make life easier? -- P
Re: Literate comments
RFC-822-HEADERS: Original-Via: == We seem to be converging here. I prefer Simon's suggestion of an appendix to Paul's suggestion of a Section 1.6, but am not too bothered either way. Will also try to work in Simon's note about file extensions. I am happy to leave the question of how to format the Prelude in Joe's lap. I'll go ahead and draft the required page. Cheers, -- P
Literate comments
Despite Paul having ruled on the matter, the debate still rages, with about half saying that is wonderful, and half saying it is awful. Under these circumstances, Paul's ruling seems right: it is pointless to legislate as part of the language. On the other hand, the current circumstance is that the main implementations do all use the convention. It seems reasonable to say this in the report -- we should at least tell other implementors what the current implementors have settled upon. This would also let Joe use the convention in presenting the standard prelude, as he says he would like to do. To be precise: I propose an additional chapter of the report, labeled `Literate comments' and no more than one page long, that states a convention for providing literate comments, notes that it is NOT part of Haskell but is supported by existing implementations, and mentions that the Prelude is presented with this convention in the report. I volunteer to draft the page. Paul, as syntax honcho you should rule on this. Cheers, -- P PS: Wadler's Law: The emotional intensity of debate on a language feature increases as one moves down the following scale: Semantics, Syntax, Lexical syntax, Comments.
