Archive | Functional

# Pure Functional Memoization

There are many computation problems that resonate through the ages. Important Problems. Problems that merit a capital P.

The Halting Problem…

P versus NP…

The Fibonacci sequence…

The Fibonacci sequence is a super-important computation Problem that has vexed mathematicians for generations. It’s so simple!

``````fibs 0 = 0
fibs 1 = 1
fibs n = (fibs \$ n - 1) + (fibs \$ n - 2)``````

Done! Right? Let’s fire up ghci and find out.

``````*Fibs> fibs 10
55``````

… looking good…

``````*Fibs> fibs 40

``````

… still waiting…

``````
102334155
``````

… Well that sure took an unfortunate amount of time. Let’s try 1000!

``````*Fibs> fibs 1000
*** Exception: <<You died before this returned>>``````

To this day, science wonders what `fibs(1000)` is. Well today we solve this!

## Memoization

The traditional way to solve this is to use Memoization. In an imperative language, we’d create an array of size n, and prepopulate `arr[0] = 0` and `arr[1] = 1`. Next we’d loop over 2 to n, and for each we’d set `arr[i] = arr[i-1] + arr[i-2]`.

Unfortunately for us, this is Haskell. What to do… Suppose we had a map of the solutions for 0 to i, we could calculate the solution for i + 1 pretty easily right?

``````fibsImpl _ 0 = 0
fibsImpl _ 1 = 1
fibsImpl m i = (mo + mt)
where
mo = Map.findWithDefault undefined (i - 1) m
mt = Map.findWithDefault undefined (i - 2) m``````

We return 0 and 1 for i = 0 and i = 1 as usual. Next we lookup n – 1 and n – 2 from the map and return their sum. This is all pretty standard. But where does the map come from?

It turns out that this is one of those times that laziness is our friend. Consider this code:

``````fibs' n = let m = fmap (fibsImpl m)
(Map.fromList (zip [0..n]
[0..n])) in
Map.findWithDefault undefined n m``````

When I first saw this pattern (which I call the Wizard Pattern, because it was clearly invented by a wizard), I was completely baffled. We pass the thing we’re creating into the function that’s creating it? Unthinkable!

It turns out that this is just what we need. Because of laziness, the fmap returns immediately, and `m` points to an unevaluated thunk. So, for i = 0, and i = 1, fibsImpl will return 0 and 1 respectively, and the map will map 0 -> 0 and 1 -> 1. Next for i = 2, Haskell will attempt to lookup from the map. When it does this, it will be forced to evaluate the result of i = 0 and i = 1, and it will add 2 -> 1 to the map. This will continue all the way through i = n. Finally, this function looks up and returns the value of fibs n in linearish time. (As we all know, Map lookup isn’t constant time, but this is a lot better than the exponential time we had before)

So let’s try it out.

``````*Fibs> fibs' 1
1
*Fibs> fibs' 10
55
*Fibs> fibs' 40
102334155``````

… so far so good…

``````*Fibs> fibs' 100
354224848179261915075
*Fibs> fibs' 1000
43466557686937456435688527675040625802564660517371780402481729089536555417949051890403879840079255169295922593080322634775209689623239873322471161642996440906533187938298969649928516003704476137795166849228875
*Fibs> fibs' 10000
33644764876431783266621612005107543310302148460680063906564769974680081442166662368155595513633734025582065332680836159373734790483865268263040892463056431887354544369559827491606602099884183933864652731300088830269235673613135117579297437854413752130520504347701602264758318906527890855154366159582987279682987510631200575428783453215515103870818298969791613127856265033195487140214287532698187962046936097879900350962302291026368131493195275630227837628441540360584402572114334961180023091208287046088923962328835461505776583271252546093591128203925285393434620904245248929403901706233888991085841065183173360437470737908552631764325733993712871937587746897479926305837065742830161637408969178426378624212835258112820516370298089332099905707920064367426202389783111470054074998459250360633560933883831923386783056136435351892133279732908133732642652633989763922723407882928177953580570993691049175470808931841056146322338217465637321248226383092103297701648054726243842374862411453093812206564914032751086643394517512161526545361333111314042436854805106765843493523836959653428071768775328348234345557366719731392746273629108210679280784718035329131176778924659089938635459327894523777674406192240337638674004021330343297496902028328145933418826817683893072003634795623117103101291953169794607632737589253530772552375943788434504067715555779056450443016640119462580972216729758615026968443146952034614932291105970676243268515992834709891284706740862008587135016260312071903172086094081298321581077282076353186624611278245537208532365305775956430072517744315051539600905168603220349163222640885248852433158051534849622434848299380905070483482449327453732624567755879089187190803662058009594743150052402532709746995318770724376825907419939632265984147498193609285223945039707165443156421328157688908058783183404917434556270520223564846495196112460268313970975069382648706613264507665074611512677522748621598642530711298441182622661057163515069260029861704945425047491378115154139941550671256271197133252763631939606902895650288268608362241082050562430701794976171121233066073310059947366875
*Fibs> fibs' 100000
2597406934722172416615503402127591541488048538651769658472477070395253454351127368626555677283671674475463758722307443211163839947387509103096569738218830449305228763853133492135302679278956701051276578271635608073050532200243233114383986516137827238124777453778337299916214634050054669860390862750996639366409211890125271960172105060300350586894028558103675117658251368377438684936413457338834365158775425371912410500332195991330062204363035213756525421823998690848556374080179251761629391754963458558616300762819916081109836526352995440694284206571046044903805647136346033000520852277707554446794723709030979019014860432846819857961015951001850608264919234587313399150133919932363102301864172536477136266475080133982431231703431452964181790051187957316766834979901682011849907756686456845066287392485603914047605199550066288826345877189410680370091879365001733011710028310473947456256091444932821374855573864080579813028266640270354294412104919995803131876805899186513425175959911520563155337703996941035518275274919959802257507902037798103089922984996304496255814045517000250299764322193462165366210841876745428298261398234478366581588040819003307382939500082132009374715485131027220817305432264866949630987914714362925554252624043999615326979876807510646819068792118299167964409178271868561702918102212679267401362650499784968843680975254700131004574186406448299485872551744746695651879126916993244564817673322257149314967763345846623830333820239702436859478287641875788572910710133700300094229333597292779191409212804901545976262791057055248158884051779418192905216769576608748815567860128818354354292307397810154785701328438612728620176653953444993001980062953893698550072328665131718113588661353747268458543254898113717660519461693791688442534259478126310388952047956594380715301911253964847112638900713362856910155145342332944128435722099628674611942095166100230974070996553190050815866991144544264788287264284501725332048648319457892039984893823636745618220375097348566847433887249049337031633826571760729778891798913667325190623247118037280173921572390822769228077292456662750538337500692607721059361942126892030256744356537800831830637593334502350256972906515285327194367756015666039916404882563967693079290502951488693413799125174856667074717514938979038653338139534684837808612673755438382110844897653836848318258836339917310455850905663846202501463131183108742907729262215943020429159474030610183981685506695026197376150857176119947587572212987205312060791864980361596092339594104118635168854883911918517906151156275293615849000872150192226511785315089251027528045151238603792184692121533829287136924321527332714157478829590260157195485316444794546750285840236000238344790520345108033282013803880708980734832620122795263360677366987578332625485944906021917368867786241120562109836985019729017715780112040458649153935115783499546100636635745448508241888279067531359950519206222976015376529797308588164873117308237059828489404487403932053592935976454165560795472477862029969232956138971989467942218727360512336559521133108778758228879597580320459608479024506385194174312616377510459921102486879496341706862092908893068525234805692599833377510390101316617812305114571932706629167125446512151746802548190358351688971707570677865618800822034683632101813026232996027599403579997774046244952114531588370357904483293150007246173417355805567832153454341170020258560809166294198637401514569572272836921963229511187762530753402594781448204657460288485500062806934811398276016855584079542162057543557291510641537592939022884356120792643705560062367986544382464373946972471945996555795505838034825597839682776084731530251788951718630722761103630509360074262261717363058613291544024695432904616258691774630578507674937487992329181750163484068813465534370997589353607405172909412697657593295156818624747127636468836551757018353417274662607306510451195762866349922848678780591085118985653555434958761664016447588028633629704046289097067736256584300235314749461233912068632146637087844699210427541569410912246568571204717241133378489816764096924981633421176857150311671040068175303192115415611958042570658693127276213710697472226029655524611053715554532499750843275200199214301910505362996007042963297805103066650638786268157658772683745128976850796366371059380911225428835839194121154773759981301921650952140133306070987313732926518169226845063443954056729812031546392324981793780469103793422169495229100793029949237507299325063050942813902793084134473061411643355614764093104425918481363930542369378976520526456347648318272633371512112030629233889286487949209737847861884868260804647319539200840398308008803869049557419756219293922110825766397681361044490024720948340326796768837621396744075713887292863079821849314343879778088737958896840946143415927131757836511457828935581859902923534388888846587452130838137779443636119762839036894595760120316502279857901545344747352706972851454599861422902737291131463782045516225447535356773622793648545035710208644541208984235038908770223039849380214734809687433336225449150117411751570704561050895274000206380497967960402617818664481248547269630823473377245543390519841308769781276565916764229022948181763075710255793365008152286383634493138089971785087070863632205869018938377766063006066757732427272929247421295265000706646722730009956124191409138984675224955790729398495608750456694217771551107346630456603944136235888443676215273928597072287937355966723924613827468703217858459948257514745406436460997059316120596841560473234396652457231650317792833860590388360417691428732735703986803342604670071717363573091122981306903286137122597937096605775172964528263757434075792282180744352908669606854021718597891166333863858589736209114248432178645039479195424208191626088571069110433994801473013100869848866430721216762473119618190737820766582968280796079482259549036328266578006994856825300536436674822534603705134503603152154296943991866236857638062351209884448741138600171173647632126029961408561925599707566827866778732377419444462275399909291044697716476151118672327238679208133367306181944849396607123345271856520253643621964198782752978813060080313141817069314468221189275784978281094367751540710106350553798003842219045508482239386993296926659221112742698133062300073465628498093636693049446801628553712633412620378491919498600097200836727876650786886306933418995225768314390832484886340318940194161036979843833346608676709431643653538430912157815543512852077720858098902099586449602479491970687230765687109234380719509824814473157813780080639358418756655098501321882852840184981407690738507369535377711880388528935347600930338598691608289335421147722936561907276264603726027239320991187820407067412272258120766729040071924237930330972132364184093956102995971291799828290009539147382437802779051112030954582532888721146170133440385939654047806199333224547317803407340902512130217279595753863158148810392952475410943880555098382627633127606718126171022011356181800775400227516734144169216424973175621363128588281978005788832454534581522434937268133433997710512532081478345067139835038332901313945986481820272322043341930929011907832896569222878337497354301561722829115627329468814853281922100752373626827643152685735493223028018101449649009015529248638338885664893002250974343601200814365153625369199446709711126951966725780061891215440222487564601554632812091945824653557432047644212650790655208208337976071465127508320487165271577472325887275761128357592132553934446289433258105028633583669291828566894736223508250294964065798630809614341696830467595174355313224362664207197608459024263017473392225291248366316428006552870975051997504913009859468071013602336440164400179188610853230764991714372054467823597211760465153200163085336319351589645890681722372812310320271897917951272799656053694032111242846590994556380215461316106267521633805664394318881268199494005537068697621855231858921100963441012933535733918459668197539834284696822889460076352031688922002021931318369757556962061115774305826305535862015637891246031220672933992617378379625150999935403648731423208873977968908908369996292995391977217796533421249291978383751460062054967341662833487341011097770535898066498136011395571584328308713940582535274056081011503907941688079197212933148303072638678631411038443128215994936824342998188719768637604496342597524256886188688978980888315865076262604856465004322896856149255063968811404400429503894245872382233543101078691517328333604779262727765686076177705616874050257743749983775830143856135427273838589774133526949165483929721519554793578923866762502745370104660909382449626626935321303744538892479216161188889702077910448563199514826630802879549546453583866307344423753319712279158861707289652090149848305435983200771326653407290662016775706409690183771201306823245333477966660525325490873601961480378241566071271650383582257289215708209369510995890132859490724306183325755201208090007175022022949742801823445413711916298449914722254196594682221468260644961839254249670903104007581488857971672246322887016438403908463856731164308169537326790303114583680575021119639905615169154708510459700542098571797318015564741406172334145847111268547929892443001391468289103679179216978616582489007322033591376706527676521307143985302760988478056216994659655461379174985659739227379416726495377801992098355427866179123126699374730777730569324430166839333011554515542656864937492128687049121754245967831132969248492466744261999033972825674873460201150442228780466124320183016108232183908654771042398228531316559685688005226571474428823317539456543881928624432662503345388199590085105211383124491861802624432195540433985722841341254409411771722156867086291742124053110620522842986199273629406208834754853645128123279609097213953775360023076765694208219943034648783348544492713539450224591334374664937701655605763384697062918725745426505879414630176639760457474311081556747091652708748125267159913793240527304613693961169892589808311906322510777928562071999459487700611801002296132304588294558440952496611158342804908643860880796440557763691857743754025896855927252514563404385217825890599553954627451385454452916761042969267970893580056234501918571489030418495767400819359973218711957496357095967825171096264752068890806407651445893132870767454169607107931692704285168093413311046353506242209810363216771910420786162184213763938194625697286781413636389620123976910465418956806197323148414224550071617215851321302030684176087215892702098879108938081045903397276547326416916845445627600759561367103584575649094430692452532085003091068783157561519847567569191284784654692558665111557913461272425336083635131342183905177154511228464455136016013513228948543271504760839307556100908786096663870612278690274831819331606701484957163004705262228238406266818448788374548131994380387613830128859885264201992286188208499588640888521352501457615396482647451025902530743172956899636499615707551855837165935367125448515089362904567736630035562457374779100987992499146967224041481601289530944015488942613783140087804311431741858071826185149051138744831358439067228949408258286021650288927228387426432786168690381960530155894459451808735197246008221529343980828254126128257157209350985382800738560472910941184006084485235377833503306861977724501886364070344973366473100602018128792886991861824418453968994777259482169137133647470453172979809245844361129618997595696240971845564020511432589591844724920942930301651488713079802102379065536525154780298059407529440513145807551537794861635879901158192019808879694967187448224156836463534326160242632934761634458163890163805123894184523973421841496889262398489648642093409816681494771155177009562669029850101513537599801272501241971119871526593747484778935488777815192931171431167444773882941064615028751327709474504763922874890662989841540259350834035142035136168819248238998027706666916342133424312054507359388616687691188185776118135771332483965209882085982391298606386822804754362408956522921410859852037330544625953261340234864689275060526893755148403298542086991221052597005628576707702567695300978970046408920009852106980295419699802138053295798159478289934443245491565327845223840551240445208226435420656313310702940722371552770504263482073984454889589248861397657079145414427653584572951329719091947694411910966797474262675590953832039169673494261360032263077428684105040061351052194413778158095005714526846009810352109249040027958050736436961021241137739717164869525493114805040126568351268829598413983222676377804500626507241731757395219796890754825199329259649801627068665658030178877405615167159731927320479376247375505855052839660294566992522173600874081212014209071041937598571721431338017425141582491824710905084715977249417049320254165239323233258851588893337097136310892571531417761978326033750109026284066415801371359356529278088456305951770081443994114674291850360748852366654744869928083230516815711602911836374147958492100860528981469547750812338896943152861021202736747049903930417035171342126923486700566627506229058636911882228903170510305406882096970875545329369434063981297696478031825451642178347347716471058423238594580183052756213910186997604305844068665712346869679456044155742100039179758348979935882751881524675930878928159243492197545387668305684668420775409821781247053354523194797398953320175988640281058825557698004397120538312459428957377696001857497335249965013509368925958021863811725906506436882127156815751021712900765992750370228283963962915973251173418586721023497317765969454283625519371556009143680329311962842546628403142444370648432390374906410811300792848955767243481200090309888457270907750873638873299642555050473812528975962934822878917619920725138309388288292510416837622758204081918933603653875284116785703720989718832986921927816629675844580174911809119663048187434155067790863948831489241504300476704527971283482211522202837062857314244107823792513645086677566622804977211397140621664116324756784216612961477109018826094677377686406176721484293894976671380122788941309026553511096118347012565197540807095384060916863936906673786627209429434264260402902158317345003727462588992622049877121178405563348492490326003508569099382392777297498413565614830788262363322368380709822346012274241379036473451735925215754757160934270935192901723954921426490691115271523338109124042812102893738488167358953934508930697715522989199698903885883275409044300321986834003470271220020159699371690650330547577095398748580670024491045504890061727189168031394528036165633941571334637222550477547460756055024108764382121688848916940371258901948490685379722244562009483819491532724502276218589169507405794983759821006604481996519360110261576947176202571702048684914616894068404140833587562118319210838005632144562018941505945780025318747471911604840677997765414830622179069330853875129298983009580277554145435058768984944179136535891620098725222049055183554603706533183176716110738009786625247488691476077664470147193074476302411660335671765564874440577990531996271632972009109449249216456030618827772947750764777446452586328919159107444252320082918209518021083700353881330983215894608680127954224752071924134648334963915094813097541433244209299930751481077919002346128122330161799429930618800533414550633932139339646861616416955220216447995417243171165744471364197733204899365074767844149929548073025856442942381787641506492878361767978677158510784235702640213388018875601989234056868423215585628508645525258377010620532224244987990625263484010774322488172558602233302076399933854152015343847725442917895130637050320444917797752370871958277976799686113626532291118629631164685159934660693460557545956063155830033697634000276685151293843638886090828376141157732003527565158745906567025439437931104838571313294490604926582363108949535090082673154497226396648088618041573977888472892174618974189721700770009862449653759012727015227634510874906948012210684952063002519011655963580552429180205586904259685261047412834518466736938580027700252965356366721619883672428226933950325930390994583168665542234654857020875504617520521853721567282679903418135520602999895366470106557900532129541336924472492212436324523042895188461779122338069674233980694887270587503389228395095135209123109258159006960395156367736067109050566299603571876423247920752836160805597697778756476767210521222327184821484446631261487584226092608875764331731023263768864822594691211032367737558122133470556805958008310127481673962019583598023967414489867276845869819376783757167936723213081586191045995058970991064686919463448038574143829629547131372173669836184558144505748676124322451519943362182916191468026091121793001864788050061351603144350076189213441602488091741051232290357179205497927970924502479940842696158818442616163780044759478212240873204124421169199805572649118243661921835714762891425805771871743688000324113008704819373962295017143090098476927237498875938639942530595331607891618810863505982444578942799346514915952884869757488025823353571677864826828051140885429732788197765736966005727700162592404301688659946862983717270595809808730901820120931003430058796552694788049809205484305467611034654748067290674399763612592434637719995843862812391985470202414880076880818848087892391591369463293113276849329777201646641727587259122354784480813433328050087758855264686119576962172239308693795757165821852416204341972383989932734803429262340722338155102209101262949249742423271698842023297303260161790575673111235465890298298313115123607606773968998153812286999642014609852579793691246016346088762321286205634215901479188632194659637483482564291616278532948239313229440231043277288768139550213348266388687453259281587854503890991561949632478855035090289390973718988003999026132015872678637873095678109625311008054489418857983565902063680699643165033912029944327726770869305240718416592070096139286401966725750087012218149733133695809600369751764951350040285926249203398111014953227533621844500744331562434532484217986108346261345897591234839970751854223281677187215956827243245910829019886390369784542622566912542747056097567984857136623679023878478161201477982939080513150258174523773529510165296934562786122241150783587755373348372764439838082000667214740034466322776918936967612878983488942094688102308427036452854504966759697318836044496702853190637396916357980928865719935397723495486787180416401415281489443785036291071517805285857583987711145474240156416477194116391354935466755593592608849200546384685403028080936417250583653368093407225310820844723570226809826951426162451204040711501448747856199922814664565893938488028643822313849852328452360667045805113679663751039248163336173274547275775636810977344539275827560597425160705468689657794530521602315939865780974801515414987097778078705357058008472376892422189750312758527140173117621279898744958406199843913365680297721208751934988504499713914285158032324823021340630312586072624541637765234505522051086318285359658520708173392709566445011404055106579055037417780393351658360904543047721422281816832539613634982525215232257690920254216409657452618066051777901592902884240599998882753691957540116954696152270401280857579766154722192925655963991820948894642657512288766330302133746367449217449351637104725732980832812726468187759356584218383594702792013663907689741738962252575782663990809792647011407580367850599381887184560094695833270775126181282015391041773950918244137561999937819240362469558235924171478702779448443108751901807414110290370706052085162975798361754251041642244867577350756338018895379263183389855955956527857227926155524494739363665533904528656215464288343162282921123290451842212532888101415884061619939195042230059898349966569463580186816717074818823215848647734386780911564660755175385552224428524049468033692299989300783900020690121517740696428573930196910500988278523053797637940257968953295112436166778910585557213381789089945453947915927374958600268237844486872037243488834616856290097850532497036933361942439802882364323553808208003875741710969289725499878566253048867033095150518452126944989251596392079421452606508516052325614861938282489838000815085351564642761700832096483117944401971780149213345335903336672376719229722069970766055482452247416927774637522135201716231722137632445699154022395494158227418930589911746931773776518735850032318014432883916374243795854695691221774098948611515564046609565094538115520921863711518684562543275047870530006998423140180169421109105925493596116719457630962328831271268328501760321771680400249657674186927113215573270049935709942324416387089242427584407651215572676037924765341808984312676941110313165951429479377670698881249643421933287404390485538222160837088907598277390184204138197811025854537088586701450623578513960109987476052535450100439353062072439709976445146790993381448994644609780957731953604938734950026860564555693224229691815630293922487606470873431166384205442489628760213650246991893040112513103835085621908060270866604873585849001704200923929789193938125116798421788115209259130435572321635660895603514383883939018953166274355609970015699780289236362349895374653428746875``````

