I finally feel like a real programming languages person. I just used unification to solve a problem besides type checking a variant of the lambda calculus. I used the excellent unification-fd package; it is a bit light on documentation but the included tests were enough for me to figure out how to use it. I might post something more detailed later on.
My problem arose due to the type system rewrite in LLVM 3.0. Prior to
this, types were all uniqued: there was one instance of each
structurally equal type. This is no longer the case. Each struct
type is named and there can be multiple structs with the same
structural type. That is fine and actually closer to what I always
wanted. Unfortunately, sometimes different names are assigned to the
same type in different compilation units (the duplicates have the same
base name but a numeric suffix). Unfortunately, types sharing a name
are not always the same -- some libraries actually do re-use type
names for different types in different compilation units.
Example of the first case:
%struct.glp_long = type { i32, i32 }
%struct.glp_long.0 = type { i32, i32 }
Example of the second case:
%struct.csa = type { %struct.glp_prob.10*, %struct.glp_bfcp.8, ... }
%struct.csa.556 = type { i32*, double*, i32*, double* }
The first type is expected to unify, while the second is not. I used
this to pick a representative type for the first case and to treat
each type name used in the second case as opaque. Oddly enough,
everything worked the first time I ran it. I noticed that some types
I expected to unify did not (e.g., the glp_prob and glp_tree types
in glpk). It turns out that the
library (intentionally?) does not always include the correct headers
to define types. In those cases, it uses the C preprocessor to just
define them to be
struct foo { double _opaque_foo[100]; };
This is a bit annoying, but I managed to work around it outside of the unification framework. I'm not sure why they don't just forward declare types like normal libraries.