An Angry Half-Dozen

HardwareLimitedandHarlequinbothmarket commercialMLcompilers,eachbootstrappedinML. Insomecorners,functionallanguagesbearareputationforgrossinefficiency,butthisreputationisoutof date.CodequalityrangesfromashadebetterthanCto anorderofmagnitudeworse,withthetypicalcasehoveringatafactoroftwoorsoslower.Oneexampleisthe 1AppearedinACMSIGPLANNotices33(2):25–30,February1998. Pseudoknotbenchmark,basedonanapplicationthatuses backtrackingsearchtodeterminethree-dimensionalproteinstructure.Alargenumberoffunctionallanguages werebenchmarkedagainstthisprogram,thebestrunning twotothreetimesslowerthantheequivalentC[12]. Thefunctionalcommunitysplitsintotwocamps.Lazy languagesevaluateargumentsondemand,andsorequire highlydisciplineduseofsideeffects;strictlanguages evaluateargumentseagerly,butmakeiteasiertoexploit sideeffects.Haskell,Miranda,andCleanarelazy;StandardML,Caml,Erlang,andSchemearestrict.Overthe pastfewyearstherehasbeenremarkableconvergence betweenthetwocommunities,andthePseudoknottests showlazya...

• Type: Journal
• Year: 1998
• Where: SIGPLAN
• Authors: Philip Wadler
• Keywords: HardwareLimitedandHarlequinbothmarket CommercialMLcompilers, SIGPLAN 1998, System Software, Thefunctionalcommunitysplitsintotwocamps.Lazy Languagesevaluateargumentsondemand, TheoremprovertoverifylivenesspropertiesofthearbitrationprotocolsinRunway.Verification Wasachievedbyahybridoftheorem-provinginHOLand Model-checkinginSMV.Thisapproachuncoverederrors