Sat Jan 26 15:09:18 CET 2013
Type inference (unification)
Turns out to be very simple. Components:
- Type environment, binding node names to type names. (Initialized by
setting each node to a separate type variable)
- Every primitive application unifies the nodes that take part in the
t_0 = t_1 = ... = t_k
- Every deconstruction application unifies the type variable of the
input node with a type-constructor-wrapped deconstructed type:
t_struct = List t_element
- Unification can be implemented by brute force deep substitution of a
symbol with its binding in the type environment.
- Can the quadratic complexity of the brute-force substitution be
linearized? EDIT: I think the trick is to just not unify
(substitute) already equal types.