When I vis­ited Cal­gary last, I explained my bounds infer­ence scheme to Brian. It took most of an entire day of solid explan­a­tions on the white­board before he under­stood what I was talk­ing about, but he didn’t have any sug­ges­tions for how to sim­plify it. “No this is right,” he said. “This is com­pletely the right way to do it.”

Some time later he said “my biggest worry is you’re going to do all this work and no one will ever be able to under­stand it.” Aside from myself, Brian is the per­son who under­stands this best in the world, so it’s dis­con­cert­ing that it took a day to explain it to him. I have low hopes that I’ll be able to put together a thesis which is under­stand­able to my com­mit­tee, but on the other hand I have high con­fid­ence in my teach­ing abil­it­ies, and what is writ­ing a thesis if not non-​​verbal teaching?

Pola is com­plex. The syn­tax and semantics are rather arcane, neces­sar­ily so: if there were any way to sim­plify it we would, and in fact we did put a few sim­pli­fic­a­tions in. The typ­ing sys­tem is mod­er­ately if you are well versed in type the­ory; if you don’t have a strong back­ground in type the­ory I can only ima­gine it appears as a tangled vine of thorny bushes, where each thorn is recurs­ively a tangled vine of thorny bushes some­how. The bounds infer­ence sys­tem is prob­ably even worse, though only because it hasn’t been done before and I’ve had to con­jure it from the ground up. I feel most con­fid­ent about the bounds infer­ence because it’s my biggest con­tri­bu­tion but also because it’ll be the easi­est to make self-​​contained and not have to worry about whatever nota­tion is con­ven­tional or canonical.

There are mul­tiple ver­sions of Pola, vari­ations I sup­pose, which I keep mostly in my head. My thesis is focused on the “polynomial-​​time with unfolds and with duplic­a­tion by peeks” vari­ant of Pola, which I think to be the most use­ful, though prob­ably the most annoy­ing to deal with. Most of the stuff I’ve writ­ten up I’m now rewrit­ing in a new nota­tion which will hope­fully be easier to understand.

A couple weeks ago my friend Angela came to my office and we chat­ted about theses. I don’t know whether to describe the pro­cess of writ­ing a thesis as van­ity or futil­ity. Maybe it’s just com­pul­sion. Whatever it is, it doesn’t seem totally sensical to con­sume so much effort and one’s twind­ling men­tal health into it. “Remem­ber: nobody cares” she said. It’s become a bit of a man­tra for me. Even if my work goes com­pletely for­got­ten and truly no one cares, I can’t help but pre­tend that people do any­way and do everything prop­erly. Every week I spend at least a couple pan­icked hours tying up loose ends that I’m entirely con­vinced no one would ever notice were loose to begin with. This dili­gence includes put­ting most of my days into dream­ing up ways to rep­res­ent things to make them easier to under­stand, even if no one fully will.

The fur­ther I get the more I notice the hacker part of me try­ing to over­take the aca­demic part of me. It’s tempt­ing to just strike out my entire chapter 3 and say “yeah ser­i­ously just down­load the soft­ware and play with it. You will learn more in 5 minutes of play­ing around than you will reread­ing this stu­pid chapter a hun­dred times”.

Man this entry soun­ded depress­ing. It’s all worth it when you do fin­ish a sec­tion, though. You do get a bit of a rush when you finally word some­thing really eleg­antly and you can visu­al­ize your com­mit­tee nod­ding along think­ing “well that’s clear. Why did put so much emphasis on some­thing that’s so simple?”

Check out the pic­ture gal­lery. Even though it was all cat­egory the­ory, and con­sequently I can fol­low almost none of the other talks, it’s still a won­der­ful con­fer­ence to go to. It’s a nice atmo­sphere, a good mix­ture of grad stu­dents, pro­fess­ors and pro­fess­ors emeriti.

After the con­fer­ence I stayed in Cal­gary for another couple weeks work­ing on my thesis and going through bounds infer­ence in detail with Brian. Unfor­tu­nately, and excit­ingly, we found a big prob­lem with the mix­ture of coin­duct­ive and induct­ive recur­sion which can take one out of poly­no­mial time. I may write on that more at some other time, but only after I think of a good way to describe it, at which point the first place it will appear is my thesis.

The fol­low­ing ffffff­fuuuuuuuuuuuu describes most of my life for this week:

I’m fly­ing out to Cal­gary Sunday morn­ing and then head­ing to Kana­nas­kis for FMCS. My code is already work­ing for many cases, but it’s not as com­plete as I’d like it to be. I’d like to do a proper demon­stra­tion of bounds infer­ence when I give my talk. It’s a pretty laid-​​back con­fer­ence so, truth be told, even if I don’t get it totally work­ing by then I can still just demo what I have, or just not demo at all.

I went to FMCS once before, in 2004 at the end of my under­grad. It’s a very nice con­fer­ence, less formal than most, which makes it a lot more fun and a lot more pro­duct­ive, I think. After the con­fer­ence I’ll be hanging around in Cal­gary for another week or so work­ing on my thesis and hanging out with the par­ents. Good times.

My visit this week to Cal­gary to work with Brian and Robin is com­ing to an end and has def­in­itely paid off again. We have another day at least of work ahead of us, but prob­ably not much more real work will get done by then since we still have the FOPARA paper to fin­ish up and get cam­era ready. But, just in the past couple of days we’ve already made tre­mend­ous pro­gress in improv­ing and sta­bil­iz­ing the lan­guage. It won’t be too much longer before “core Pola” is finalized.

I should say there was one inter­est­ing res­ult that Brian told me about. The peek con­struct is a unique con­struct to the lan­guage, which allows one to, under some restric­tions, break affine­ness, i.e., allows one to ref­er­ence a vari­able mul­tiple times to give the pro­gram­mer more express­ive­ness. It’s a del­ic­ate busi­ness since affine­ness is what keeps Pola pro­grams polynomial-​​time, par­tic­u­larly in the con­text of recur­sion. As it turns out, if you remove the recursion-​​symbol restric­tions on peeks — allow­ing recur­sion within the con­di­tion of a peek—but keep the other restric­tions on peeks, you exactly cap­ture PSPACE! We demon­strated this by chan­ging just a couple lines of code, allow­ing recur­sion, and cod­ing up QSAT to play with. (more…)

I sub­mit­ted the paper to FOPARA this after­noon. It’s not a fant­astic paper, but it’s not too bad. I prob­ably say that about every paper. The scheme we came up with for bounds infer­ence was slightly hair­ier than I’d hoped which means there were a lot of loose ends to track down while stay­ing within the page limit.

In any case I’m pretty excited about that being done. I can relax a bit and do more imple­ment­a­tion work before LCC.

On a note of annoy­ance, I put a link in the paper to the Pola pro­ject home only to find that Red­mine stopped work­ing about two days ago. Dream­host may have done an upgrade of Rails or some­thing, I’m not sure, but it’s a prob­lem I didn’t fore­see. I’ll have to try to fix it tonight or tomorrow.

My under­gradu­ate super­visor (from the Uni­ver­sity of Cal­gary), Robin Cock­ett, was in town today on a short visit. My two cur­rent super­visors, Robin and I spent the entire day in a friendly research meet­ing. I sup­pose the biggest bene­fit was the every­one got to meet each other, but we also covered a lot of ground on Pola and what we should be focus­ing on.

The first big change is that we’re going to, again, redo peeks and cases. Peeks and cases have long been a prob­lem with Pola and one which is, so far as I know, com­pletely unique to Pola. In a typ­ical func­tional lan­guage, case con­structs are no mat­ter at all: you have some datum and you case on it to see what it is (is it an empty list or a non-​​empty list?) and go on your way. In Pola things are not so neat and tidy: cent­ral to the work­ings of Pola is the idea that often you’re not allowed to ref­er­ence a vari­able more than once (lest you break out of poly­no­mial time). This restric­tion can be waived, very del­ic­ately, if you prom­ise to only “peek” at a value but not use it. The dis­tinc­tion between a case (“con­sum­ing” a value) and a peek has always been a bit awk­ward, but also very dan­ger­ous to play with if you don’t want to acci­dent­ally allow non-​​polynomial things slip­ping in. I think we’ve finally figured out a good scheme.

The second big change is dis­cuss­ing how to the bounds infer­ence. This is a huge one because hav­ing the com­piler infer bounds is, in my mind, the raison d’être for Pola. I’m almost done imple­ment­ing very loose, clumsy bounds. They’re cor­rect as upper bounds, but they’re so loose as to be nigh use­less. There will never be a per­fect solu­tion to get­ting totally tight bounds and I’m becom­ing increas­ingly aware that there is a huge trade-​​off between being able to get tight bounds on things and hav­ing to carry around a lot of typ­ing inform­a­tion that allows you to infer those bounds. This is what I’ll be spend­ing most of my time on in the near future.

As for the prob­lem I men­tioned last time about hav­ing to imple­ment my own poly­no­mial arith­metic: I just rewrote it myself and I’m happy with it. It works and it’s much cleaner than before.