September 3, 2009 Edinburgh, Scotland Haskell’09 Proceedings of the 2009 ACM SIGPLAN Haskell Symposium Sponsored by: ACM SIGPLAN Co-located with: ICFP’09 The Association for Computing Machinery 2 Penn Plaza, Suite 701 New York, New York 10121-0701 Copyright © 2009 by the Association for Computing Machinery, Inc. (ACM). Permission to make digital or hard copies of portions of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyright for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permission to republish from: Publications Dept., ACM, Inc. Fax +1 (212) 869-0481 or <[email protected]>. For other copying of articles that carry a code at the bottom of the first or last page, copying is permitted provided that the per-copy fee indicated in the code is paid through the Copyright Clearance Center, 222 Rosewood Drive, Danvers, MA 01923. Notice to Past Authors of ACM-Published Articles ACM intends to create a complete electronic archive of all articles and/or other material previously published by ACM. If you have written a work that has been previously published by ACM in any journal or conference proceedings prior to 1978, or any SIG Newsletter at any time, and you do NOT want this work to appear in the ACM Digital Library, please inform [email protected], stating the title of the work, the author(s), and where and when published. ISBN: 978-1-60558-508-6 Additional copies may be ordered prepaid from: ACM Order Department PO Box 30777 New York, NY 10087-0777, USA Phone: 1-800-342-6626 (US and Canada) +1-212-626-0500 (Global) Fax: +1-212-944-1318 E-mail: [email protected] Hours of Operation: 8:30 am – 4:30 pm ET ACM Order Number 565097 Printed in the USA ii Foreword It is my great pleasure to welcome you to the 2nd ACM Haskell Symposium. This meeting follows the first occurrence of the Haskell Symposium last year and 11 previous instances of the Haskell Workshop. The name change reflects both the steady increase of influence of the Haskell Workshop on the wider community as well as the increasing number of high quality submissions. The Call for Papers attracted 31 submissions from Asia, Europe, North and South America, of which 12 were accepted. During the review period, each paper was evaluated by at least three Program Committee members, and many papers received an additional external review. Based on these reviews, the submissions were chosen during a five-day electronic PC meeting and judged on their impact, clarity and relevance to the Haskell community. Because of the constraints of a one-day workshop, many papers with valuable contributions could not be accepted. To accommodate more papers, the PC chose to allocate 25-minute presentation slots for 11 papers and allocate a 15-minute slot for one paper, a short experience report. The program also includes a tool demonstration and a discussion on the future of Haskell. Foremost, I would like to thank the authors of all submitted papers for their hard work. The Program Committee also deserves strong thanks for their efforts in selecting from the many excellent submissions, despite a tight review period. My gratitude goes to the external reviewers, for responding on short notice. Special thanks go to Andy Gill, chair of the 2008 Haskell Symposium, and the rest of the Steering Committee. The Conference Management System EasyChair was invaluable; my thanks to its lead developer Andrei Voronkov. Finally, my thanks go to Christopher Stone and Michael Sperber, the ICFP Workshop Co-Chairs, Graham Hutton, the ICFP General Chair, Lisa Tolles from Sheridan Printing, and ACM SIGPLAN for their support and sponsorship. Stephanie Weirich Haskell’09 Program Chair University of Pennsylvania iii Table of Contents Haskell 2009 Symposium Organization..............................................................................................vi Session 1 Session Chair: Janis Voigtlaender (TU Dresden) • Types Are Calling Conventions.....................................................................................................................1 Maximilian C. Bolingbroke (University of Cambridge), Simon L. Peyton Jones (Microsoft Research) • Losing Functions without Gaining Data – another look at defunctionalisation...................................13 Neil Mitchell, Colin Runciman (University of York, UK) Session 2 Session Chair: Jeremy Gibbons (University of Oxford) • Push-Pull Functional Reactive Programming...........................................................................................25 Conal M. Elliott (LambdaPix) • Unembedding Domain-Specific Languages...............................................................................................37 Robert Atkey, Sam Lindley, Jeremy Yallop (The University of Edinburgh) • Lazy Functional Incremental Parsing........................................................................................................49 Jean-Philippe Bernardy (Chalmers University of Technology & University of Gothenburg) • Roll Your Own Test Bed for Embedded Real-Time Protocols: A Haskell Experience.......................61 Lee Pike (Galois, Inc.), Geoffrey Brown (Indiana University), Alwyn Goodloe (National Institute of Aerospace) Session 3 Session Chair: Mark P. Jones (Portland State University) • A Compositional Theory for STM Haskell................................................................................................69 Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon (Microsoft Research) • Parallel Performance Tuning for Haskell..................................................................................................81 Don Jones Jr. (University of Kentucky), Simon Marlow, Satnam Singh (Microsoft Research) • The Architecture of the Utrecht Haskell Compiler..................................................................................93 Atze Dijkstra, Jeroen Fokker, S. Doaitse Swierstra (Universiteit Utrecht) Session 4 Session Chair: Simon Marlow (Microsoft Research) • Alloy: Fast Generic Transformations for Haskell..................................................................................105 Neil C. C. Brown, Adam T. Sampson (University of Kent) • Type-Safe Observable Sharing in Haskell...............................................................................................117 Andy Gill (The University of Kansas) • Finding the Needle: Stack Traces for GHC.............................................................................................129 Tristan O. R. Allwood (Imperial College), Simon Peyton Jones (Microsoft Research), Susan Eisenbach (Imperial College) Author Index................................................................................................................................................141 v Haskell 2009 Symposium Organization Program Chair: Stephanie Weirich (University of Pennsylvania, USA) Steering Committee Chair: Andres Löh (University of Bonn, Germany) Steering Committee: Gabriele Keller (University of New South Wales, Australia) Andy Gill (University of Kansas, USA) Doaitse Swierstra (Utrecht University, The Netherlands) Colin Runciman (University of York, UK) John Hughes (Chalmers and Quviq, Sweden) Program Committee: Jeremy Gibbons (Oxford University, UK) Bastiaan Heeren (Open Universiteit Nederland, The Netherlands) John Hughes (Chalmers and Quviq, Sweden) Mark Jones (Portland State University, USA) Simon Marlow (Microsoft Research, UK) Ulf Norell (Chalmers, Sweden) Chris Okasaki (United States Military Academy, USA) Ross Paterson (City University London, UK) Alexey Rodriguez Yakushev (Vector Fabrics, The Netherlands) Don Stewart (Galois, USA) Janis Voigtländer (TU Dresden, Germany) Additional reviewers: Niklas Broberg Bruno Oliveira Magnus Carlsson Lee Pike Jacome Cunha Riccardo Pucella Iavor Diatchki Claudio Russo Marko van Eekelen Peter Sewell Nate Foster Doaitse Swierstra Alex Gerdes Aaron Tomb Stefan Holdermans Jesse Tov Wolfgang Jeltsch Dimitrios Vytiniotis Jerzy Karczmarczuk Adam Wick John Launchbury Baltasar Trancon y Widemann Gavin Lowe Peter Wong Henrik Nilsson Sponsor: vi Types Are Calling Conventions MaximilianC.Bolingbroke SimonL.PeytonJones UniversityofCambridge MicrosoftResearch [email protected] [email protected] Abstract unacceptable performance penalties for a language like Haskell, because of the pervasive use of higher-order functions, currying, It is common for compilers to derive the calling convention of a polymorphism, and laziness. Fast function calls are particularly functionfromitstype.Doingsoissimpleandmodularbutmisses importantinafunctionalprogramminglanguage,socompilersfor manyoptimisationopportunities,particularlyinlazy,higher-order theselanguages–suchastheGlasgowHaskellCompiler(GHC)– functionallanguageswithextensiveuseofcurrying.Werestorethe typicallyuseamixtureofadhocstrategiestomakefunctioncalls lostopportunitiesbydefiningStrictCore,anewintermediatelan- efficient. guagewhosetypesystemmakesthemissingdistinctions:laziness Inthispaperwetakeamoresystematicapproach.Weoutline isexplicit,andfunctionstakemultipleargumentsandreturnmulti- anewintermediatelanguageforacompilerforapurelyfunctional pleresults. programminglanguage,thatisdesignedtoencodethemostimpor- Categories and Subject Descriptors D.3.1 [Programming Lan- tantaspectsofafunction’scallingconventiondirectlyinthetype guages]:FormalDefinitionsandTheory–Semantics; D.3.2[Pro- systemofaconciselambdacalculuswithasimpleoperationalse- gramming Languages]: Language Classifications – Applicative mantics. (functional) languages; D.3.4 [Programming Languages]: Pro- cessors–Optimization • We present Strict Core, a typed intermediate language whose types are rich enough to describe all the calling conventions GeneralTerms Languages,Performance that our experience with GHC has convinced us are valuable (Section3).Forexample,StrictCoresupportsuncurriedfunc- 1. Introduction tionssymmetrically,withbothmultipleargumentsandmultiple Intheimplementationofalazyfunctionalprogramminglanguage, results. imaginethatyouaregiventhefollowingfunction: • We show how to translate a lazy functional language like Haskell into Strict Core (Section 4). The source language, f ::Int →Bool →(Int,Bool) which we call FH, contains all the features that we are inter- Howwouldyougoaboutactuallyexecutinganapplicationoff to estedincompilingwell–laziness,parametricpolymorphism, twoarguments?Therearemanyfactorstoconsider: higher-orderfunctionsandsoon. • Howmanyargumentsaregiventothefunctionatonce?Oneat • Weshowthatthepropertiescapturedbytheintermediatelan- atime,ascurryingwouldsuggest?Asmanyareasavailableat guageexposeawealthofopportunitiesforprogramoptimiza- theapplicationsite?Someotheranswer? tion by discussing four of them – definition-site and use-site arity raising (Section 6.1 and Section 6.2), thunk speculation • Howdoesthefunctionreceiveitsarguments?Inregisters?On (Section 5.5) and deep unboxing (Section 5.6). These optimi- thestack?Bundledupontheheapsomewhere? sationswereawkwardorsimplyinaccessibleinGHC’searlier • Sincethisisalazylanguage,theargumentsshouldbeevaluated Coreintermediatelanguage. lazily.Howisthisachieved?Iff isstrictinitsfirstargument, canwedosomethingabitmoreefficientbyadjustingf andits Althoughourinitialcontextisthatoflazyfunctionalprogramming callers? languages,StrictCoreisacall-by-valuelanguageandshouldalso • How are the results returned to the caller? As a pointer to a besuitableforuseincompilingastrict,pure,languagesuchasTim- heap-allocatedpair?Orinsomeotherway? ber[1],orahybridlanguagewhichmakesuseofbothevaluation strategies. Theanswerstothesequestions(andothers)arecollectivelycalled Nosinglepartofourdesignisnew,andwediscussrelatedwork thecallingconventionofthefunctionf.Thecallingconventionof inSection7.However,thepiecesfittogetherverynicely.Forexam- afunctionistypicallydeterminedbythefunction’stypesignature. ple:thesymmetrybetweenargumentsandresults(Section3.1);the Thissufficesforalargely-first-orderlanguagelikeC,butitimposes useofn-aryfunctionstogetthunks“forfree”,includingso-called “multi-thunks” (Section 3.4); and the natural expression of algo- rithms and data structures with mixed strict/lazy behaviour (Sec- tion3.5). Permissiontomakedigitalorhardcopiesofallorpartofthisworkforpersonalor classroomuseisgrantedwithoutfeeprovidedthatcopiesarenotmadeordistributed forprofitorcommercialadvantageandthatcopiesbearthisnoticeandthefullcitation 2. Thechallengeweaddress onthefirstpage.Tocopyotherwise,torepublish,topostonserversortoredistribute tolists,requirespriorspecificpermissionand/orafee. InGHCtoday,typeinformationaloneisnotenoughtogetadefini- Haskell’09, September3,2009,Edinburgh,Scotland,UK. tivespecificationofafunction’scallingconvention.Thenextfew Copyright(cid:13)c 2009ACM978-1-60558-508-6/09/09...$5.00 sectionsdiscusssomeexamplesofwhatwelosebyworkingwith 1 theimprecise,conservativecallingconventionimpliedbythetype systemasitstands. Shorthand Expansion xn (cid:44) (cid:104)x ,...,x (cid:105) (n(cid:62)0) 1 n 2.1 Strictarguments x (cid:44) (cid:104)x ,...,x (cid:105) (n(cid:62)0) 1 n Considerthefollowingfunction: x (cid:44) (cid:104)x(cid:105) Singleton x,y (cid:44) (cid:104)x ,...,x ,y ,...,y (cid:105) Concatenation f ::Bool →Int 1 n 1 m f x =casex of True →...;False →... Figure1:Notationforsequences This function is certainly strict in its argument x. GHC uses this information to generate more efficient code for calls to f, using call-by-value to avoid allocating a thunk for the argument. insidiously-pervasivepropagationofad-hocarityinformation;and However,whengeneratingthecodeforthedefinitionoff,canwe thelatterimposesaperformancepenalty[2]. really assume that the argument has already been evaluated, and Forthehigher-ordercase,considerthewell-knownlist-combining hence omit instructions that checks for evaluated-ness? Well, no. combinatorzipWith,whichwemightwritelikethis: Forexample,considerthecall zipWith =λf ::(a →b →c).λxs::List a.λys::List b. map f [fibonacci 10,1234] casexs of Nil →Nil Sincemapisusedwithbothstrictandlazyfunctions,mapwillnot (Cons x xs(cid:48))→ usecall-by-valuewhencallingf.SoinGHCtoday,f isconserva- caseys of tive,andalwaystestsitsargumentforevaluated-nesseventhough Nil →Nil inmostcallstheansweris‘yes’. (Cons y ys(cid:48))→Cons (f x y)(zipWith f xs(cid:48) ys(cid:48)) Anobviousalternativewouldbetotreatfirst-ordercalls(where thecallsitecan“see”thedefinitionoff,andyoucanstaticallysee Thefunctionalargumentf isalwaysappliedtotwoarguments, thatyouruse-sitehasasatleastasmanyargumentsasthedefinition anditseemsashamethatwecannotsomehowcommunicatethat site demands) specially, and generate a wrapper for higher-order information to the functions that are actually given to zipWith callsthatdoestheargumentevaluation.Thatwouldwork,butitis so that they might be compiled with a less pessimistic calling fragile.Forexample,thewrapperapproachtoamapcallmightdo convention. somethinglikethis: 2.3 Optionally-strictsourcelanguages map (λx.casex of y →f y)[...] Leavingtheissueofcompilationaside,Haskell’ssource-leveltype Here, the case expression evaluates x before passing it to f, system is not expressive enough to encode an important class of to satisfy f’s invariant that its argument is always evaluated1. invariants about how far an expression has been evaluated. For But, alas, one of GHC’s optimising transformations is to rewrite example, you might like to write a function that produces a list case x of y → e to e[x/y], if e is strict in x. This transfor- ofcertainly-evaluatedInts,whichwemightwriteas[!Int].Wedo mation would break f’s invariant, resulting in utterly wrong be- notattempttosolvetheissuesofhowtoexposethisfunctionality haviour or even a segmentation fault – for example, if it lead to totheuserinthispaper,butwemakeafirststepalongthisroadby erroneouslytreatingpartofanunevaluatedvalueasapointer.GHC describinganintermediatelanguagewhichisabletoexpresssuch hasastrongly-typedintermediatelanguagethatissupposedtobe types. immune to segmentation faults, so this fragility is unacceptable. ThatiswhyGHCalwaysmakesaconservativeassumptionabout 2.4 Multipleresults evaluated-ness. In a purely functional language like Haskell, there is no direct Thegenerationofspuriousevaluated-nesschecksrepresentsan analogue of a reference parameter, such as you would have in obviouslostopportunityfortheso-called“dictionary”arguments an imperative language like C++. This means that if a function that arise from desugaring the type-class constraints in Haskell. wishes to return multiple results it has to encapsulate them in a Theseareconstructedbythecompilersoastobenon-bottoming, datastructureofsomekind,suchasatuple: and hence may always be passed by value regardless of how a functionusesthem.Canweavoidgeneratedevaluated-nesschecks splitList::[Int]→(Int,[Int]) forthese,withouttheuseofanyad-hocery? splitList xs =casexs of (y:ys)→(y,ys) 2.2 Multiplearguments Unfortunately,creatingatuplemeansthatyouneedtoallocate ablobofmemoryontheheap–andthiscanbearealperformance Considerthesetwofunctions: drag,especiallywhenfunctionsreturningmultipleresultsoccurin f x y =x +y tightloops. g x =letz =factorial 10in λy →x +y+z How can we compile functions which – like this one – return multipleresults,efficiently? Theyhavethesametype(Int →Int →Int),butweevaluate applicationsofthemquitedifferently–g canonlydealwithbeing 3. StrictCore appliedtooneargument,afterwhichitreturnsafunctionclosure, whereasf canandshouldbeappliedtotwoargumentsifpossible. We are now in a position to discuss the details of our proposed GHC currently discovers this arity difference between the two compilerintermediatelanguage,whichwecallStrictCoreANF2. functionsstatically(forfirst-ordercalls)ordynamically(forhigher- Strict CoreANF makes extensive useof sequences of variables, ordercalls).However,theformerrequiresanapparently-modestbut types, values, and terms, so we pause to establish our notation for sequences. We use angle brackets (cid:104)x ,x ,...,x (cid:105) to denote 1 2 n 1InHaskell,acaseexpressionwithavariablepatternislazy,butinGHC’s currentcompilerintermediatelanguageitisstrict,andthatisthesemantics 2ANFstandsforA-normalform,whichwillbeexplainedfurtherinSec- weassumehere. tion3.6 2 a possibly-empty sequence of n elements. We often abbreviate suchasequenceasxn or,wherenisunimportant,asx.Whenno Variables x,y,z ambiguityarisesweabbreviatethesingletonsequence(cid:104)x(cid:105)tojust x.AllthisnotationissummarisedinFigure1. TypeVariables α,β We also adopt the “variable convention” (that all names are unique) throughout this paper, and assume that whenever the en- Kinds vironmentisextended,thenameaddedmustnotalreadyoccurin κ ::= (cid:63) Kindofconstructedtypes theenvironment–α-conversioncanbeusedasusualtogetaround | κ→κ Kindoftypeconstructors thisrestrictionwherenecessary. 3.1 SyntaxofStrictCore Binders ANF b ::= x:τ Valuebinding StrictCore isahigher-order,explicitly-typed,purely-functional, ANF | α:κ Typebinding call-by-valuelanguage.InspirititissimilartoSystemF,butitis slightlymoreelaboratesothatitstypescanexpressarichervariety Types ofcallingconventions.Thekeydifferencefromanordinarytyped τ,υ,σ ::= T Typeconstructors lambdacalculus,isthis: | α Typevariablereferences A function may take multiple arguments simultaneously, | b→τ Functiontypes and(symmetrically)returnmultipleresults. | τ υ Typeapplication The syntax of types τ, shown in Figure 2, embodies this idea: a function type takes the form b → τ, where b is a sequence Atoms of binders (describing the arguments of the function), and τ is a a ::= x Termvariablereferences sequenceoftypes(describingitsresults).Herearethreeexample | (cid:96) Literals functiontypes: AtomsInArguments f1 : Int →Int g ::= a Valuearguments : (cid:104) :Int(cid:105)→(cid:104)Int(cid:105) | τ Typearguments f2 : (cid:104)α:(cid:63),α(cid:105)→α : (cid:104)α:(cid:63), :α(cid:105)→(cid:104)α(cid:105) Multi-valueTerms f3 : (cid:104)α:(cid:63),Int,α(cid:105)→(cid:104)α,Int(cid:105) e ::= a Returnmultiplevalues : (cid:104)α:(cid:63), :Int, :α(cid:105)→(cid:104)α,Int(cid:105) | letx:τ = eine Evaluation | valrecx:τ = vine Allocation f4 : α:(cid:63)→Int →α→(cid:104)α,Int(cid:105) | ag Application : (cid:104)α:(cid:63)(cid:105)→(cid:104)(cid:104) :Int(cid:105)→(cid:104)(cid:104) :α(cid:105)→(cid:104)α,Int(cid:105)(cid:105)(cid:105) | caseaof p → e Branchonvalues In each case, the first line uses simple syntactic abbreviations, which are expanded in the subsequent line. The first, f1, takes HeapAllocatedValues one argument and returns one result3. The second, f2, shows a v ::= λb.e Closures polymorphicfunction:StrictCoreusesthenotationofdependent | Cτ,a Constructeddata products, in which a single construct (here b → τ) subsumes both∀andfunctionarrow.HoweverStrictCoreisnotdependently Patterns typed, so that types cannot depend on terms: for example, in the p ::= Defaultcase type(cid:104)x:Int(cid:105) → (cid:104)τ(cid:105),theresulttypeτ cannotmentionx.Forthis | (cid:96) Matchesexactliteralvalue reason,wealwayswritevaluebindersintypesasunderscores“ ”, | Cx:τ Matchesdataconstructor andusuallyomitthemaltogether,writing(cid:104)Int(cid:105)→(cid:104)τ(cid:105)instead. The next example, f3, illustrates a polymorphic function that DataTypes takes a type argument and two value arguments, and returns two d ::= dataTα:κ=c| ... |c Datadeclarations results. Finally, f4 gives a curried version of the same function. c ::= Cτ Dataconstructors Admittedly, this uncurried notation is more complicated than the unarynotationofconventionalSystemF,inwhichallfunctionsare Programs d,e curried.Theextracomplexityiscrucialbecause,aswewillseein Section 3.3, it allows us to express directly that a function takes TypingEnvironments severalargumentssimultaneously,andreturnsmultipleresults. Γ ::= (cid:15) Emptyenvironment Thesyntaxofterms(alsoshowninFigure2)isdrivenbythe | Γ,x:τ Valuebinding sameimperatives.Forexample,StrictCoreANF hasn-aryapplica- | Γ,α:κ Typebinding tionag;andafunctionmayreturnmultipleresultsa.Apossibly- | Γ,C:b→(cid:104)Tα(cid:105) Dataconstructorbinding recursivecollectionofheapvaluesmaybeallocatedwithvalrec, | Γ,T:κ Typeconstructorbinding whereaheapvalueisjustalambdaorconstructorapplication.Fi- nally,evaluationisperformedbylet;sincethetermontheright- Syntacticsugar hand side may return multiple values, the let may bind multiple Shorthand Expansion values.Here,forexample,isapossibledefinitionoff3 above: Valuebinders τ (cid:44) :τ f3 =λ(cid:104)α:(cid:63),x:Int,y:α(cid:105).(cid:104)y,x(cid:105) Thunktypes {τ ,...,τ } (cid:44) (cid:104)(cid:105)→(cid:104)τ ,...,τ (cid:105) 1 n 1 n In support of the multi-value idea, terms are segregated into Thunkterms {e} (cid:44) λ(cid:104)(cid:105). e three syntactically distinct classes: atoms a, heap values v, and Figure2:SyntaxofStrictCore ANF 3RecallFigure1,whichabbreviatesasingletonsequence(cid:104)Int(cid:105)toInt 3 Γ(cid:96)κ τ : κ Γ(cid:96) a : τ a T:κ∈Γ B(T)=κ x:τ ∈Γ L((cid:96))=τ Γ(cid:96)κ T : κ TYCONDATA Γ(cid:96)κ T : κ TYCONPRIM Γ(cid:96) x : τ VAR Γ(cid:96) (cid:96) : τ LIT a a Γα(cid:96):κκα∈:Γκ TYVAR Γ(cid:96)b Γ: (cid:96)Γκ(cid:48) b∀→i.Γτ(cid:48) (cid:96):κ(cid:63)τi : (cid:63) TYFUN Γ(cid:96)e : τ ∀i.Γ(cid:96) a : τ Γ(cid:96)κ τ :Γκ1(cid:96)→κ τκυ2 :Γκ(cid:96)κ υ : κ1 TYCONAPP Γ(cid:96)aa :i τ i MULTI 2 Γ(cid:96)e : τ Γ,x:τ (cid:96)e : σ 1 2 LET Figure3:KindingrulesforStrictCoreANF Γ(cid:96)letx:τ = e1ine2 : σ ∀j.Γ,x:τ (cid:96) v : τ Γ,x:τ (cid:96)e : σ v j j 2 VALREC multi-valuetermse.Anatomaisatrivialterm–aliteral,variable Γ(cid:96)valrecx:τ = vine2 : σ reference, or (in an argument position) a type. A heap value v is Γ(cid:96) a : b→τ Γ(cid:96) b→τ @g : υ a app a heap-allocated constructor application or lambda term. Neither APP Γ(cid:96)ag : υ atomsnorheapvaluesrequireevaluation.Thethirdclassofterms is much more interesting: a multi-value term (e) is a term that Γ(cid:96) a : τ ∀i.Γ(cid:96) p → e : τ ⇒τ a scrut alt i i scrut eitherdiverges,orevaluatestoseveral(zero,one,ormore)values Γ(cid:96)caseaof p → e : τ CASE simultaneously. 3.2 StaticsemanticsofStrictCoreANF Γ(cid:96)v v : τ ThestaticsemanticsofStrictCore isgiveninFigure3,Figure4 Γ(cid:96)b : Γ(cid:48) Γ(cid:48) (cid:96)e : τ ANF LAM andFigure5.Despiteitsineluctablevolume,itshouldpresentfew Γ(cid:96) λb.e : b→τ v surprises.ThetermjudgementΓ(cid:96)e:τ typesamulti-valuedterm e,givingitamulti-typeτ.Therearesimilarjudgementsforatoms C:b→(cid:104)Tα(cid:105)∈Γ a,andvaluesv,exceptthattheypossesstypes(notmulti-types).An Γ(cid:96)app b→(cid:104)Tα(cid:105) @τ,a : (cid:104)υ(cid:105) importantinvariantofStrictCoreANF isthis:variablesandvalues Γ(cid:96) Cτ,a : υ DATA v have types τ, not multi-types τ. In particular, the environment Γ mapseachvariabletoatypeτ (notamulti-type). Γ(cid:96) p → e : τ ⇒τ Theonlyotherunusualfeatureisthetiresomeauxiliaryjudge- alt scrut mentΓ(cid:96) b→τ @g : υ,showninFigure5,whichcomputes Γ(cid:96)e : τ app DEFALT theresulttypeυthatresultsfromapplyingafunctionoftypeb→τ Γ(cid:96)alt → e : τscrut ⇒τ toargumentsg. L((cid:96))=τ Γ(cid:96)e : τ scrut The last two pieces of notation used in the type rules are for LITALT Γ(cid:96) (cid:96) → e : τ ⇒τ introducingprimitivesandareasfollows: alt scrut L Mapsliteralstotheirbuilt-intypes Γ,x:τ (cid:96) Cσ,x : (cid:104)Tσ(cid:105) v B Mapsbuilt-intypeconstructorstotheirkinds–thedo- Γ,x:τ (cid:96)e : τ mainmustcontainatleastallofthetypeconstructors CONALT Γ(cid:96) Cx:τ → e : Tσ⇒τ returnedbyL alt 3.3 OperationalsemanticsofStrictCoreANF Γ(cid:96)d : Γ StrictCoreANF isdesignedtohaveadirectoperationalinterpreta- Γ0 =Γ,T:κ1 →...→κm →(cid:63) tion, which is manifested in its small-step operational semantics, ∀i.Γ (cid:96)c : Tα:κminΓ i−1 i i giveninFigure7.Eachsmallstepmovesfromoneconfiguration Γ(cid:96)dataTα:κm =c | ... |c : Γ DATADECL toanother.Aconfigurationisgivenby(cid:104)H; e; Σ(cid:105),whereHrepre- 1 n n sentstheheap,eisthetermunderevaluation,andΣrepresentsthe stack–thesyntaxofstacksandheapsisgiveninFigure6. Γ(cid:96)c : Tα:κinΓ WedenotethefactthataheapHcontainsamappingfromxto ∀i.Γ(cid:96)κ τ : (cid:63) i aheapvaluev byH[x (cid:55)→ v].Thisstandsincontrasttoapattern DATACON Γ(cid:96)Cτ : Tα:κin (Γ,C:α:κ,τ →(cid:104)Tα(cid:105)) suchasH,x (cid:55)→ v,whereweintendthatH doesnotincludethe mappingforx ThesyntaxofStrictCoreiscarefullydesignedsothatthereisa (cid:96)d,e : τ 1–1correspondencebetweensyntacticformsandoperationalrules: Γ =(cid:15) ∀i.Γ (cid:96)d : Γ Γ (cid:96)e : τ 0 i−1 i i n • RuleEVALbeginsevaluationofamulti-valuedterme1,pushing (cid:96)dn,e : τ PROGRAM ontothestacktheframeletx:τ =•ine .Althoughitisapure 2 language,StrictCore usescall-by-valueandhenceevaluates ANF Figure4:TypingrulesforStrictCore e beforee .Ifyouwanttodelayevaluationofe ,useathunk ANF 1 2 1 (Section3.4). • Dually,ruleRETreturnsamultiplevaluetotheletframe,bind- ingthextothe(atomic)returnedvaluesa.Inthislatterrule,the simultaneoussubstitutionmodelstheideathate returnsmul- tion3.2)guaranteesthatthenumberofreturnedvaluesexactly 1 tiplevaluesinregisterstoitscaller.Thestaticsemantics(Sec- matchesthenumberofbinders. 4 EVAL (cid:104)H; letx:τ =e1ine2; Σ(cid:105) (cid:32) D(cid:104)H; e1; letx:τE=•ine2.Σ(cid:105) RET (cid:104)H; a; letx:τ =•ine2.Σ(cid:105) (cid:32) H; e2[a/x]; Σ D E ALLOC (cid:104)H; valrecx:τ =vine; Σ(cid:105) (cid:32) H,y(cid:55)→v[y/x]; e[y/x]; Σ y(cid:54)∈dom(H) BETA DH[x(cid:55)→λbn.e]; xan; ΣE (cid:32) DH; e[a/bn]; ΣE (n>0) ENTER (cid:104)H,x(cid:55)→λ(cid:104)(cid:105).e; x (cid:104)(cid:105); Σ(cid:105) (cid:32) (cid:104)H,x(cid:55)→ ; e; updatex.Σ(cid:105) UPDATE (cid:104)H; a; updatex.Σ(cid:105) (cid:32) (cid:104)H[x(cid:55)→I(cid:32)ND a]; a; Σ(cid:105) IND (cid:104)H[x(cid:55)→IND a]; x (cid:104)(cid:105); Σ(cid:105) (cid:32) (cid:104)H; a; Σ(cid:105) CASE-LIT ˙H; case(cid:96)of ...,(cid:96) → e,...; Σ¸ (cid:32) (cid:104)H; e; Σ(cid:105) CASE-CON DH[x(cid:55)→Cτ,an]; casexof ...,Cbn → e,...; ΣE (cid:32) DH; e[a/bn]; ΣE CASE-DEF (cid:104)H; caseaof ..., → e,...; Σ(cid:105) (cid:32) (cid:104)H; e; Σ(cid:105) Ifnoothermatch Figure7:OperationalsemanticsofStrictCore ANF numberofargumentsatthecallsiteexactlymatcheswhatthe Γ(cid:96)b : Γ functionisexpecting. Γ,α:κ(cid:96)b : Γ(cid:48) Rules CASE-LIT, CASE-CON, and CASE-DEF deal with pattern Γ(cid:96)(cid:104)(cid:105) : Γ BNDRSEMPTY Γ(cid:96)α:κ,b : Γ(cid:48) BNDRSTY mwiatthchthinugnk(sse(eSeScetciotinon3.43).5);while ENTER, UPDATE,and IND deal Γ(cid:96)κ τ : (cid:63) Γ,x:τ (cid:96)b : Γ(cid:48) BNDRSVAL 3.4 Thunks Γ(cid:96)x:τ,b : Γ(cid:48) BecauseStrictCore isacall-by-valuelanguage,ifweneedto ANF delay evaluation of an expression we must explicitly thunk it in Γ(cid:96)app b→τ @g : υ the program text, and correspondingly force it when we want to actuallyaccessthevalue. APPEMPTY Γ(cid:96)app (cid:104)(cid:105)→τ @ (cid:104)(cid:105) : τ Ifweonlycaredaboutcall-by-name,wecouldmodelathunk as a nullary function (a function binding 0 arguments) with type Γ(cid:96) a : σ Γ(cid:96) b→τ @g : υ a app APPVAL (cid:104)(cid:105) → Int. Then we could thunk a term e by wrapping it in a Γ(cid:96)app ( :σ,b)→τ @a,g : υ nullarylambdaλ(cid:104)(cid:105).e,andforceathunkbyapplyingitto(cid:104)(cid:105).This Γ(cid:96)κ σ : κ Γ(cid:96) `b→τ´[σ/α]@g : υ call-by-name approach would unacceptably lose sharing, but we app can readily turn it into call-by-need by treating nullary functions APPTY Γ(cid:96) (α:κ,b)→τ @σ,g : υ (henceforth called thunks) specially in the operational semantics app (Figure7),whichiswhatwedo: Figure5:Typingrulesdealingwithmultipleabstractionandappli- • In rule ENTER, an application of a thunk to (cid:104)(cid:105) pushes onto cation thestackathunkupdateframementioningthethunkname.It alsooverwritesthethunkintheheapwithablackhole( ),to expressthefactthatenteringathunktwicewithnointerv(cid:32)ening Heapvalues h ::= λb. e Abstraction update is always an error [3]. We call all this entering, or | Cτ,a Constructor forcing,athunk. | IND a Indirection • Whenthemachineevaluatestoaresult(avectorofatomsa), | Blackhole UPDATEoverwritestheblackholewithanindirectionIND a, (cid:32) pops the update frame, and continues as if it had never been Heaps H ::= (cid:15) | H,x(cid:55)→h there. Stacks Σ ::= (cid:15) • Finally,theINDruleensuresthat,shouldtheoriginalthunkbe enteredtoagain,thevaluesavedintheindirectionisreturned | updatex.Σ directly (remember – the indirection overwrote the pointer to | letx:τ =•ine.Σ thethunkdefinitionthatwasintheheap),sothatthebodyof Figure6:SyntaxforoperationalsemanticsofStrictCore thethunkisevaluatedatmostonce. ANF We use thunking to describe the process of wrapping a term e in a nullary function λ(cid:104)(cid:105).e. Because thunking is so common, we • Rule ALLOC performs heap allocation, by allocating one or use syntactic sugar for the thunking operation on both types and moreheapvalues,eachofwhichmaypointtotheothers.We expressions – if something is enclosed in {braces} then it is a modeltheheapaddressofeachvaluebyafreshvariableythat thunk.SeeFigure2fordetails. isnotalreadyusedintheheap,andfreshenboththevandeto AnunusualfeatureisthatStrictCore supportsmulti-valued reflectthisrenaming. ANF thunks,withatypesuchas(cid:104)(cid:105)→(cid:104)Int,Bool(cid:105),or(usingoursyntac- • RuleBETAperformsβ-reduction,bysimultaneouslysubstitut- ticsugar){Int,Bool}.Multi-thunksarosenaturallyfromtreating ingforallthebindersinonestep.Thissimultaneoussubstitu- thunksasaspecialkindoffunction,butthisadditionalexpressive- tion models the idea of calling a function passing several ar- nessturnsouttoallowustodoatleastonenewoptimisation:deep guments in registers. The static semantics guarantees that the unboxing(Section5.6). 5