Here is a fun thing you can do with your internet. It is a very simple experiment I figured out in the process of seeing whether something else was feasible — namely, I thought it would be nice to voluntarily circumvent livejournal's filtering-out of various interesting content (flash, etc.) by posting posts in an escaped form which a single additional click on the bookmarklet or somethin' could restore to their intended form.

--- ETA:

Except as far as I can figure, "various interesting content" is in fact limited to just flash, which makes a bookmarklet solution kind of pointless. I thought (non-officially sanctioned lj poll) forms were in this category of stuff that gets filtered out, but apparently not:

Well, a good reason for a test case to fail is that the test case is wrong.

The trouble with writing good test cases for this type theory is that the ones that create general enough unification problems to be interesting require (as far as I can tell) fifth-order signatures to be typechecked. Or maybe it's fourth; what would you call a signature with a type family in it like c : ({a:world} (({b:world} ((t -o t) -> t) -> t) -> t)) -> type. ? My brain already becomes mushy at about three and a half levels of functional left-hand-side nesting, so it is complete purée now. — --- ETA: Hey, I can get it down by one order after all: c : ({a:w} (({b:w} (t @ p -> t @ q) -> t) -> t)) -> type exhibits enough unificational generality, and it's almost something I can make sense of: a type family indexed by a sort of strong double-negation of a refinement of the type t -> t. Maybe with a merely half-mushy brain I can make some progress now...

I've been reading a lot about equational unification this afternoon, trying to find the best possible algorithm to fill the checking/synthesizing boundary of my type checker. I hadn't really looked into the area much since like four years ago, but it's really quite amazing stuff.

All I really need right now is a trivial subset of what's called ACU-unification, where ACU stands for "associative, commutative, unit". This arises from the fact that world labels are relatively first-class things, and type-checking for the elimination of a forall quantifier over worlds postpones the choice of world as an existential variable to be later unified:

Γ |- S : [X/w]A > C ------------------------------ Γ |- S : ∀w.A > C

so what I wind up with is some equations where both sides are lists (delimited by "world concatenation", an operator that's essentially linear logic's tensor) of existential variables and world parameters.

General ACU-unification talks about terms built out of other function symbols and stuff, and here I have only constants and the AC function symbol — so I figure it should be ultra-efficient to do it, but I don't yet know how to adapt the stuff that claims to be ultra-efficient in the general case. I do know a stupid way of reducing the problem to linear diophantine equations, but them's nasty.