Neat. Even that last one only took a few seconds to return!

# Aeson Revisited

As many of you know, the documentation situation in Haskell leaves something to be desired. Sure, if you are enlightened, and can read the types, you’re supposedly good. Personally, I prefer a little more documentation than “clearly this type is a monoid in the category of endofunctors”, but them’s the breaks.

Long ago, I wrote about some tricks I found out about using Aeson, and I found myself using Aeson again today, and I’d like to revisit one of my suggestions.

## Types With Multiple Constructors

Last time we were here, I wrote about parsing JSON objects into Haskell types with multiple constructors. I proposed a solution that works fine for plain enumerations, but not types with fields.

Today I had parse some JSON into the following type:

``````data Term b a =
App b [Term b a]
| Var VarId
| UVar a``````

I thought “I’ve done something like this before!” and pulled up my notes. They weren’t terribly helpful. So I delved into the haddocs for Aeson, and noticed that Aeson's Result type is an instance of `MonadPlus`. Could I use `mplus` to try all three different constructors, and take whichever one works?

``````instance (FromJSON b, FromJSON a)
=> FromJSON (Term b a) where
parseJSON (Object v) = parseVar `mplus` parseUVar
`mplus` parseApp
where
parseApp = do
ident <- v .: "id"
terms <- v .: "terms"
return \$ App ident terms
parseVar = Var <\$> v .: "var"
parseUVar = UVar <\$> v .: "uvar"
parseJSON _ = mzero``````

