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.

I’m going to be going to attend­ing FMCS 2010 in Kana­nas­kis — not far from Cal­gary — in a couple weeks. I’ll be giv­ing a talk on the imple­ment­a­tion of Pola in some capa­city, though I haven’t figured out how broadly scoped or what to focus on.

I’m get­ting pretty psyched about it. The con­fer­ence will be fun if it’s any­thing like I remem­ber FMCS 2004 to be. The loc­a­tion is amaz­ing. Plus after that I get to spend some time in Cal­gary with my par­ents and hanging out with Brian and, prob­ably most import­antly but least awe­somely, work­ing on my thesis.

This is a follow-​​up to this post. Mark was mag­nan­im­ously amaz­ing and bought an Itanium machine for “the lab”. It’s cur­rently sit­ting in my apart­ment. I’ll make another post tomor­row, I expect, where I actu­ally get to play with it prop­erly, but I thought at the very least I’d make a post about the head­aches of actu­ally get­ting it working.

Go through the pic­tures and read the run­ning com­ment­ary because I’m not going to repeat the pic­tures here.

Sadly the machine is noisy and relatedly prob­ably quite a power sucker. It’s in the corner of the liv­ing room, not far from where Jasna’s office is so I’m not going to be able to leave it on very often, I don’t think. The noise would prob­ably drive Jasna crazy.

I should say I still haven’t got a chance to really sit down and play with it — namely play with the assem­bler — like I planned because HP-​​UX needs so much more set­ting up. I’m going to have to install pretty well the entire GNU user­land because HP’s user­land is abso­lute garbage.

Through red­dit I found the story of The Ghost in the Machine, the story of a man who had a ghostly vis­ion, a grey blob out of the corner of his eye. I won’t retell the whole story, but he even­tu­ally tracked it down to a 19Hz stand­ing wave where he’d had the sight­ing. 19Hz is sus­pi­ciously close to what is doc­u­mented to be the res­on­ant fre­quency of the human eye­ball in vivo. The belief is that a vibrat­ing eye­ball — per­haps in con­junc­tion with other doc­u­mented effects of “uneas­i­ness” due to infra­sonic ambi­ence — leads to ghostly visions.

The 19Hz hypo­thesis was bolstered by tak­ing it to other notori­ously haunted places.

As I dug deeper and did more research, the whole thing felt a bit too neat and tidy, as if I were play­ing out a Fringe plot. Sup­port­ing the whole hypo­thesis is a NASA tech­nical report from 1976, which some­how adds to the 1-​​hour drama aesthetic.

I still have to go through the NASA tech­nical report in detail, but I had a bit of jeal­ousy when I got to the pre­face and saw it was actu­ally a Ph.D. thesis. Every now and then I get a twinge of thesis envy. Could there pos­sibly be a more badass thesis than determ­in­ing the res­on­ant fre­quency of human eye­balls? For NASA? In truth, if I were doing my Ph.D. thesis in 1976, there’s no doubt I’d be doing some­thing bor­ing and computer-​​related. Sigh.

I’m actu­ally really dis­ap­poin­ted no one’s actu­ally tried out — or pub­lished, at any rate — this 19Hz hypo­thesis exper­i­ment­ally. I need to set up some sub­woof­ers around cam­pus and see if any ghost sight­ings come out of it.

Yes, I’m a com­puter archi­tec­ture nerd. I expect this won’t sur­prise anyone.

The recent story on Microsoft end­ing sup­port for Itanium (side note: this is hardly news. No one ran Win­dows on Itanium in the first place) rekindled my love affair with the Itanium archi­tec­ture. Every six to twelve months I become infatu­ated with it all over again.

My infatu­ation usu­ally dies down when I real­ize the Itanium is out of reach for mere mor­tals. Some­times I day dream about when I’ve acci­dent­ally stumbled into money and I’m able to afford one. It’s hard to find a new Itanium server for under $30k and play­ing around with the online con­fig­ur­at­ors it’s not hard to run your­self into the half a mil­lion dol­lar range.

Today’s dif­fer­ent, though: today I decided to check out Ebay. Used Itanium serv­ers are actu­ally very cheap. Here’s one for $340. It’s only about 6 or 7 years out-​​of-​​date, too. Being out-​​of-​​date with Itanium isn’t such a big deal since they were never in-​​date to begin with. The pro­spect that I might be able to buy myself one as a gradu­ation present — when I have time to play with it — is exciting.

I won’t bore you with the details of Itanium and why it failed in its prom­ise to be the next big saviour, the one com­puter archi­tec­ture to bind them all. I was actu­ally going to write about why I love the Itanium so much, but before I knew it I’d writ­ten six para­graphs about how beau­ti­ful the archi­tec­ture is and real­ized no one but me would ever care to read it. Suf­fice it to say it’s the nicest archi­tec­ture I’ve ever seen, from the per­spect­ive of someone who truly enjoys writ­ing assembly code, the per­fect bal­ance between expos­ing the archi­tec­ture and hid­ing away the mundane details that some­time plagued RISC archi­tec­tures. Whenever someone fool­ishly asks me about Itanium — don’t worry, I’m usu­ally able to restrain myself — I describe it as “everything SPARC should have been”, SPARC being one of the more eleg­ant RISC archi­tec­tures to date.

