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.