Portability | semi-portable (MPTCs, fundeps,...) |
---|---|
Stability | experimental |
Maintainer | wren@community.haskell.org |
Safe Haskell | None |
This module defines the classes and primitive types used by unification and related functions.
- data UTerm t v
- freeze :: Traversable t => UTerm t v -> Maybe (Fix t)
- unfreeze :: Functor t => Fix t -> UTerm t v
- data UnificationFailure t v
- = OccursIn v (UTerm t v)
- | TermMismatch (t (UTerm t v)) (t (UTerm t v))
- | UnknownError String
- class Traversable t => Unifiable t where
- class Eq v => Variable v where
- class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> t where
- data Rank t v = Rank !Word8 !(Maybe (UTerm t v))
- class BindingMonad t v m => RankedBindingMonad t v m | m t -> v, v m -> t where
- lookupRankVar :: v -> m (Rank t v)
- incrementRank :: v -> m ()
- incrementBindVar :: v -> UTerm t v -> m ()
Unification terms
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.
Functor t => Monad (UTerm t) | |
Functor t => Functor (UTerm t) | |
(Functor t, MonadPlus t) => MonadPlus (UTerm t) | |
Functor t => Applicative (UTerm t) | |
Foldable t => Foldable (UTerm t) | |
Traversable t => Traversable (UTerm t) | |
Alternative t => Alternative (UTerm t) | |
(Show v, Show (t (UTerm t v))) => Show (UTerm t v) |
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.
Errors
data UnificationFailure t v 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.
Updated: 0.8.1 added Functor
, Foldable
, and Traversable
instances.
OccursIn v (UTerm t v) | 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 (UTerm t v)) (t (UTerm t v)) | The top-most level of the terms do not match (according
to |
UnknownError String | Required for the |
Functor t => Functor (UnificationFailure t) | |
Foldable t => Foldable (UnificationFailure t) | |
Traversable t => Traversable (UnificationFailure t) | |
(Show (t (UTerm t v)), Show v) => Show (UnificationFailure t v) | |
Error (UnificationFailure t v) |
Basic type classes
class Traversable t => Unifiable t whereSource
class Eq v => Variable v whereSource
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
.
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
class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> 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 -> 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.
Generate a new free variable guaranteed to be fresh in
m
.
newVar :: UTerm t v -> m vSource
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.
(Unifiable t, Applicative m, Monad m) => BindingMonad t IntVar (IntBindingT t m) | |
(Unifiable t, Applicative m, Monad m) => BindingMonad t IntVar (IntRBindingT t m) | |
Unifiable t => BindingMonad t (STVar s t) (STBinding s) | |
Unifiable t => BindingMonad t (STRVar s t) (STRBinding s) |
Weighted path compression
The target of variables for RankedBindingMonad
s. 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.
class BindingMonad t v m => RankedBindingMonad t v m | m t -> v, v m -> t whereSource
An advanced class for BindingMonad
s 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
.
lookupRankVar :: v -> m (Rank t v)Source
Given a variable pointing to UTerm t v
, return its
rank and the term it's bound to.
incrementRank :: v -> m ()Source
Increase the rank of a variable by one.
incrementBindVar :: v -> UTerm t v -> m ()Source
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 }
(Unifiable t, Applicative m, Monad m) => RankedBindingMonad t IntVar (IntRBindingT t m) | |
Unifiable t => RankedBindingMonad t (STRVar s t) (STRBinding s) |