Control.Unification.Types

This module defines the classes and primitive types used by unification and related functions.

Unification terms

data UTerm t v

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

Functor t => Monad (UTerm t)

Defined 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)

Defined in Control.Unification.Types

Methods

fmap :: (a -> b) -> UTerm t a -> UTerm t b

(<$) :: a -> UTerm t b -> UTerm t a

Functor t => Applicative (UTerm t)

Defined in Control.Unification.Types

Methods

pure :: 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)

Defined in Control.Unification.Types

Methods

fold :: 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)

Defined in Control.Unification.Types

Methods

traverse :: 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)

Defined in Control.Unification.Types

Methods

showsPrec :: Int -> UTerm t v -> ShowS

show :: UTerm t v -> String

showList :: [UTerm t v] -> ShowS

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

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

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

Errors

class Fallible t v a where

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

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

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

Fallible t v (UFailure t v)

Defined in Control.Unification.Types

Methods

occursFailure :: v -> UTerm t v -> UFailure t v

mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> UFailure t v

data UFailure t v

A concrete representation for the Fallible type class. Whenever possible, you should prefer to keep the concrete representation abstract by using the Fallible class instead.

Updated: 0.10.0 Used to be called UnificationFailure. Removed the UnknownError constructor, and the Control.Monad.Error.Error instance associated with it. Renamed OccursIn constructor to OccursFailure; and renamed TermMismatch constructor to MismatchFailure.

Updated: 0.8.1 added Functor, Foldable, and Traversable instances.

Constructors

OccursFailure v (UTerm t v)

MismatchFailure (t (UTerm t v)) (t (UTerm t v))

Instances

Fallible t v (UFailure t v)

Defined in Control.Unification.Types

Methods

occursFailure :: v -> UTerm t v -> UFailure t v

mismatchFailure :: t (UTerm t v) -> t (UTerm t v) -> UFailure t v

Functor t => Functor (UFailure t)

Defined in Control.Unification.Types

Methods

fmap :: (a -> b) -> UFailure t a -> UFailure t b

(<$) :: a -> UFailure t b -> UFailure t a

Foldable t => Foldable (UFailure t)

Defined in Control.Unification.Types

Methods

fold :: Monoid m => UFailure t m -> m

foldMap :: Monoid m => (a -> m) -> UFailure t a -> m

foldMap' :: Monoid m => (a -> m) -> UFailure t a -> m

foldr :: (a -> b -> b) -> b -> UFailure t a -> b

foldr' :: (a -> b -> b) -> b -> UFailure t a -> b

foldl :: (b -> a -> b) -> b -> UFailure t a -> b

foldl' :: (b -> a -> b) -> b -> UFailure t a -> b

foldr1 :: (a -> a -> a) -> UFailure t a -> a

foldl1 :: (a -> a -> a) -> UFailure t a -> a

toList :: UFailure t a -> [a]

null :: UFailure t a -> Bool

length :: UFailure t a -> Int

elem :: Eq a => a -> UFailure t a -> Bool

maximum :: Ord a => UFailure t a -> a

minimum :: Ord a => UFailure t a -> a

sum :: Num a => UFailure t a -> a

product :: Num a => UFailure t a -> a

Traversable t => Traversable (UFailure t)

Defined in Control.Unification.Types

Methods

traverse :: Applicative f => (a -> f b) -> UFailure t a -> f (UFailure t b)

sequenceA :: Applicative f => UFailure t (f a) -> f (UFailure t a)

mapM :: Monad m => (a -> m b) -> UFailure t a -> m (UFailure t b)

sequence :: Monad m => UFailure t (m a) -> m (UFailure t a)

(Show (t (UTerm t v)), Show v) => Show (UFailure t v)

Defined in Control.Unification.Types

Methods

showsPrec :: Int -> UFailure t v -> ShowS

show :: UFailure t v -> String

showList :: [UFailure t v] -> ShowS

Basic type classes

class Traversable t => Unifiable t where

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)))

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)))

Instances

Unifiable Par1

Defined in Control.Unification.Types

Methods

zipMatch :: Par1 a -> Par1 a -> Maybe (Par1 (Either a (a, a)))

Unifiable (V1 :: Type -> Type)

Defined in Control.Unification.Types

Methods

zipMatch :: V1 a -> V1 a -> Maybe (V1 (Either a (a, a)))

Unifiable (U1 :: Type -> Type)

Defined in Control.Unification.Types

Methods

zipMatch :: U1 a -> U1 a -> Maybe (U1 (Either a (a, a)))

Unifiable f => Unifiable (Rec1 f)

Defined in Control.Unification.Types

Methods

zipMatch :: Rec1 f a -> Rec1 f a -> Maybe (Rec1 f (Either a (a, a)))

Eq c => Unifiable (K1 i c :: Type -> Type)

Defined in Control.Unification.Types

Methods

zipMatch :: K1 i c a -> K1 i c a -> Maybe (K1 i c (Either a (a, a)))

(Unifiable f, Unifiable g) => Unifiable (f :+: g)