It turns out that I can.

# Baby’s First Proof

Unlike many languages that you learn, in Coq, things are truly different. Much like your first functional language after using nothing but imperative languages, you have to re-evaluate things. Instead of just defining functions, you have to prove properties of them. So, let’s take a look at a few basic ways to do that.

## Simpl and Reflexivity

Here we have two basic “tactics” that we can use to prove simple properties. Suppose we have some function `addition`. We’re all familiar with how this works; `2 + 2 = 4`, right? Prove it:

``````Lemma two_plus_two:
2 + 2 = 4.
Proof.

First, what is this `Admitted.` thing? Admitted basically tells Coq not to worry about it, and just assume it is true. This is the equivalent of your math professor telling you “don’t worry about it, Aristotle says it’s true, are you calling Aristotle a liar?” and if you let this make it into live code, you are a bad person. We must make this right!

``````Lemma two_plus_two:
2 + 2 = 4.
Proof.
simpl.
reflexivity.
Qed.``````

That’s better. This is a simple proof; we tell Coq to simplify the expression, then we tell Coq to verify that the left-hand-side is the same as the right-hand-side. One nice feature of Coq is that lets you step through these proofs to see exactly how the evaluation is proceeding. If you’re using Proof General, you can use the buttons `Next`, `Goto`, and `Undo` to accomplish this. If you put the point at `Proof.` and click `Goto`, Coq will evaluate the buffer up to that point, and a window should appear at the bottom with the following:

