Portability | semi-portable (MPTCs, FlexibleContexts) |
---|---|

Stability | experimental |

Maintainer | wren@community.haskell.org |

This module provides first-order structural unification over general structure types. It also provides the standard suite of functions accompanying unification (applying bindings, getting free variables, etc.).

The implementation makes use of numerous optimization techniques. First, we use path compression everywhere (for weighted path compression see Control.Unification.Ranked). Second, we replace the occurs-check with visited-sets. Third, we use a technique for aggressive opportunistic observable sharing; that is, we track as much sharing as possible in the bindings (without introducing new variables), so that we can compare bound variables directly and therefore eliminate redundant unifications.

- data MutTerm v t
- freeze :: Traversable t => MutTerm v t -> Maybe (Fix t)
- unfreeze :: Functor t => Fix t -> MutTerm v t
- data UnificationFailure v t
- = OccursIn (v (MutTerm v t)) (MutTerm v t)
- | TermMismatch (t (MutTerm v t)) (t (MutTerm v t))
- | UnknownError String

- class Traversable t => Unifiable t where
- class Variable v where
- class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad v t m | m -> v t where
- getFreeVars :: BindingMonad v t m => MutTerm v t -> m [v (MutTerm v t)]
- applyBindings :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> e m (MutTerm v t)
- freshen :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> e m (MutTerm v t)
- (===) :: BindingMonad v t m => MutTerm v t -> MutTerm v t -> m Bool
- (=~=) :: BindingMonad v t m => MutTerm v t -> MutTerm v t -> m (Maybe (IntMap Int))
- (=:=) :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> MutTerm v t -> e m (MutTerm v t)
- (<:=) :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> MutTerm v t -> e m Bool
- equals :: BindingMonad v t m => MutTerm v t -> MutTerm v t -> m Bool
- equiv :: BindingMonad v t m => MutTerm v t -> MutTerm v t -> m (Maybe (IntMap Int))
- unify :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> MutTerm v t -> e m (MutTerm v t)
- unifyOccurs :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> MutTerm v t -> e m (MutTerm v t)
- subsumes :: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) => MutTerm v t -> MutTerm v t -> e m Bool
- fullprune :: BindingMonad v t m => MutTerm v t -> m (MutTerm v t)
- semiprune :: BindingMonad v t m => MutTerm v t -> m (MutTerm v t)
- occursIn :: BindingMonad v t m => v (MutTerm v t) -> MutTerm v t -> m Bool

# Data types, classes, etc

## Mutable terms

freeze :: Traversable t => MutTerm v t -> Maybe (Fix t)Source

*O(n)*. Extract a pure term from a mutable term, or return
`Nothing`

if the mutable term actually contains variables. N.B.,
this function is pure, so you should manually apply bindings
before calling it.

## Errors

data UnificationFailure v t Source

The possible failure modes that could be encountered in unification and related functions. While many of the functions could be given more accurate types if we used ad-hoc combinations of these constructors (i.e., because they can only throw one of the errors), the extra complexity is not considered worth it.

OccursIn (v (MutTerm v t)) (MutTerm v t) | A cyclic term was encountered (i.e., the variable
occurs free in a term it would have to be bound to in
order to succeed). Infinite terms like this are not
generally acceptable, so we do not support them. In logic
programming this should simply be treated as unification
failure; in type checking this should result in a "could
not construct infinite type Note that since, by default, the library uses visited-sets instead of the occurs-check these errors will be thrown at the point where the cycle is dereferenced/unrolled (e.g., when applying bindings), instead of at the time when the cycle is created. However, the arguments to this constructor should express the same context as if we had performed the occurs-check, in order for error messages to be intelligable. |

