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

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded