Lecture Notes in Computer Science 7241 CommencedPublicationin1973 FoundingandFormerSeriesEditors: GerhardGoos,JurisHartmanis,andJanvanLeeuwen EditorialBoard DavidHutchison LancasterUniversity,UK TakeoKanade CarnegieMellonUniversity,Pittsburgh,PA,USA JosefKittler UniversityofSurrey,Guildford,UK JonM.Kleinberg CornellUniversity,Ithaca,NY,USA AlfredKobsa UniversityofCalifornia,Irvine,CA,USA FriedemannMattern ETHZurich,Switzerland JohnC.Mitchell StanfordUniversity,CA,USA MoniNaor WeizmannInstituteofScience,Rehovot,Israel OscarNierstrasz UniversityofBern,Switzerland C.PanduRangan IndianInstituteofTechnology,Madras,India BernhardSteffen TUDortmundUniversity,Germany MadhuSudan MicrosoftResearch,Cambridge,MA,USA DemetriTerzopoulos UniversityofCalifornia,LosAngeles,CA,USA DougTygar UniversityofCalifornia,Berkeley,CA,USA GerhardWeikum MaxPlanckInstituteforInformatics,Saarbruecken,Germany Viktória Zsók Zoltán Horváth Rinus Plasmeijer (Eds.) Central European Functional Programming School 4th Summer School, CEFP 2011 Budapest, Hungary, June 14-24, 2011 Revised Selected Papers 1 3 VolumeEditors ViktóriaZsók EötvösLorándUniversity,FacultyofInformatics DepartmentofProgrammingLanguagesandCompilers PázmányPéterSétány1/C,1117Budapest,Hungary E-mail:[email protected] ZoltánHorváth EötvösLorándUniversity,FacultyofInformatics DepartmentofProgrammingLanguagesandCompilers PázmányPéterSétány1/C,1117Budapest,Hungary E-mail:[email protected] RinusPlasmeijer RadboudUniversity,ComputerandInformationSciencesInstitute Heyendaalseweg135,6525AJNijmegen,TheNetherlands E-mail:[email protected] ISSN0302-9743 e-ISSN1611-3349 ISBN978-3-642-32095-8 e-ISBN978-3-642-32096-5 DOI10.1007/978-3-642-32096-5 SpringerHeidelbergDordrechtLondonNewYork LibraryofCongressControlNumber:2012942467 CRSubjectClassification(1998):D.1.1,D.1.3,D.2,D.3.2 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©Springer-VerlagBerlinHeidelberg2012 Thisworkissubjecttocopyright.Allrightsarereserved,whetherthewholeorpartofthematerialis concerned,specificallytherightsoftranslation,reprinting,re-useofillustrations,recitation,broadcasting, reproductiononmicrofilmsorinanyotherway,andstorageindatabanks.Duplicationofthispublication orpartsthereofispermittedonlyundertheprovisionsoftheGermanCopyrightLawofSeptember9,1965, initscurrentversion,andpermissionforusemustalwaysbeobtainedfromSpringer.Violationsareliable toprosecutionundertheGermanCopyrightLaw. Theuseofgeneraldescriptivenames,registerednames,trademarks,etc.inthispublicationdoesnotimply, evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevantprotectivelaws andregulationsandthereforefreeforgeneraluse. Typesetting:Camera-readybyauthor,dataconversionbyScientificPublishingServices,Chennai,India Printedonacid-freepaper SpringerispartofSpringerScience+BusinessMedia(www.springer.com) Preface Thisvolumepresentstherevisedlecturenotesofselectedtalksgivenatthefourth Central European Functional Programming School, CEFP 2011, held during June 14–24, in Budapest (Hungary) at E¨otv¨os Lora´nd University, Faculty of Informatics. Thesummerschoolwasorganizedinthespiritoftheadvancedprogramming schools. CEFP involves an ever-growing number of students, researchers, and teachersfromacrossEurope,providingopportunitiesespeciallyforstudentsfrom Central, and Eastern Europeancountries. The intensive program offered a creative, inspiring environment for presen- tations and exchange of ideas on new specific programming topics. The lec- turescoveredawiderangeofdistributedandmulticorefunctionalprogramming subjects. We are very grateful to the lecturers and researchers for the time and effort they devoted to their talks and lecture notes. The lecture notes were each care- fullycheckedbyreviewersselectedfromexpertsonfunctionalprogramming.The papers were revisedby the lecturers based on the reviews.This revisionprocess guaranteedthat only high-quality papers were accepted for the volume. The last two papers in the volume are selectedpapers of the PhD Workshop organizedfor the participants of the summer school. Wewouldliketoexpressourgratitudefortheworkofallthemembersofthe ProgramCommittee and the Organizing Committee. Thewebsiteforthesummerschoolcanbefoundat:http://plc.inf.elte.hu/cefp/. March 2012 Vikto´ria Zso´k Zolt´an Horva´th Rinus Plasmeijer Organization CEFP 2011 was organized by E¨otv¨os Lora´nd University, Budapest, Hungary, and Pannonia Tourist Service, Budapest, Hungary. Sponsoring Institutions The summer school was supported by the: – Erasmus Intensive Programme (IP) Project No. ERA-IP2010/11 10/0242- E/4006 – CEEPUS program via the CEEPUS CII-HU-19 Network – EricssonHungary – Morgan Stanley Hungary The scientific editorialprocessof the summer schoolproceedings wassupported by the European Union and co-financed by the European Social Fund (Grant Agreement no. TAMOP 4.2.1/B-09/1/KMR-2010-0003). Table of Contents A ProgrammingTutor for Haskell.................................. 1 Johan Jeuring, Alex Gerdes, and Bastiaan Heeren Defining Multi-user Web Applications with iTasks.................... 46 Rinus Plasmeijer, Peter Achten, Bas Lijnse, and Steffen Michels Reasoning about I/O in Functional Programs........................ 93 Andrew Butterfield Eden — ParallelFunctional Programmingwith Haskell ............... 142 Rita Loogen Single Assignment C (SAC): High Productivity Meets High Performance..................................................... 207 Clemens Grelck Reasoning about Multi-process Systems with the Box Calculus ........ 279 Greg Michaelson and Gudmund Grov Paralleland Concurrent Programming in Haskell..................... 339 Simon Marlow Feldspar: Application and Implementation .......................... 402 Emil Axelsson and Mary Sheeran Static Analysis of Complex Software Systems Implemented in Erlang ... 440 Melinda To´th and Istv´an Boz´o Extending Little Languages into Big Systems........................ 499 Ga´bor P´ali Some New Approaches in Functional Programming Based on Categories ...................................................... 517 Viliam Slodiˇc´ak, Pavol Macko, and Valerie Novitzk´a Author Index.................................................. 533 A Programming Tutor for Haskell Johan Jeuring1,2, Alex Gerdes1, and Bastiaan Heeren1 1 School of Computer Science, Open Universiteit Nederland, P.O. Box 2960, 6401 DL Heerlen, The Netherlands {jje,age,bhr}@ou.nl 2 Department of Information and Computing Sciences, Universiteit Utrecht Abstract. Intheselectureswewillintroduceaninteractivesystemthat supportswritingsimplefunctionalprograms.Usingthissystem,students learning functional programming: – develop theirprograms incrementally, – receive feedback about whetheror not they are on the right track, – can ask for a hint when they are stuck, – see how a complete program is stepwise constructed, – get suggestions about how to refactor their program. The system itself is implemented as a functional program, and uses fundamental concepts such as rewriting, parsing, strategies, program transformations and higher-order combinators such as the fold. We will introducetheseconcepts,andshow howtheyareused intheimplemen- tation of theinteractive functional programming tutor. 1 Introduction Howdoyouwriteafunctionalprogram?HowcanIlearnit?Ouranswertothese questionsdependsonwhoisasking.Ifitisafirst-yearbachelorcomputerscience student who just finished an introductory object-oriented programming course, we would start with explaining the basic ideas of functional programming, and setmanysmallfunctionalprogrammingexercisesforthestudenttosolve.Ifitis a starting computer science Ph.D. student with a basic knowledge of functional programming,wewouldtakeaseriouspieceofsoftwaredevelopedinafunctional programming language, analyse it, discuss the advanced concepts used in the implementation, and set a task in which the software is extended or changed. These answers are based on our (and others) experience as teachers: there is no final answer (yet) to the question how programming is learned best, and what makes programming hard [Fincher and Petre, 2004]. We borrow from research thatstudieshowcomplexcognitiveskillsarelearned,inwhichtheimportanceof providing worked-outexamples [Merri¨enboer and Paas, 1990], giving hints, and giving immediate feedback on actions of students [Hattie and Timperley, 2007] is emphasised. These lecture notes address the question ‘How do youwrite a functional pro- gram’ with the audience of advanced graduate students or starting Ph.D. stu- dents in mind. The serious piece of software addresses the same question: ‘How V.Zso´k,Z.Horva´th,andR.Plasmeijer(Eds.):CEFP2011,LNCS7241,pp.1–45,2012. (cid:2)c Springer-VerlagBerlinHeidelberg2012 2 J. Jeuring, A. Gerdes, and B. Heeren do you write a functional program?’, but now with a first-year bachelor stu- dent computer science in mind. We will introduce an intelligent functional pro- grammingtutoringsystemforHaskell[Peyton Jones et al.,2003], usingwhicha student can: – develop a program incrementally, – receive feedback about whether or not she is on the right track, – ask for a hint when she is stuck, – can see how a complete program is stepwise constructed, – get suggestions about how to refactor her program. As far as we are aware, this is the first intelligent tutoring system for Haskell. The implementation of the intelligent functional programming tutor uses many advanced functional programming concepts. To support incremental de- velopment of programs and refactoring, the tutor uses rewrite and refinement rules. To give feedback about whether or not a student is on the right track the tutor uses strategies to describe the various solutions, and parsing to follow the student’s behaviour. To give hints to a student that is stuck, the system usesseveralanalysisfunctions onstrategies,viewingastrategyasacontext-free grammar. These notes will introduce all of these concepts. Thesenotesareorganisedasfollows.Section2introducesourintelligentfunc- tionalprogrammingtutorbymeansofsomeexampleinteractions.Section3gives the architectureofthe softwarefor the tutor.Section4discussesrewriteandre- finement rules and shows how they are used in the tutor. Section 5 introduces strategies for solving functional programming problems. Section 6 introduces our strategy language. Section 7 shows how we use techniques from parsing to follow student behaviour, and to give hints to a student that is stuck. Section 8 discusses related and future work, and concludes. 2 A Programming Tutor for Haskell This section introduces our intelligent functional programming tutoring system by means of some interactions of a hypothetical student with the tutor. The functional programming tutor is an example of an intelligent tutoring system for the domain of functional programming. An intelligent tutoring system is an environment that sets tasks for a student, and offers support to the student when solving these tasks, by means of hints, corrections, and worked-out so- lutions [VanLehn, 2006]. So the intelligent functional programming tutor sets smallfunctional programmingtasks,andgivesfeedbackininteractionswiththe student. 2.1 Reverse Elisajuststartedacourseonfunctionalprogramming,andhasattendedlectures onhowtowritesimplefunctionalprogramsonlists.Herteacherhassetacouple A Programming Tutorfor Haskell 3 Fig.1. The web-based functional programming tutor 1 of exercises from H-99: Ninety-nine Haskell Problems , in particular problem 5: reverse a list. We now show a couple of possible scenarios in which Elisa interacts with the tutor to solve this problem. A screenshot of the tutor is shown in Figure 1. At the start of a tutoring session the tutor gives a problem description: Write a function that reverses a list. For example: Data.List(cid:2) reverse"A man, a plan, a canal, panama!" "!amanap ,lanac a ,nalp a ,nam A" Data.List(cid:2) reverse[1,2,3,4] [4,3,2,1] and displays the name of the function to be defined: reverse=⊥ The task of a student is to refine the incomplete parts, denoted by ⊥, of the program. The symbol ⊥ is used as a placeholder for a hole in a program that needstoberefinedtoacompleteprogram.Astudentcanusesuchholestodefer the refinementofpartsoftheprogram.After eachrefinement,astudentcanask thetutorwhetherornottherefinementisbringinghimorherclosertoacorrect solution,or,ifthestudentdoesn’tknowhowtoproceed,askthetutorforahint. Besides holes, a student can also introduce new declarations, function bindings, alternatives, and refine patterns. 1 http://www.haskell.org/haskellwiki/99_Haskell_exercises 4 J. Jeuring, A. Gerdes, and B. Heeren Suppose Elisa has no idea where to start and asks the tutor for help. The tutor offers several ways to help a student. For example, it can list all possible ways to proceed solving an exercise. In this case, the tutor would respond with: There are several ways you can proceed: – Introduce a helper function that uses an accumulating parameter. – Implement reverse using the foldl function. – Use explicit recursion. We assume here that a student has some means to obtain information about concepts such as accumulated parameters that are mentioned in the feedback texts given by the tutor. This information might be obtained via lectures, an assistant, or lecture notes, or might even be included in the tutor at some later stage. Among the different possibilities, the tutor can make a choice, so if Elisa doesn’t want to choose, but just wants a single hint to proceed, she gets: Introduce a helper function that uses an accumulating parameter. Here weassume thatthe teacherhas setupthe tutor to preferthe solutionthat uses a helper function with an accumulating parameter. Elisa can ask for more detailedinformationatthispoint,andthetutorrespondswithincreasingdetail: Define function reverse in terms of a function reverse’, which takes an extra parameter in which the reversed list is accumulated. with the final bottom-out hint: Define: reverse=reverse(cid:4) ⊥ wherereverse(cid:4) acc=⊥ Atthis point, Elisacanrefinethe functionatmultiple positions. Inthis exercise we do not impose an order on the sequence of refinements. However, the tutor offers a teacher the possibility to enforce a particular order of refinements. Sup- (cid:4) posethatElisachoosestoimplementreverse bypatternmatchingonthesecond argument, which is a list, starting with the empty list case: (cid:4) reverse=reverse [] where reverse(cid:4) acc[] = ⊥ (cid:4) Note that this step consists of two smaller steps: the argument to reverse has (cid:4) beeninstantiatedto [], andthe definitionofreverse gotanextraargument.She continues with: (cid:4) reverse=reverse [] where (cid:4) reverse acc[] = [] The tutor responds with: Incorrect [] in the right hand side of reverse’ on line 3