``````1 subgoals, subgoal 1 (ID 2)

============================
2 + 2 = 4``````

This is telling you that Coq has 1 thing left to prove: ` 2 + 2 = 4`. Click next, the bottom should change to:

``````1 subgoals, subgoal 1 (ID 2)

============================
4 = 4``````

Coq processed the `simpl` tactic and now the thing it needs to prove is that `4 = 4`. Obviously this is true, so if we click next…

``No more subgoals.``

`reflexivity` should succeed, and it does. If we click next one more time:

``two_plus_two is defined``

This says that this Lemma has been defined, and we can now refer to it in other proofs, much like we can call a function. Now, you may be wondering “do I really have to simplify `2 + 2`?” No, you don’t, `reflexivity` will simplify on it’s own, this typechecks just fine:

``````Lemma two_plus_two:
2 + 2 = 4.
Proof.
reflexivity.
Qed.``````

So, what’s the point of `simpl` then? Let’s consider a more complicated proof.

## Induction

``````Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.``````

This lemma state that for any n, n + 0 = n. This is the same as when you’d write `∀` in some math. Other bits of new syntax is `n : nat`, which means that n has the type nat. The idea here is that no matter what natural number n is, n + 0 = n. So how do we prove this? One might be tempted to try:

``````Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.
Proof.
reflexivity.
Qed.``````

One would be wrong. What is Coq stupid? Clearly n + 0 = n, Aristotle told me so! Luckily for us, this is a pretty easy proof, we just need to be explicit about it. We can use induction to prove this. Let me show the whole proof, then we’ll walk through it step by step.

``````Lemma n_plus_zero_eq_n:
forall (n : nat), n + 0 = n.
Proof.
intros n.
induction n as [| n'].
{
reflexivity.
}
{
simpl.
rewrite -> IHn'.
reflexivity.
}
Qed.``````

Place the point at `Proof` and you’ll see the starting goal:

``````1 subgoals, subgoal 1 (ID 6)

============================
forall n : nat, n + 0 = n``````

Click next and step over `intros n.`

``````1 subgoals, subgoal 1 (ID 7)

n : nat
============================
n + 0 = n``````

What happened here is `intros n` introduces the variable n, and names it n. We could have done `intros theNumber` and the bottom window would instead show:

``````1 subgoals, subgoal 1 (ID 7)

theNumber : nat
============================
theNumber + 0 = theNumber``````

The `intros` tactic reads from left to right, so if we had some `Lemma foo : forall (n m : nat), [stuff]`, we could do `intros nName mName.`, and it would read in n, and bind it to nName, and then read in m and bind it to mName. Click next and evaluate `induction n as [| n'].`

``````2 subgoals, subgoal 1 (ID 10)

============================
0 + 0 = 0

subgoal 2 (ID 13) is:
S n' + 0 = S n'``````

The `induction` tactic implements the standard proof by induction, splitting our goal into two goals: the base case and the n + 1 case. Similarly to `intros`, this will create subgoals starting with the first constructor of an ADT, and ending with the last.

## On Natural Numbers in Coq

Let us take a second to talk about how numbers are represented in Coq. Coq re-implements all types within itself, so `nat` isn’t a machine integer, it’s an algebraic datatype of the form:

``````Inductive nat : Set :=
| O : nat
| S : nat -> nat.``````

`O` is zero, `S O` is one, and `S (S (S (O)))` is three. There is a lot of syntax sugar in place that lets you write 49 instead of `S (S ( ... ( S O) ... ))`, and that’s a good thing.

The point of all of this is that we can pattern match on `nat` much like we can a list.

## More Induction

…anyways, all this brings us back to induction and this mysterious `as [| n'].` What this is doing is binding names to all the fields of the ADT we are deconstructing. The `O` constructor takes no parameters, so there is nothing to the left of the `|`. The `S` constructor takes a `nat`, so we give it the name `n'`. Click next and observe the bottom change:

``````1 focused subgoals (unfocused: 1)
, subgoal 1 (ID 10)

============================
0 + 0 = 0``````

The curly braces “focuses” the current subgoal, hiding all irrelevant information. Curly braces are optional, but I find them to be very helpful as the bottom window can become very cluttered in large proofs. Here we see the base case goal being to prove that 0 + 0 = 0. Obviously this is true, and we can have Coq verify this by `reflexivity.` Click next until the next opening curly brace is evaluated. We see the next subgoal:

``````1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 13)

n' : nat
IHn' : n' + 0 = n'
============================
S n' + 0 = S n'``````

