Unification Algorithm

    type term =
    | Var of string
    | Term of string * term list

You either have a type variable with a name, or a type constructor with a name and a list of arguments.

Unification takes a list of term pairs which have to be made matching.

Unification returns a list of substitutions, where a substitution is a pair of a string and a term, aka the variable name that should be substituted with the term.

Steps for unifying two terms

Try to match

2 Vars

no subs if names equal, otherwise return sub [(v1,v2)]

2 Terms

• fail if constructor names are different
• fail if length of args are different

Unify the args of the 2 constructors and return those substitutions.

Term and Var

• fail if var occurs in the term

return [(var,term)]

Unifying a list of constraints

• Unify rest of list
• Apply substitutions to head
• unify the two terms that make up the head

Collecting constraints in code for type unification/inference

• any function application is a constraint between the types of the args and the type of the function
• use the same type variables for specific names to ensure the type of that name is properly constrained
• Polymorphic variables/functions that appear multiple times are separate names! Don’t reuse those names. For example, the empty list has type 'a list. That free variable means that each use of the empty list can be bound to a different type constraint since each use adds another free variable to the equation.

– TODO: Maybe work an example?