unification-fd-0.11.1: Simple generic unification algorithms.

Control.Unification

Description

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.

Synopsis

# Data types, classes, etc

## Unification terms

data UTerm t v Source #

The type of terms generated by structures t over variables v. The structure type should implement Unifiable and the variable type should implement Variable.

The Show instance doesn't show the constructors, in order to improve legibility for large terms.

All the category theoretic instances (Functor, Foldable, Traversable,...) are provided because they are often useful; however, beware that since the implementations must be pure, they cannot read variables bound in the current context and therefore can create incoherent results. Therefore, you should apply the current bindings before using any of the functions provided by those classes.

Constructors

 UVar !v A unification variable. UTerm !(t (UTerm t v)) Some structure containing subterms.

#### Instances

Instances details
 Functor t => Monad (UTerm t) Source # Instance detailsDefined in Control.Unification.Types Methods(>>=) :: UTerm t a -> (a -> UTerm t b) -> UTerm t b #(>>) :: UTerm t a -> UTerm t b -> UTerm t b #return :: a -> UTerm t a # Functor t => Functor (UTerm t) Source # Instance detailsDefined in Control.Unification.Types Methodsfmap :: (a -> b) -> UTerm t a -> UTerm t b #(<\$) :: a -> UTerm t b -> UTerm t a # Functor t => Applicative (UTerm t) Source # Instance detailsDefined in Control.Unification.Types Methodspure :: a -> UTerm t a #(<*>) :: UTerm t (a -> b) -> UTerm t a -> UTerm t b #liftA2 :: (a -> b -> c) -> UTerm t a -> UTerm t b -> UTerm t c #(*>) :: UTerm t a -> UTerm t b -> UTerm t b #(<*) :: UTerm t a -> UTerm t b -> UTerm t a # Foldable t => Foldable (UTerm t) Source # Instance detailsDefined in Control.Unification.Types Methodsfold :: Monoid m => UTerm t m -> m #foldMap :: Monoid m => (a -> m) -> UTerm t a -> m #foldMap' :: Monoid m => (a -> m) -> UTerm t a -> m #foldr :: (a -> b -> b) -> b -> UTerm t a -> b #foldr' :: (a -> b -> b) -> b -> UTerm t a -> b #foldl :: (b -> a -> b) -> b -> UTerm t a -> b #foldl' :: (b -> a -> b) -> b -> UTerm t a -> b #foldr1 :: (a -> a -> a) -> UTerm t a -> a #foldl1 :: (a -> a -> a) -> UTerm t a -> a #toList :: UTerm t a -> [a] #null :: UTerm t a -> Bool #length :: UTerm t a -> Int #elem :: Eq a => a -> UTerm t a -> Bool #maximum :: Ord a => UTerm t a -> a #minimum :: Ord a => UTerm t a -> a #sum :: Num a => UTerm t a -> a #product :: Num a => UTerm t a -> a # Traversable t => Traversable (UTerm t) Source # Instance detailsDefined in Control.Unification.Types Methodstraverse :: Applicative f => (a -> f b) -> UTerm t a -> f (UTerm t b) #sequenceA :: Applicative f => UTerm t (f a) -> f (UTerm t a) #mapM :: Monad m => (a -> m b) -> UTerm t a -> m (UTerm t b) #sequence :: Monad m => UTerm t (m a) -> m (UTerm t a) # (Show v, Show (t (UTerm t v))) => Show (UTerm t v) Source # Instance detailsDefined in Control.Unification.Types MethodsshowsPrec :: Int -> UTerm t v -> ShowS #show :: UTerm t v -> String #showList :: [UTerm t v] -> ShowS #

freeze :: Traversable t => UTerm t v -> 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.

unfreeze :: Functor t => Fix t -> UTerm t v Source #

O(n). Embed a pure term as a mutable term.

## Errors

class Fallible t v a where 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.

This is a finally-tagless encoding of the UFailure data type so that we can abstract over clients adding additional domain-specific failure modes, introducing monoid instances, etc.

Since: 0.10.0

Methods

