Jason (jcreed) wrote,

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.
Tags: work

  • (no subject)

    Had a good bunch of discussions with Sean and Alyssa at work. Supposed to be stupid hot this weekend when we were planning to do the final cleanup of…

  • (no subject)

    Started moving some stuff into the new place in Astoria! Basically just books, but pretty much all our books made it there. Made a Zipcar reservation…

  • (no subject)

    Got lease signed! Movin' to Astoria imminently, I guess. Restaurant situation seems incredibly good over there.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded