A substitution is but a map; the existential quantifiers are necessary to ensure we can reuse from Data.Map

Note that we must be able to compare Exists phi. This comparison needs to work heterogeneously and it must return EQ only when the contents are in fact equal. Even though we only need this instance for Data.Map

A typical example for phi is Const Int at, representing a variable. The Ord instance would then be:

instance Ord (Exists (Const Int)) where
  compare (Exists (Const x)) (Exists (Const y))
    = compare x y

Empty substitution

Inserts a point in a substitution. Note how the index of phi must match the index of the term being inserted. This is important when looking up terms because we must unsafeCoerce the existential type variables to return.

Please, always use this insertion function; or, if you insert by hand, ensure thetype indices match.

Looks a value up in a substitution, see substInsert

Applies a substitution to a term once; Variables not in the support of the substitution are left untouched.

Unification can return succesfully or find either a OccursCheck failure or a SymbolClash failure.

Attempts to unify two Holes

Attempts to unify two Holes, but ignores which error happened when they could not be unified.

Attempts to unify two Holes with an already existing substitution

The minimization step performs the occurs check and removes unecessary steps, returning an idempodent substitution when successful. For example;

sigma = fromList
          [ (0 , bin 1 2)
          , (1 , bin 4 4) ]

Then, minimize sigma will return fromList [(0 , bin (bin 4 4) 2) , (1 , bin 4 4)] This returns Left vs if occurs-check fail for variables vs.