So, what do we have here? This is the n + 1 case; here the n’ in `S n'` is the original n. A particularly bored reader may try to prove `forall (n : nat), S n = n + 1` and I’ll leave that as an exercise. However, this follows from the definition of `nat`.

Also of note here is `IHn'`. `IH` stands for induction hypothesis, and this is that n’ + 0 = n’. So, how do we proceed? Click next and observe how the subgoal changes:

``````1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 15)

n' : nat
IHn' : n' + 0 = n'
============================
S (n' + 0) = S n'``````

It brought the `+ 0` inside the `S` constructor. Notice that now there is `n' + 0` on the left hand side. Click next and watch closely what happens:

``````1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 16)

n' : nat
IHn' : n' + 0 = n'
============================
S n' = S n'``````

Here we use the induction hypothesis to rewrite all occurrences of `n' + 0`, which was the left hand side of the induction hypothesis as `n'`, which was the right hand side of the induction hypothesis. This is what the `rewrite` tactic does. Notice now that the subgoal is `S n' = S n'` which `reflexivity` will surely find to be true. So, what would happen if we had done `rewrite <- IHn'.`?

``````1 focused subgoals (unfocused: 0)
, subgoal 1 (ID 16)

n' : nat
IHn' : n' + 0 = n'
============================
S (n' + 0 + 0) = S (n' + 0)``````

It rewrote all instances of `n'`, which was the right hand side of the induction hypothesis with `n' + 0` which was the left hand side of the induction hypothesis. Obviously, this isn’t what we want. I should note that you can undo this by rewriting to the right twice…

``````  {
simpl.
rewrite <- IHn'.
rewrite -> IHn'.
rewrite -> IHn'.
reflexivity.
}``````

…and it will technically work. But don’t do this, it’s silly and there’s no room for silliness in a rigorous mathematical proof.

Personally, I have a hard time keeping it straight what the left and right rewrites do. I sometimes find myself just trying one, and then the other if I guessed wrong. Think of it like this: `rewrite -> foo` rewrites the current goal, replacing all occurrences of the thing on the left hand side of the equation of `foo` with the thing on the right hand side of the equation. It changes from the left to the right. And vice-versa for `rewrite <-`, which changes from the right to the left.

# Getting Started With Coq and Proof General

Today we’ll be talking about Coq. Coq is a dependently typed programming language and theorem proof assistant. Given that I’ve just now got the toolchain installed, I’m hardly qualified to say much more than that. However, I am qualified to talk about installing the toolchain, which is precisely what I intend to do.

To get started with Coq, you’ll need the usual things: a properly configured editor and the Coq compiler. Installing these isn’t terribly difficult. First, let’s install the compiler. If you’re running Ubuntu, this is quite simple:

``\$ sudo apt-get install coq``

After this is done, you should have access to the compiler (`coqc`) and the REPL (`coqtop`):

``````\$ which coqc
/usr/bin/coqc
\$ which coqtop
/usr/bin/coqtop
\$ coqc --version
The Coq Proof Assistant, version 8.4pl4 (July 2014)
compiled on Jul 27 2014 23:12:44 with OCaml 4.01.0``````

OK! Now for the (slightly) harder part: our properly configured editor. Here we have two choices: CoqIDE or Proof General. CoqIDE is a simple IDE that ships with Coq, so if you’re satisfied with this, then feel free to stop reading now: CoqIDE comes with Coq and should be already installed at this point!

However, if you want to be truly cool, you’ll opt for Proof General. Proof General is an Emacs plugin. Unfortunately, Proof General is not available in Melpa, so we get to install it manually. Fortunately for us, Proof General is in the repos, so if you’re running Ubuntu you can just `apt-get` it:

``\$ sudo apt-get install proofgeneral proofgeneral-doc``

This will install Proof General, and set Emacs to load it up when you open a `.v` file. (My condolences to all those who write Verilog and Coq on the same machine) However, some configuration remains to be done. First fire up emacs and execute:

``M-x customize-group <enter> proof-general <enter>``

Expand `Proof Assistants` and ensure `Coq` is selected. Now open up a `.v` file and behold the glory!

Wait a minute, where’s my undo-tree? My rainbow-delimiters? My whitespace-mode? It’s not your imagination, Proof General has inexplicably ignored your fancy `.emacs` config. This is all a bit irritating, but you can work around it by re-adding these things to the `coq-mode-hook`:

``````(add-hook 'coq-mode-hook 'rainbow-delimiters-mode)

This is a bit of a sorry state of affairs, and if anybody reading this knows a better way I’d love to hear it. For now, I got my shinies back, so it’ll do.

Regardless, Proof General should be ready to go at this point. We are ready to continue our journey down the rabbit hole into wonderland… See you all on the other side!

# Random Operators: How to Make Friends and Influence Your Co-workers

If you were to ask me what language does operator overloading right, my unqualified answer would be Haskell. Unlike many languages, such as Rust or C++, operators aren’t these special things. They are just functions. Also, unlike many languages, you can define any arbitrary operator.

Now, ask me what I think is a major issue with Haskell. Do it. I dare you.

Well, if you insist…

A major issue I have with Haskell is that there are too many operators! Hundreds in base, and every library author thinks it’s ok to create hundreds more! Unfortunately, such is life; might as well get used to it.

There are two operators in particular that are quite prolific, and I think worthy of further discussion: `.` and `\$`.

## Function Composition

Here is the type of `.` :

``(.) :: (b -> c) -> (a -> b) -> a -> c``

`.` is the function composition operator. Take a function `f :: a -> b` and a function `g :: b -> c`, you can create a function `fg :: a -> c`:

``````fg :: a -> c
fg = g . f``````

You can chain these together too. Let `h :: c -> d`, `i :: d -> e`, and just for fun `j :: e -> a`:

``````funWithCategories :: a -> a
funWithCategories = j . i . h . g . f``````

Try it with your friends! They’ll love you!

I know, it was hard for me to write too, but I’ll be darned if it doesn’t look good! Just replace the `.` with “after”, and read it out loud:

