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.

Exactly the clean­est and most express­ive way to impose restric­tions on recur­sion on peeks while stay­ing in P, which is the real goal of Pola, hasn’t been entirely hammered out yet. There are any of num­bers of ways to get it to work, but no one’s sure if they’re clean enough. I’m extremely excited that, except for the recur­sion busi­ness, the mech­an­ism of type-​​checking peeks has finally been solved, extremely cleanly using bunched logics. It had been a real mess before and the new for­mu­la­tion is really a thing of beauty. It’s what I’ve always wanted for peeks, even if I’d never heard of bunched logics before.

Aside from the mat­ter of me find­ing the time to actu­ally fin­ish imple­ment­ing these things — though I’m still mak­ing good progress! — is the mat­ter of infer­ring bounds, which from my (very prac­tic­ally based) view­point is the whole motiv­a­tion for the lan­guage. The ini­tial write-​​up I shoe­horned into the end of the FOPARA paper is def­in­itely on the right track, but the details need to be cleaned up some.