I just finished reading A Balance of Power: Expressive, Analyzable Controller Programming. It’s an interesting proposal, but I’m writing just to express my satisfaction with the following sentence:
When we hit expressive limits, however, our goal is not to keep growing this language—down that path lies sendmail.cf and other sulphurous designs—but to call out to full-language code.
‘Sulphurous’ indeed. Come for the nonmonotonic interpretation of learning, stay for the colorful prose.
I’ve released a bugfix for PHPEnkoder version 1.12. Get this: before version 5.5, PHP didn’t support arbitrary array index expressions. The problem was a line:
$ord = unpack("N",$c)[1];
Which I changed to:
$bs = unpack("N",$c);
$ord = $bs[1];
This is really ridiculous. Like, serious amateur hour ridiculous. Like, if your final project in a compiler’s class had syntactic limitation, you would not get a good grade. PHP is a fractal of bad design. Ugh. Just: ugh.
And while I’m complaining about these sorts of things, where are the structured content management systems? PHPEnkoder’s email and mailto: detection is a giant, horrible kludge of regular expressions. Where’s the CMS where the filters get passed a structured, syntactic representation of the page to be rendered? This is a serious question, and if you know of one, please tell me.
I’m really delighted to have resolved a longstanding problem with PHPEnkoder and Unicode: PHPEnkoder should no longer choke on the various multi-byte characters, such as é and ü and ß. (No really, look: email hidden; JavaScript is required!)
As usual, updates are available from the WordPress plugin directory or from your dashboard.
The third chapter of my dissertation is effectively a longer version of an ESOP 2011 paper, Polymorphic Contracts. We define FH, a polymorphic calculus with manifest contracts. Atsushi Igarashi, with whom I did the original FH work that appeared in ESOP 2011, and his student Taro Sekiyama have been working on continuing some of the FH work. They discovered—after my defense!—a bug in FH’s metatheory.
Short version: FH used parallel reduction as a conversion relation. A key property of this relation is substitutivity. We phrased it as “if e1 ⇒ e1′ and e2 ⇒ e2′ then e1{e2/x} ⇒ e1′{e2’/x}”. Unfortunately, this doesn’t hold for FH, due to subtleties in FH’s reduction rules for casts. The cast reduction rules are implicitly performing equality checks on types, and these equality checks can be affected by substitutions to change which reduction rule applies. The (tentative) solution in my thesis is to use a simpler type (and term) conversion relation which we call common subexpression reduction (CSR). In CSR, we relate types and terms that are closed by closing substitutions σ1 →* σ2. That is, the CSR conversion is the smallest congruence which is substitutive for →*, i.e., where if e →* e’ then T{e/x} ≡ T{e’/x}.
Long version: I’ve excerpted Section 3.5 of my thesis which discusses the System FH type conversion bug.