Substitutions map variables (internally represented as Ints) to Terms of a specific type. A key design principle of this library is that each type has its set of variables, that do not overlap. So in the following substitution the variable 1 of type Char tracks the term `Con c` while the variable 1 of type Int tracks the term `Con 42`. There is no possibility of ambiguity, and this simplifies the definition of Term.

>>> :set -XTypeApplications
>>> ex_substitution = insert @Char 1 (Con 'c') . insert @Int 1 (Con 42) $ empty :: Substitution
>>> ex_substitution
Substitution { Int -> [(1,Con 42)], Char -> [(1,Con 'c')] }

This is a class that expresses the constraint we need every type in our substitution to have. It is an implementation detail of the library, but helps in understanding which datatype we can have in our substitutions.

A datatype that includes a constraint (this is useful because, as a substitution contains heterogeneous terms, we have to be sure that those terms have some common behaviour to be able to operate on them, and we use Constrained to assure that).

The generic eliminator for Constrained

The empty substitution, which does not contain variable bindings

>>> empty
Substitution {  }

Insert a variable binding into a substitution

>>> :set -XTypeApplications
>>> insert @Int 1 (Con 42) empty
Substitution { Int -> [(1,Con 42)] }

A substitution with only one variable binding

>>> :set -XTypeApplications
>>> singleton @Int 1 (Con 42)
Substitution { Int -> [(1,Con 42)] }

Search for a variable in the substitution

>>> lookup @Int 1 $ singleton @Int 1 (Con 42)
Just (Con 42)
>>> lookup @String 1 $ singleton @Int 1 (Con 42)
Nothing

The union of two substitutions. It has the same bias of union in Data.Map, if you think a substitution as a [(Type, Value)] map-like structure

>>> union (singleton @Int 1 (Con 42)) (singleton @Char 1 (Con 'c'))
Substitution { Int -> [(1,Con 42)], Char -> [(1,Con 'c')] }

We can fold a substitution in a monoidal value

>>> fold (\a -> [show a]) (insert @Char 1 (Con 'c') . insert @Int 1 (Con 42) $ empty)
["Con 42","Con 'c'"]

Take all variables that are free in a substitution. This amounts to taking all the free variables of the internal terms

This class means that we can calculate the free variables of something and apply to it a substitution. The default instance signatures appear duplicated for a bug of haddock.

This datatype encodes the free (not bound) variables that we can have in a term or a substitution. Basically, since our variables are overlappable, a set of variables for every type.

>>> FreeVars (fromList [TM.WrapTypeable @Int $ Const (IS.fromList [1,2]), TM.WrapTypeable @Char $ Const (IS.fromList [1,3])])
FreeVars { Int -> [1,2], Char -> [1,3] }

Usually one would get a FreeVars from using the method ftv of the Substitutable class.

>>> ftv (Var 1 :: Term Int)
FreeVars { Int -> [1] }

We can query if a variable is in the FreeVars at a certain type

>>> :set -XTypeApplications
>>> memberFreeVars @Int 1 (ftv (Var 1 :: Term Int))
True
>>> memberFreeVars @Int 1 (ftv (Var 1 :: Term Char))
False

Get all the free variables of a type, as variables of that term. This is made to implement the equivalent of prolog's term_variables.

Visited sets: an abstraction in the Dijkstra paper that let us avoid expensive occurs check in the substitution process, substituting it with checking visited sets when the substitution is applied. This datatype is representationally equivalent to FreeVars, ie. it is only a IntSet for every type.

>>> Visited (fromList [TM.WrapTypeable @Int $ Const (IS.fromList [1,2]), TM.WrapTypeable @Char $ Const (IS.fromList [1,3])])
Visited { Int -> [1,2], Char -> [1,3] }

This datatype is only meant to be used in the library, the user shouldn't need it.

We can query if a variable at a certain type has been visited

>>> :set -XTypeApplications
>>> memberVisited @Int 1 mempty
False
>>> memberVisited @Int 1 $ insertVisited @Int 1 mempty
True

We can signal that a variable at a certain type has been visited

>>> :set -XTypeApplications
>>> insertVisited @Int 1 mempty
Visited { Int -> [1] }