Defined in Control.Unification.Types

Methods

zipMatch :: (f :+: g) a -> (f :+: g) a -> Maybe ((f :+: g) (Either a (a, a)))

(Unifiable f, Unifiable g) => Unifiable (f :*: g)

Defined in Control.Unification.Types

Methods

zipMatch :: (f :*: g) a -> (f :*: g) a -> Maybe ((f :*: g) (Either a (a, a)))

Unifiable f => Unifiable (M1 i c f)

Defined in Control.Unification.Types

Methods

zipMatch :: M1 i c f a -> M1 i c f a -> Maybe (M1 i c f (Either a (a, a)))

(Unifiable f, Unifiable g) => Unifiable (f :.: g)

Defined in Control.Unification.Types

Methods

zipMatch :: (f :.: g) a -> (f :.: g) a -> Maybe ((f :.: g) (Either a (a, a)))

class Eq v => Variable v where

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

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

Variable IntVar

Defined in Control.Unification.IntVar

Methods

getVarID :: IntVar -> Int

Variable (STVar s t)

Defined in Control.Unification.STVar

Methods

getVarID :: STVar s t -> Int

Variable (STRVar s t)

Defined in Control.Unification.Ranked.STVar

Methods

getVarID :: STRVar s t -> Int

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

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

lookupVar, freeVar, bindVar

Methods

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

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

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

newVar :: UTerm t v -> m v

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 ()

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

Instances

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

Defined in Control.Unification.IntVar

Methods

lookupVar :: IntVar -> IntBindingT t m (Maybe (UTerm t IntVar))

freeVar :: IntBindingT t m IntVar

newVar :: UTerm t IntVar -> IntBindingT t m IntVar

bindVar :: IntVar -> UTerm t IntVar -> IntBindingT t m ()

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

Defined in Control.Unification.Ranked.IntVar

Methods

lookupVar :: IntVar -> IntRBindingT t m (Maybe (UTerm t IntVar))

freeVar :: IntRBindingT t m IntVar

newVar :: UTerm t IntVar -> IntRBindingT t m IntVar

bindVar :: IntVar -> UTerm t IntVar -> IntRBindingT t m ()

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

Defined in Control.Unification.STVar

Methods

lookupVar :: STVar s t -> STBinding s (Maybe (UTerm t (STVar s t)))

freeVar :: STBinding s (STVar s t)

newVar :: UTerm t (STVar s t) -> STBinding s (STVar s t)

bindVar :: STVar s t -> UTerm t (STVar s t) -> STBinding s ()

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

Defined in Control.Unification.Ranked.STVar

Methods

lookupVar :: STRVar s t -> STRBinding s (Maybe (UTerm t (STRVar s t)))

freeVar :: STRBinding s (STRVar s t)

newVar :: UTerm t (STRVar s t) -> STRBinding s (STRVar s t)

bindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()

Weighted path compression

data Rank t v

The target of variables for RankedBindingMonads. In order to support weighted path compression, each variable is bound to both another term (possibly) and also a "rank" which is related to the length of the variable chain to the term it's ultimately bound to.

The rank can be at most log V, where V is the total number of variables in the unification problem. Thus, A Word8 is sufficient for 2^(2^8) variables, which is far more than can be indexed by getVarID even on 64-bit architectures.

Constructors

Rank !Word8 !(Maybe (UTerm t v))

Instances

(Show v, Show (t (UTerm t v))) => Show (Rank t v)

Defined in Control.Unification.Types

Methods

showsPrec :: Int -> Rank t v -> ShowS

show :: Rank t v -> String

showList :: [Rank t v] -> ShowS

class BindingMonad t v m => RankedBindingMonad t v m | m t -> v, v m -> t where

An advanced class for BindingMonads which also support weighted path compression. The weightedness adds non-trivial implementation complications; so even though weighted path compression is asymptotically optimal, the constant factors may make it worthwhile to stick with the unweighted path compression supported by BindingMonad.

Minimal complete definition

lookupRankVar, incrementRank

Methods

lookupRankVar :: v -> m (Rank t v)

Given a variable pointing to UTerm t v, return its rank and the term it's bound to.

incrementRank :: v -> m ()

Increase the rank of a variable by one.

incrementBindVar :: v -> UTerm t v -> m ()

Bind a variable to a term and increment the rank at the same time. The default implementation is:

incrementBindVar t v = do { incrementRank v ; bindVar v t }

Instances

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

Defined in Control.Unification.Ranked.IntVar

Methods

lookupRankVar :: IntVar -> IntRBindingT t m (Rank t IntVar)

incrementRank :: IntVar -> IntRBindingT t m ()

incrementBindVar :: IntVar -> UTerm t IntVar -> IntRBindingT t m ()

Unifiable t => RankedBindingMonad t (STRVar s t) (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

lookupRankVar :: STRVar s t -> STRBinding s (Rank t (STRVar s t))

incrementRank :: STRVar s t -> STRBinding s ()

incrementBindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()