``"j after i after h after g after f"``

Or, if you prefer to look at code:

``````funWithCategories :: a -> a
funWithCategories a = j (i (h (g (f a))))``````

… or in C:

``````a fun_with_categories(a input)
{
return j(i(h(g(f(input)))));
}``````

## Function Application

Now, let’s talk about `\$` the function application operator. Here is the type of `\$` :

``(\$) :: (a -> b) -> a -> b``

Basically it applied its right hand side argument to the left hand side function. Thus `show 1` is the same thing as `show \$ 1`. However, there’s a twist. Function application in Haskell is the highest precedence thing that can happen. This means that we often have to use a lot of parenthesis to make our code compile. Say I wanted to convert the output of `2 + 2`. This won’t work:

``````Prelude> show 2 + 2

<interactive>:25:8:
No instance for (Num String) arising from a use of ‘+’
In the expression: show 2 + 2
In an equation for ‘it’: it = show 2 + 2``````

What actuall happened was:

``(show 2) + 2``

…and that’s just silly. To make this code compile, we have to add parenthesis:

``````Prelude> show (2 + 2)
"4"``````

which is kind of annoying. However, we can use `\$` to eliminate these parenthesis!

``````Prelude> show \$ 2 + 2
"4"``````

The function application operator has a precedence of 0, so the addition happens first! It has a right fixity so you can chain it!

``````funWithOperators :: a -> a
funWithOperators a = j \$ i \$ h \$ g \$ f a``````

## Hey, I’ve Seen That Function Before!

If this looks familiar to you, then you’ve been paying attention!

``````(\$) ::             (a -> b) -> a -> b
(.) :: (b -> c) -> (a -> b) -> a -> c``````

If you chop off the first argument of `.` and squint, they kind of look the same. Logically, they can often be used interchangeably, however you will end up using some parenthesis with `.`.

Use `\$` if you’re trying to produce a value for use right now. If you find yourself doing something like this:

``show (show ( show( show "catcatcatcat")))``

… then change it to this and save yourself the hassle of counting parenthesis:

``show \$ show \$ show \$ show "catcatcatcat"``

Use `.` when you’re trying to make a function. If you find yourself doing something like this:

``````showWith :: (Show a) => (a -> String) -> a -> String
showWith = -- stuff

shower :: (Show a) => a -> String
shower a = show \$ show \$ show \$ show a

showWith shower "catcatcatcat"``````

… then you can avoid defining shower like so:

``showWith (show . show . show . show) "catcatcatcat"``

# Do We Really Need All These Monad Transformers?

Since I first learned about them, I’ve been a fan of Monad Transformers. Just stick them all together and we can pretend we’re writing Java, who doesn’t want that? Mutable State, Logging, Configuration, Exceptions, they’re all there. Heck, stick some IO in that if you like. Apparently, there’s even a pre-built Reader/Writer/State Monad in there. However, lately I’ve been working on a fairly large Haskell project, and this project doesn’t use Monad transformers. And you know what? It’s working out for them just fine.

Lately, I’ve been wondering if all these transformers are really worth the effort? After you’ve chained together some massive `runFoo (runBar (runBaz (runMonadRun ))) foobarbaz` function, and got it all working right and not returning some ridiculous nested tuple, what have you gained?

First up is `ReaderT`. `ReaderT` let’s us carry around a read-only configuration. In an `ReaderT` Monad, we can do the following:

``````foo :: (MonadReader c m) => a -> m b
foo a = do -- stuff
-- more stuff, presumably using config``````

…without having to have a config parameter on our function. This is nice because it improves readability. Right? Because this is so bad:

``````foo :: c -> a -> b
foo c a = -- stuff, presumably using config``````

“But `ReaderT` gets you `local`!” you say:

``````foo :: (MonadReader c m) => a -> m b
foo a = do -- stuff
local modifyC bar
where
modifyC c = -- change the config

Nifty, I agree. Or we chould just do:

``````foo :: c -> a -> b
foo c a = bar (modifyC c)
where
modifyC c = -- change the config
bar c = -- some function of c``````

…which I believe is much clearer, because I didn’t have to go to Hackage to figure out what `local` does.

## StateT

Conceptually kind of a combination of `ReaderT` and `WriterT` (I’m going to skip `WriterT` for the sake of brevity), `StateT` lets us use mutable state in a Monadic function:

``````foo :: (MonadState s m) => a -> m b
foo a = do state <- get
-- do stuff, presumably change the state
put state'
-- more stuff``````

So, what’s the non-monadic alternative? I imagine something like this:

``````foo :: s -> a -> (s, b)
foo s a = (s', a')
where
s' = -- do something to change the state
a' = -- do something using s'``````

I suppose that’d be workable, but now we have this tuple to deal with. We have a few options. We can do pattern matching:

``````bar :: a -> (s, b)
bar a = (s', b')
where
s = -- some initial state
(s', b) = foo s a
b' = -- do something, using b but not s'``````

…or we can use something like `uncurry`:

``````-- uncurry :: (a -> b -> c) -> (a, b) -> c

baz :: s -> a -> (s, b)
baz a = foo (uncurry \$ bar a)``````

Both of these are much harder to understand than the Monadic version in my opinion. For both, we have to shimmy our data to fit the interface, and these are just contrived examples.

## ExceptT

Finally, I’d like to talk about `ExceptT`. This monad lets us simulate exceptions. Unlike Haskell’s normal exception system, where exceptions can only be caught in `IO`, these exceptions can be caught within the `ExceptT` monad:

``````crud :: (MonadError String m) => a -> m b
crud a = throwError "Oh crud!"

-- doesn't catch
foo :: (MonadError String m) => a -> m c
foo a = do -- stuff
res <- curd a
-- doesn't make it this far

-- catches the exception
bar :: (MonadError String m) => a -> m c
bar a = do -- stuff
res <- catchError handler (crud a)
-- still rolling
where
handler e = -- exception handler``````

Seems reasonable right? Or, we could just use `Either`:

``````crud :: a -> Either String b
crud a = Left "Oh crud!"

-- must handle the error
foo :: a -> c
foo a = case (crud a) of
Left e -> -- handle error
Right c -> -- all good``````

Personally, I find these two to be a wash. Both are understandable. The Monadic version has the potential for the programmer to forget to handle the error, but the non-monadic version involved a noisy case statement.

## Not As Clear As It Seemed Before

As you can see, these things are hit and miss. Having thought about it while typing this out, if I had some function that just needed to read a config and throw an error, I’d probably define it like this:

``````foo :: c -> a -> Either String b
``````

…however, if I needed to throw some state in there:

``````foo :: (MonadReader c m,
a -> m b
``````

Suddenly the `ReaderT` and `StateT` become more attractive; why not throw them on the stack? I suppose the point is that maybe using a huge transformer isn’t the best way, not that it certainly isn’t the best way. Just some food for thought.

Lately, I’ve been working on parallelizing some Haskell. I’ve been furiously coding away, but at some point you have to stop “optimizing”, and see if you’ve actually accomplished anything.

Unfortunately, Haskell is kind of lazy, which makes benchmarking difficult. You could write some massive huge function, run it in `main`, and time it. Your time will likely be just above 0 seconds.

After some searching, it turns out that the answer is on Hackage. The Criterion package is a benchmarking library that can be used to effectively analyze performance. Using it could probably be simpler, but not by much!

## First a function:

Let’s optimize a function:

``````fibs :: Int -> Int
fibs 0 = 0
fibs 1 = 1
fibs n = fibs (n - 1) + fibs (n - 2)``````

Good old Fibonacci Sequence. As you likely know, this implementation isn’t very good. It starts to get slow at around 20, and at around 40, it’s runtime begins to be measurable in minutes. Let’s try to optimize it:

`````` Int -> Int
goodFibs 0 = 0
goodFibs 1 = 1
goodFibs n = goodFibs' (n, 2, 1, 0)
where
goodFibs' (to, count, n, nmo)
| to == count = n + nmo
| otherwise = goodFibs'
(to, (count + 1),
(n + nmo), n)``````

You may have seen an implementation like this before. The gimmick here is that instead of using the traditional recursive definition, we just count up to the nth position of the sequence. But is it actually faster? Let’s find out.

We can write a simple test bench for this. First, we need to `cabal install criterion`, then we are ready to go. Now, let’s write our test bench:

``````import Criterion.Main

main :: IO ()
main = defaultMain [bgroup "Good Fibs"
[bench "4" \$ nf goodFibs 4,
bench "15" \$ nf goodFibs 15,
bench "30" \$ nf goodFibs 30],
[bench "4" \$ nf fibs 4,
bench "15" \$ nf fibs 15,
bench "30" \$ nf fibs 30]]``````

There’s a fair amount going on here. Let’s walk through this function-by-function:

#### `defaultMain :: [Benchmark] -> IO ()`

This is a function that takes a list of benchmarks and runs them. This function allows you to pass arguments to Criterion to control its operation. A list of these options can be obtained by passing `--help` to the program.

#### `nf :: NFData b => (a -> b) -> a -> Benchmarkable`

This function takes a function from `a -> b`, and an `a`, and evaluates the function to normal form. This solves the laziness problem as a value that is evaluated to normal form is completely evaluated. You could also have used `whnf :: (a -> b) -> a -> Benchmarkable` to evaluate to weak head normal form. There are also IO versions of these functions.

#### `bench :: String -> Benchmarkable -> Benchmark`

This function takes a string, and a `Benchmarkable`, and returns a `Benchmark`. Nothing magical going on here; this is how you make a benchmark. The string is the name of your benchmark.

#### `bgroup :: String -> [Benchmark] -> Benchmark`

This function takes a string and a list of benchmarks, and returns a `Benchmark`. This allows you to group benchmarks. As you can see, I’ve grouped 3 separate calls to `fibs` and `goodFibs` using `bgroup`. As above, the string is the name of your benchmark group.

## Now, the payoff

So, how did I do? Let’s try it out. Build your program, and execute it. You should see something like this:

``````
benchmarking Good Fibs/4
time                 16.87 ns   (16.87 ns .. 16.88 ns)
1.000 R²   (1.000 R² .. 1.000 R²)
mean                 16.88 ns   (16.87 ns .. 16.88 ns)
std dev              7.316 ps   (5.814 ps .. 8.984 ps)

benchmarking Good Fibs/15
time                 29.59 ns   (29.57 ns .. 29.61 ns)
1.000 R²   (1.000 R² .. 1.000 R²)
mean                 29.62 ns   (29.61 ns .. 29.63 ns)
std dev              28.03 ps   (23.33 ps .. 33.59 ps)

benchmarking Good Fibs/30
time                 47.32 ns   (47.21 ns .. 47.43 ns)
1.000 R²   (1.000 R² .. 1.000 R²)
mean                 47.27 ns   (47.20 ns .. 47.35 ns)
std dev              231.7 ps   (210.4 ps .. 255.3 ps)

time                 33.35 ns   (33.34 ns .. 33.37 ns)
1.000 R²   (1.000 R² .. 1.000 R²)
mean                 33.37 ns   (33.35 ns .. 33.42 ns)
std dev              99.38 ps   (25.73 ps .. 205.0 ps)

time                 9.446 μs   (9.444 μs .. 9.448 μs)
1.000 R²   (1.000 R² .. 1.000 R²)
mean                 9.435 μs   (9.416 μs .. 9.444 μs)
std dev              41.64 ns   (3.462 ns .. 69.91 ns)

As you can see, my `goodFibs` does well. It grows mostly linearly with increasingly higher arguments, and all invocations take some amount of nanoseconds.
My `fibs` doesn’t do so well. `fibs 4` takes nanoseconds, `fibs 15` takes microseconds, and `fibs 30` takes milliseconds. Clearly `goodFibs` was worth the time put into it, and I’m not one of Knuth’s monsters. Yay me!