For my pur­poses it doesn’t mat­ter if Itanium is prac­tical or pop­u­lar or well-​​fabricated or none of the above since it’s just for my own enjoy­ment. One of the biggest prob­lems is that no one’s man­aged to write a suit­able com­piler for it. That suits me just fine since I’d rather be writ­ing assembly code by hand or writ­ing my own com­piler for it. I’m actu­ally half con­vinced that if any­one actu­ally is going to write a bril­liant com­piler for Itanium, one that intel­li­gently takes advant­age of all its spec­u­lat­ive loads and rotat­ing register win­dows and sim­ilar toys that I like to drool over, it’s going to be a com­piler that has a ser­i­ous leg up in static ana­lysis, maybe for a lan­guage that’s been ser­i­ously restric­ted, for which my research would be appropriate.

Well I’m not so arrog­ant as to think that I can write a com­piler for Itanium where so some of the world’s top back-​​end developers have failed before. Even if fail­ure is nigh guar­an­teed, it would be a really fun chal­lenge, and it’s always more fun when the chal­lenge is inher­ent in the beauty of what you’re work­ing with. I think I may have to ser­i­ously put aside a few hun­dred dol­lars for after gradu­ation so I have this to play with.

The LambdaVM pro­ject is actu­ally a really bril­liant pro­ject. It’s a modi­fic­a­tion of GHC to tar­get the JVM. I installed it in Octo­ber of last year and played around with it, feel­ing that it might actu­ally have a place in help­ing spread the gos­pel of Pola.

The thing is I can’t expect people to down­load the source to Pola if they want to play around with it, so I have to provide pre-​​compiled bin­ar­ies. OS X, Win­dows and Sol­aris are easy for me to pro­duce bin­ar­ies for, but then you have to think about Linux, BSD, OpenSol­aris, 64-​​bit Win­dows, etc., on vari­ous plat­forms. Tra­di­tion­ally I have about 6 or 7 bin­ar­ies up there for the most pop­u­lar archi­tec­tures — past releases have been most pop­u­lar with x86 Debian and x86 Win­dows — but every time I make a new release I have to rebuild them all.

So I was hop­ing to have a JVM ver­sion of Pola to put up there as a catch-​​all for archi­tec­tures I hadn’t had a chance to build for yet. While the LambdaVM pro­ject has treated me fant­ast­ic­ally well for little toy examples, it doesn’t do well for Pola. I tried it and it crashed after about 2 minutes after run­ning out of heap space. The stack trace showed it was still doing type inference…after two minutes…some­thing which Pola nat­ively com­piled does in less than a hun­dredth of a second.

I’m sure if I fiddled around with it I could get it sort of work­ing, but it doesn’t seem like a good use of my time, espe­cially since the end res­ult will be huge — the JAR file is 18MB, com­pared to 2MB for an uncom­pressed bin­ary — and many orders of mag­nitude slower and since I still have hopes of gradu­at­ing soon.

Still, the LambdaVM pro­ject is pretty awe­some. I hope it ends up kick­ing some ass.

I’m cur­rently hanging out at my gate in Pear­son air­port. In a couple hours I’ll be on my way to Paris and tomor­row morn­ing I’ll catch my con­nect­ing flight to Ams­ter­dam and then I take the train to Utrecht to see Jasna’s sis­ter, Ana, and her hus­band, Andre.

Jasna and I aren’t very good with sep­ar­a­tion, though I think this time went bet­ter than most. It could be that it’s a shorter sep­ar­a­tion this time — five days, in con­trast to Jasna’s recent two-​​month trip — or that we’re too tired from last night’s Hallowe’en party to get as worked up. Maybe we’re just get­ting bet­ter at it, though. It’s not like no tears were shed, but I think we did rel­at­ively well.

Unfor­tu­nately today my cam­era bat­tery decided to crap out on me. The upside to this is Jasna lent me her (very awe­some) DSLR cam­era for the trip. I’ll try to keep pic­tures of blondes down to a min­imum. Mostly I’m excited to see Ana and Andre, but I think they’ll be busy most of the time, so I’ll prob­ably ven­ture into Ams­ter­dam at least once to enter­tain myself. I brought the cam­era cable with me, so watch my photo gal­lery in the next day or two for pic­tures to start appearing.

The con­fer­ence — and my present­a­tion there — I haven’t thought a whole lot about yet. I’ll have to dis­ap­pear to Eind­hoven, which I think is only about half an hour from Utrecht — but then again maybe everything’s half an hour away from everything in the Neth­er­lands, who knows — and see what’s going on there. I’m fairly excited to see what FOPARA ends up being like since this is the first year the workshop’s being done. I’m espe­cially excited to see the Hume pro­ject people, like Kevin Ham­mond, since I’ve never met any.

I should say there’s still a lot of work that’s going on behind the scenes, work even on what I’m going to present to FOPARA. While I was in Cal­gary we decided to put in a new typ­ing sys­tem based on bunched logics which deals eleg­antly with a lot of the prob­lems with peeks that we’ve been sort­ing out in Pola, plus some new features.

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…)