occursFailure :: v -> UTerm t v -> a Source #

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 a = Foo a" error.

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.

mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> a Source #

The top-most level of the terms do not match (according to zipMatch). In logic programming this should simply be treated as unification failure; in type checking this should result in a "could not match expected type Foo with inferred type Bar" error.

#### Instances

Instances details
 Fallible t v (UFailure t v) Source # Instance detailsDefined in Control.Unification.Types MethodsoccursFailure :: v -> UTerm t v -> UFailure t v Source #mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> UFailure t v Source #

## Basic type classes

class Traversable t => Unifiable t where Source #

An implementation of syntactically unifiable structure. The Traversable constraint is there because we also require terms to be functors and require the distributivity of sequence or mapM.

Updated: 0.11 This class can now be derived so long as you have a Generic1 instance.

Minimal complete definition

Nothing

Methods

zipMatch :: t a -> t a -> Maybe (t (Either a (a, a))) Source #

Perform one level of equality testing for terms. If the term constructors are unequal then return Nothing; if they are equal, then return the one-level spine filled with resolved subterms and/or pairs of subterms to be recursively checked.

default zipMatch :: (Generic1 t, Unifiable (Rep1 t)) => t a -> t a -> Maybe (t (Either a (a, a))) Source #

#### Instances

Instances details
 Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: Par1 a -> Par1 a -> Maybe (Par1 (Either a (a, a))) Source # Unifiable (V1 :: Type -> Type) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: V1 a -> V1 a -> Maybe (V1 (Either a (a, a))) Source # Unifiable (U1 :: Type -> Type) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: U1 a -> U1 a -> Maybe (U1 (Either a (a, a))) Source # Unifiable f => Unifiable (Rec1 f) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: Rec1 f a -> Rec1 f a -> Maybe (Rec1 f (Either a (a, a))) Source # Eq c => Unifiable (K1 i c :: Type -> Type) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: K1 i c a -> K1 i c a -> Maybe (K1 i c (Either a (a, a))) Source # (Unifiable f, Unifiable g) => Unifiable (f :+: g) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: (f :+: g) a -> (f :+: g) a -> Maybe ((f :+: g) (Either a (a, a))) Source # (Unifiable f, Unifiable g) => Unifiable (f :*: g) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: (f :*: g) a -> (f :*: g) a -> Maybe ((f :*: g) (Either a (a, a))) Source # Unifiable f => Unifiable (M1 i c f) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: M1 i c f a -> M1 i c f a -> Maybe (M1 i c f (Either a (a, a))) Source # (Unifiable f, Unifiable g) => Unifiable (f :.: g) Source # Instance detailsDefined in Control.Unification.Types MethodszipMatch :: (f :.: g) a -> (f :.: g) a -> Maybe ((f :.: g) (Either a (a, a))) Source #

class Eq v => Variable v where Source #

An implementation of unification variables. The Eq requirement is to determine whether two variables are equal as variables, without considering what they are bound to. We use Eq rather than having our own eqVar method so that clients can make use of library functions which commonly assume Eq.

Methods

getVarID :: v -> Int Source #

Return a unique identifier for this variable, in order to support the use of visited-sets instead of occurs-checks. This function must satisfy the following coherence law with respect to the Eq instance:

x == y if and only if getVarID x == getVarID y

#### Instances

Instances details
 Source # Instance detailsDefined in Control.Unification.IntVar Methods Variable (STVar s t) Source # Instance detailsDefined in Control.Unification.STVar MethodsgetVarID :: STVar s t -> Int Source # Variable (STRVar s t) Source # Instance detailsDefined in Control.Unification.Ranked.STVar MethodsgetVarID :: STRVar s t -> Int Source #

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

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.

Minimal complete definition

Methods

lookupVar :: v -> m (Maybe (UTerm t v)) Source #

Given a variable pointing to UTerm t v, return the term it's bound to, or Nothing if the variable is unbound.

freeVar :: m v Source #

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

newVar :: UTerm t v -> m v 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 -> UTerm t v -> m () Source #

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

#### Instances

