# 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.

My thoughts on Operator Overloading are hardly a secret. Some languages, such as Haskell, support it in a sane manner. Some languages, such as C++ don’t. Either way though, I’m not a fan.

That said, there is one case where I support it; when what you are trying to overload an operator to do makes sense for your type. In other words, if it makes sense to multiply an Employee object, feel free to overload the multiplication operator. Since we don’t usually model mating when we implement an employee object, I don’t usually approve.

## Multiplying a Fraction

However, if we have a fraction class, that has a numerator and denominator component, overloading the multiplication operator suddenly becomes reasonable:

``````frac<T> operator *(const frac<T> & rhs) const
{
return frac<T>(numer * rhs.numer, denom * rhs.denom);
};``````

In C++, many of the built in operators are available to be overloaded. You can do basically anything in an operator overload, but if you do, that makes you a bad person. Here we have a straightforward implementation, that I’m going to assume you don’t need to have explained to you. But let’s talk `const` correctness.

In this signature, the `const` appears twice. The right hand side argument is a `const` reference. Since this is a reference, no copy occurs, but with references can come mutability. The `const` here prevents any mutation from occurring. There is also a `const` at the end of the signature. That means that this function cannot modify the `this` pointer.

This function returns a new `frac<t>`, so no need for `const` there.

## Convert a Fraction to a Double

Next, you can overload the casting operator, and if you are a good person you’ll use this for type conversions. Let’s implement `(double)` for our fraction:

``````operator double() const
{
return (double) numer / denom;
}``````

This code is pretty straight forward. We divide the numerator by the denominator, and cast it to double in case integer division occurs. Cast operator overloads don’t have a return type, which is a bit strange but something we can work with.

## Streaming operators

Finally, I’d like to talk about streaming operator overloads. For any overloaded operator, there are two forms: member and non-member. Member overloads take `n - 1` arguments, where the minus 1 is the current object (and the left hand side). Non member overloads can’t access the this pointer, so they need to take the left hand side as a parameter.

Member overloads obviously have access to private class members, which makes them more powerful than non-member. Which leads us to the streaming operators. Streaming operators need to return `std::ostream &`, so they must be non-member. The problem is that we want to print the private numerator and denominator fields. The solution? make it a friend:

``````friend std::ostream & operator <<(std::ostream & lhs,
const frac<T> & rhs)
{
lhs << rhs.numer << '/' << rhs.denom;
return lhs;
};``````

With that problem solved, this function becomes pretty straight forward. We stream the fields, formatted correctly, into the left hand side `std::ostream &`, then we return the left hand side argument for further use by the next part of the streaming chain.

# Back in the Saddle with C++

Next quarter, I’ll be taking a graphics programming class. It was a year ago to the day that I last wrote about getting a makefile set up for OpenGL development. As you can imagine nothing came of it. Why? The obvious answer is that OpenGL is hard.

Secondary answers include the fact that almost all of the literature is assuming C++, and I was swimming against the tide trying to use C. Well, I won’t have a choice this time, the class is in C++, so I’m stuck with my old nemesis again.

What follows in the next few posts is an attempt to refamiliarize myself with C++. It’s been a while since I’ve done any significant work in C++ and a lot has happened. I’ll be going over a lot of basic stuff, so that I have a centralized crash course for myself when I’m stuck trying to remember if it’s `const &`, `& const`, `& const &`, or `co&n&st` (stranger things have happened).

## Namespaces

First up: namespaces. Namespaces are a formalization of the c convention of writing functions called stuff like `dmp_doStuff`. First we can declare our namespace:

``````namespace dmp
{
void doStuff()
}``````

…and we can call this function by doing `dmp::doStuff()`. This may involve an extra keystroke, but we can also use it like so:

``````using namespace dmp;

doStuff();
doStuff();
doStuff();

while (stuffUndone()) doStuff;
``````

## <Template> Classes

Now that we got that out of the way, let’s get into the meat of it: template classes. First up, due to some incredibly unfortunate reason, a C++ template class has to go in the header file. This sad fact is one of C++’s many transgressions against society, but we’ll not worry about that for now.

To declare a class (inside of a namespace if you’re a good citizen):

``````namespace dmp
{
template <typename T> class frac
{
public:
/* public stuff goes here */
private:
T numer;
T denom;
/* and your privates go here */
};
}``````

`template <typename T>` would be omitted if this weren’t a template class. Here we declare a class `frac` with one generic type `T`. Our class has two private fields of type `T`. As we all know, class members are private by default, but I don’t like to rely on “default behaviors”, so it doesn’t hurt to make it explicit. Let’s add some public constructors:

``````    frac(T inNumer, T inDenom)
: numer(inNumer), denom(inDenom)
{};

frac(const frac<T> & toCopy)
: numer(toCopy.numer), denom(toCopy.denom)
{};``````

Here we use initializer lists to populate the numerator and denominator. The first constructor takes two arguments of the same type (`T`), and the second is the copy constructor.

According to Microsoft, initializer lists are more efficient than assignment in the function body, which is why we prefer them here. There are certain cases where you must use an initializer list, and cases where you cannot use them. Your compiler will tell you if you mess this up.

``````    ~frac()
{};``````

Here we have a marvel of software engineering. Since we really don’t have anything to destroy, we can let it do nothing. It should be noted that this destructor is not virtual, so it’s not really safe to extend this class (more on this another day).

## Conclusion

Honestly, namespaces and constructors/destructors are two of my favorite features of C++. Simple, but helpful in eliminating boilerplate. I almost might be convinced to compile “C” with a C++ compiler to get these features. Coming up will be some features that I’m a bit more iffy about, such as operator overloading. however, when used appropriately, these things can also be good, more to come!

# 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"``