This module's namesake function.

Unification is an important step of typechecking polymorphic lambda calculi, taking two type expressions and computing their differences to produce a sequence of substitutions needed to make both type expressions equivalent.

This implementation computes a list of substitutions with the substitutions to be applied first at the end of the list and the ones to be applied last at the beginning. This is an artifact of how the reordering of the substitutions works and can be remedied with a reverse if needed.

Behaviour

• Unifying two compatable type expressions

  >>> unify (forall a. a) (A → B)
  Right [(A → B, a)]
  

  >>> unify (forall a b c. a → (b → c) → a) (forall x. x → (I → x) → G)
  Right [(G, a), (G, c), (G, x), (I, b)]
  

• Unifying incompatable type expressions yeilds errors.

  >>> unify (A) (B)
  Left [SubsMismatch A B]
  

• Unifying a poly type with a type expression that contains that poly type yeilds a cyclic substitution error.

  >>> unify (a) (F a)
  Left [CyclicSubstitution (mkGraph [(2,(F a))] [(2,2,(a))])]]
  -- The above is a graph showing the cycle of (F a) trying to substitute it's own poly type (a)
  

• Unifying equivalent type expressions yeilds empty lists.

  >>> unify (forall a. a → C) (forall x. x → C)
  Right []
  

  >>> unify (X → Y) (X → Y)
  Right []
  

unify with Gr as the instance for DynGraph.

Type ordering operator, true if the second argument is more specific or equal to the first.

Behaviour

• A type expression with poly types being ordered against one without them.

  >>> (∀ a. a) ⊑ (X → Y)
  True
  

• A type expression being ordered against itself, displaying reflexivity.

  >>> (X → X) ⊑ (X → X)
  True
  

• All type expressions are more specific than a type expression of just a single (bound or unbound) poly type.

  >>> (a) ⊑ (a)
  True
  

  >>> (a) ⊑ (b)
  True
  

  >>> (a) ⊑ (X)
  True
  

  >>> (a) ⊑ (X → Y)
  True
  

  etc.

Non-unicode ⊑.

Test to see if two types have valid substitutions between eachother.

Validate substitutions and fold them into a single substitution function.

applyAllSubs using fgl's Gr.

Without validating if the substitutions are consistent, fold them into a single function that applies all substitutions to a given type expression.

Given a list of substitutions, resolve all the mutual substitutions and return a list of substitutions in the form (t, p).

Errors in poly type substitution.

A substitution conflict's root, with a tree of types substituting variables as the first element [1] and the second element being the type where these clashing substitutions converge.

1

to be read that the first element of the tuple is a forest of substitutions leading the final type expression with a substitution conflict.

TODO: Put a diagram here instead.

Function that builds a graph representing valid substitutions or reports any part of the graph's structure that would make the substitutions invalid.

substitutionGraph using fgl's Gr.

A version of substitutionGraph that works within fgl's NodeMap state monad.

For a given list of substitutions, either find and report inconsistencies through SubsErr or compute a topsort by order of substitution such that for a list of substitutions [a, b, c] c should be applied, then b, then a.

This backward application is a product of how the graph used to compute the reordering is notated and how topsorting is ordered. In this graph for nodes N, M and egde label p, N --p-> M notates that all instances of p in M will be substituted by N. In regular topsort this means that N will preceed M in the list, but this doesn't make sense when we topsort to tuples of the form (N, p).

A version of topsortSubs that takes an already generated graph rather than building it's own.

If given a graph with cycles or nodes with 2 or more inward edges of the same label then there's no garuntee that the substitutions will be applied correctly.

From a graph representing substitutions of variables p in terms t, where edges represent the origin node replacing the variable represented by the edge label in the target node.

e.g. The edge (N, (x -> x), x) corresponds to replacing all instances of the variable x in (x -> x) with N.

Find all contexts with non-unique inward labels, paired with each label that wasn't unique.