Documentation

Compose two substitutions. Applying s1 @@ s2 is the same as applying first s2, then s1; that is, semantically, composition of substitutions corresponds exactly to function composition when they are considered as functions on terms.

As one would expect, composition is associative and has idS as its identity.

Note that we do not apply s1 to all the values in s2, since the substitution is maintained lazily; we do not need to maintain the invariant that values in the mapping do not contain any of the keys. This makes composition much faster, at the cost of making application more complex.

Class of things supporting substitution. Substitutes n b a means that we can apply a substitution of type Subst n b to a value of type a, replacing all the free names of type n inside the a with values of type b, resulting in a new value of type a.

We also do a lazy occurs-check during substitution application, so we need the ability to throw a unification error.

Carrier type for unification: we maintain a current substitution, a counter for generating fresh unification variables, and can throw unification errors.

Counter for generating fresh unification variables.

Run a Unification effect via the UnificationC carrier. Note that we also require an ambient Reader TDCtx effect, so unification will be sure to pick up whatever type aliases happen to be in scope.

Unify two types, returning a unified type equal to both. Note that for efficiency we don't do an occurs check here, but instead lazily during substitution.

We keep track of a set of pairs of types we have seen; if we ever see a pair a second time we simply assume they are equal without recursing further. This constitutes a finite (coinductive) algorithm for doing unification on recursive types.

For example, suppose we wanted to unify rec s. Unit + Unit + s and rec t. Unit + t. These types are actually equal since their infinite unfoldings are both Unit + Unit + Unit + ... In practice we would proceed through the following recursive calls to unify:

    (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
        { unfold the LHS }
    (Unit + Unit + (rec s. Unit + Unit + s)) =:= (rec t. Unit + t)
        { unfold the RHS }
    (Unit + Unit + (rec s. Unit + Unit + s)) =:= (Unit + (rec t. Unit + t)
        { unifyF matches the + and makes two calls to unify }
    Unit =:= Unit   { trivial}
    (Unit + (rec s. Unit + Unit + s))        =:= (rec t. Unit + t)
        { unfold the RHS }
    (Unit + (rec s. Unit + Unit + s))        =:= (Unit + (rec t. Unit + t))
        { unifyF on + }
    (rec s. Unit + Unit + s)                 =:= (rec t. Unit + t)
        { back to the starting pair, return success }
  

Unify a unification variable which is not bound by the current substitution with another term. If the other term is also a variable, we must look it up as well to see if it is bound.

Perform unification on two non-variable terms: check that they have the same top-level constructor and recurse on their contents.