Instances details
 (Unifiable t, Applicative m, Monad m) => BindingMonad t IntVar (IntBindingT t m) Source # Instance detailsDefined in Control.Unification.IntVar MethodslookupVar :: IntVar -> IntBindingT t m (Maybe (UTerm t IntVar)) Source #bindVar :: IntVar -> UTerm t IntVar -> IntBindingT t m () Source # (Unifiable t, Applicative m, Monad m) => BindingMonad t IntVar (IntRBindingT t m) Source # Instance detailsDefined in Control.Unification.Ranked.IntVar MethodslookupVar :: IntVar -> IntRBindingT t m (Maybe (UTerm t IntVar)) Source #bindVar :: IntVar -> UTerm t IntVar -> IntRBindingT t m () Source # Unifiable t => BindingMonad t (STVar s t) (STBinding s) Source # Instance detailsDefined in Control.Unification.STVar MethodslookupVar :: STVar s t -> STBinding s (Maybe (UTerm t (STVar s t))) Source #freeVar :: STBinding s (STVar s t) Source #newVar :: UTerm t (STVar s t) -> STBinding s (STVar s t) Source #bindVar :: STVar s t -> UTerm t (STVar s t) -> STBinding s () Source # Unifiable t => BindingMonad t (STRVar s t) (STRBinding s) Source # Instance detailsDefined in Control.Unification.Ranked.STVar MethodslookupVar :: STRVar s t -> STRBinding s (Maybe (UTerm t (STRVar s t))) Source #freeVar :: STRBinding s (STRVar s t) Source #newVar :: UTerm t (STRVar s t) -> STRBinding s (STRVar s t) Source #bindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s () Source #

# Operations on one term

getFreeVars :: BindingMonad t v m => UTerm t v -> m [v] Source #

Walk a term and determine which 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.

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

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 occursFailure 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 occursFailure exception will be thrown.

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

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 occursFailure exception will be thrown.

# Operations on two terms

## Symbolic names

(===) infix 4 Source #

Arguments

 :: BindingMonad t v m => UTerm t v -> UTerm t v -> m Bool

equals

(=~=) infix 4 Source #

Arguments

 :: BindingMonad t v m => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))

equiv

(=:=) infix 4 Source #

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)

unify

(<:=) infix 4 Source #

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m Bool

subsumes

## Textual names

equals infix 4 Source #

Arguments

 :: BindingMonad t v m => UTerm t v -> UTerm t v -> 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.

equiv infix 4 Source #

Arguments

 :: BindingMonad t v m => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))

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.

unify infix 4 Source #

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)

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.

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)

A variant of unify which uses occursIn instead of visited-sets. This should only be used when eager throwing of occursFailure 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.

subsumes infix 4 Source #

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em 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.

# Operations on many terms

getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v] Source #

Same as getFreeVars, but works on several terms simultaneously. This is more efficient than getting the free variables for each of the terms separately because we can make use of sharing across the whole collection. That is, each time we move to the next term, we still remember the bound variables we've already looked at (and therefore do not need to traverse, since we've already seen whatever free variables there are down there); whereas we would forget between each call to getFreeVars.

Since: 0.7.0

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

Same as applyBindings, but works on several terms simultaneously. This function preserves sharing across the entire collection of terms, whereas applying the bindings to each term separately would only preserve sharing within each term.

Since: 0.7.0

Arguments

 :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

Same as freshen, but works on several terms simultaneously. This is different from freshening each term separately, because freshenAll preserves the relationship between the terms. For instance, the result of

mapM freshen [UVar 1, UVar 1]

would be [UVar 2, UVar 3] or something alpha-equivalent, whereas the result of

freshenAll [UVar 1, UVar 1]

would be [UVar 2, UVar 2] or something alpha-equivalent.

Since: 0.7.0

# Helper functions

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

fullprune :: BindingMonad t v m => UTerm t v -> m (UTerm t v) 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 t v m => UTerm t v -> m (UTerm t v) 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 t v m => v -> UTerm t v -> m Bool Source #

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.