TermMismatch (t (MutTerm v t)) (t (MutTerm v t)) | The top-most level of the terms do not match (according
to |

UnknownError String | Required for the |

(Show (t (MutTerm v t)), Show (v (MutTerm v t))) => Show (UnificationFailure v t) | |

Error (UnificationFailure v t) |

## Basic type classes

class Traversable t => Unifiable t whereSource

An implementation of unification variables. Note that we do
not require variables to be functors. Thus, it does not matter
whether you give them vacuous functor instances, or use clever
tricks like `CoYoneda STRef`

to give them real functor instances.

eqVar :: v a -> v b -> BoolSource

Determine whether two variables are equal *as variables*,
without considering what they are bound to. The default
implementation is:

eqVar x y = getVarID x == getVarID y

Return a unique identifier for this variable, in order to support the use of visited-sets instead of occurs-checks.

class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad v t m | m -> v t whereSource

The basic class for generating, reading, and writing to bindings stored in a monad. These three functionalities could be split apart, but are combined in order to simplify contexts. Also, because most functions reading bindings will also perform path compression, there's no way to distinguish "true" mutation from mere path compression.

The superclass constraints are there to simplify contexts, since
we make the same assumptions everywhere we use `BindingMonad`

.

lookupVar :: v (MutTerm v t) -> m (Maybe (MutTerm v t))Source

Given a variable pointing to `MutTerm v t`

, return the
term it's bound to, or `Nothing`

if the variable is unbound.

freeVar :: m (v (MutTerm v t))Source

Generate a new free variable guaranteed to be fresh in
`m`

.

newVar :: MutTerm v t -> m (v (MutTerm v t))Source

Generate a new variable (fresh in `m`

) bound to the given
term. The default implementation is:

newVar t = do { v <- freeVar ; bindVar v t ; return v }

bindVar :: v (MutTerm v t) -> MutTerm v t -> m ()Source

Bind a variable to a term, overriding any previous binding.

(Unifiable t, Applicative m, Monad m) => BindingMonad IntVar t (IntBindingT t m) | |

(Unifiable t, Applicative m, Monad m) => BindingMonad IntVar t (IntRBindingT t m) | |

Unifiable t => BindingMonad (STVar s) t (STBinding s) | |

Unifiable t => BindingMonad (STRVar s t) t (STRBinding s) |

# Operations on one term

getFreeVars :: BindingMonad v t m => MutTerm v t -> m [v (MutTerm v t)]Source

Walk a term and determine what variables are still free. N.B., this function does not detect cyclic terms (i.e., throw errors), but it will return the correct answer for them in finite time.

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> e m (MutTerm v t) |

Apply the current bindings from the monad so that any remaining
variables in the result must, therefore, be free. N.B., this
expensively clones term structure and should only be performed
when a pure term is needed, or when `OccursIn`

exceptions must
be forced. This function *does* preserve sharing, however that
sharing is no longer observed by the monad.

If any cyclic bindings are detected, then an `OccursIn`

exception
will be thrown.

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> e m (MutTerm v t) |

Freshen all variables in a term, both bound and free. This ensures that the observability of sharing is maintained, while freshening the free variables. N.B., this expensively clones term structure and should only be performed when necessary.

If any cyclic bindings are detected, then an `OccursIn`

exception
will be thrown.

# Operations on two terms

## Symbolic names

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> MutTerm v t | |

-> e m (MutTerm v t) |

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> MutTerm v t | |

-> e m Bool |

## Textual names

:: BindingMonad v t m | |

=> MutTerm v t | |

-> MutTerm v t | |

-> m Bool |

Determine if two terms are structurally equal. This is essentially
equivalent to `(`

except that it does not require applying
bindings before comparing, so it is more efficient. N.B., this
function does not consider alpha-variance, and thus variables
with different names are considered unequal. Cf., `==`

)`equiv`

.

Determine if two terms are structurally equivalent; that is, structurally equal modulo renaming of free variables. Returns a mapping from variable IDs of the left term to variable IDs of the right term, indicating the renaming used.

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> MutTerm v t | |

-> e m (MutTerm v t) |

Unify two terms, or throw an error with an explanation of why unification failed. Since bindings are stored in the monad, the two input terms and the output term are all equivalent if unification succeeds. However, the returned value makes use of aggressive opportunistic observable sharing, so it will be more efficient to use it in future calculations than either argument.

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> MutTerm v t | |

-> e m (MutTerm v t) |

A variant of `unify`

which uses `occursIn`

instead of visited-sets.
This should only be used when eager throwing of `OccursIn`

errors
is absolutely essential (or for testing the correctness of
`unify`

). Performing the occurs-check is expensive. Not only is
it slow, it's asymptotically slow since it can cause the same
subterm to be traversed multiple times.

:: (BindingMonad v t m, MonadTrans e, Functor (e m), MonadError (UnificationFailure v t) (e m)) | |

=> MutTerm v t | |

-> MutTerm v t | |

-> e m Bool |

Determine whether the left term subsumes the right term. That
is, whereas `(tl =:= tr)`

will compute the most general substitution
`s`

such that `(s tl === s tr)`

, `(tl <:= tr)`

computes the most
general substitution `s`

such that `(s tl === tr)`

. This means
that `tl`

is less defined than and consistent with `tr`

.

*N.B.*, this function updates the monadic bindings just like
`unify`

does. However, while the use cases for unification often
want to keep the bindings around, the use cases for subsumption
usually do not. Thus, you'll probably want to use a binding monad
which supports backtracking in order to undo the changes.
Unfortunately, leaving the monadic bindings unaltered and returning
the necessary substitution directly imposes a performance penalty
or else requires specifying too much about the implementation
of variables.

# Helper functions

Client code should not need to use these functions, but they are exposed just in case they are needed.

fullprune :: BindingMonad v t m => MutTerm v t -> m (MutTerm v t)Source

Canonicalize a chain of variables so they all point directly to the term at the end of the chain (or the free variable, if the chain is unbound), and return that end.

N.B., this is almost never the function you want. Cf., `semiprune`

.

semiprune :: BindingMonad v t m => MutTerm v t -> m (MutTerm v t)Source

Canonicalize a chain of variables so they all point directly to the last variable in the chain, regardless of whether it is bound or not. This allows detecting many cases where multiple variables point to the same term, thereby allowing us to avoid re-unifying the term they point to.

occursIn :: BindingMonad v t m => v (MutTerm v t) -> MutTerm v t -> m BoolSource

Determine if a variable appears free somewhere inside a term. Since occurs checks only make sense when we're about to bind the variable to the term, we do not bother checking for the possibility of the variable occuring bound in the term.