Copyright	(C) 2018-19 Carlo Nucera
License	BSD-style (see the file LICENSE)
Maintainer	Carlo Nucera <meditans@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Generic.Unification.Unification

Contents

The Unifiable typeclass
A concrete transformer

Description

This module implements the unification algorithm described in `Efficient functional Unification and Substitution` by A.Dijkstra. The essential feature of the algorithm is that it is quite fast, and it dispenses with unification checks during the unification phase (you can perform it when applying substitutions directly). Further optimisations may come in future.

Synopsis

class Substitutable a => Unifiable a where
- unify :: Monad m => Term a -> Term a -> UnificationT m (Term a)
- checkOccurs :: Monad m => Term a -> UnificationT m (Term a)
type SubstitutableGenConstraints a = (Typeable a, Generic a, HasDatatypeInfo a, Eq a, Show a, Substitutable a, All2 (Compose Show Term) (Code a), All2 (Compose Eq Term) (Code a), All2 (And Unifiable Substitutable) (Code a))
data UnificationError
- = IncompatibleUnification
- | OccursCheckFailed
newtype UnificationT m a = Unification {
- unUnificationT :: StateT Substitution (ExceptT UnificationError m) a
}
evalUnificationT :: Monad m => UnificationT m a -> m (Either UnificationError a)
runUnificationT :: Monad m => UnificationT m a -> Substitution -> m (Either UnificationError (a, Substitution))

The Unifiable typeclass

class Substitutable a => Unifiable a where #

This is the class that offers the interface for unification. The user of the library is not supposed to add instances to this class.

Methods

unify :: Monad m => Term a -> Term a -> UnificationT m (Term a) #

Unify two values in the monad. This operation does not perform the occur check, for performance reasons and because you may not need it (for example when using non-recursive structures). If you want to be sure that your terms do not contain cycles, use the following function.

checkOccurs :: Monad m => Term a -> UnificationT m (Term a) #

This function will perform the occurs check, returning an equivalent term or a OccursCheckFailed exception. If you want to explicitly observe the occurs check failure, use @@ from the Substitutable class.

Instances

Unifiable Char #
Instance details Defined in Generic.Unification.Unification Methods unify :: Monad m => Term Char -> Term Char -> UnificationT m (Term Char) # checkOccurs :: Monad m => Term Char -> UnificationT m (Term Char) # uni :: Monad m => Substitution -> Term Char -> Term Char -> UnificationT m (Term Char)
Unifiable Int #
Instance details Defined in Generic.Unification.Unification Methods unify :: Monad m => Term Int -> Term Int -> UnificationT m (Term Int) # checkOccurs :: Monad m => Term Int -> UnificationT m (Term Int) # uni :: Monad m => Substitution -> Term Int -> Term Int -> UnificationT m (Term Int)
SubstitutableGenConstraints a => Unifiable a #
Instance details Defined in Generic.Unification.Unification Methods unify :: Monad m => Term a -> Term a -> UnificationT m (Term a) # checkOccurs :: Monad m => Term a -> UnificationT m (Term a) # uni :: Monad m => Substitution -> Term a -> Term a -> UnificationT m (Term a)
Unifiable String #
Instance details Defined in Generic.Unification.Unification Methods unify :: Monad m => Term String -> Term String -> UnificationT m (Term String) # checkOccurs :: Monad m => Term String -> UnificationT m (Term String) # uni :: Monad m => Substitution -> Term String -> Term String -> UnificationT m (Term String)

type SubstitutableGenConstraints a = (Typeable a, Generic a, HasDatatypeInfo a, Eq a, Show a, Substitutable a, All2 (Compose Show Term) (Code a), All2 (Compose Eq Term) (Code a), All2 (And Unifiable Substitutable) (Code a)) #

A constraint synonym that indicates all the constraints a type should have to be automatically part of the Unifiable class.

data UnificationError #

Encodes what could go wrong in unification. The monad UnificationT is instance of MonadError UnificationError.

Constructors

IncompatibleUnification	Two terms that were unified have incompatible shapes.
OccursCheckFailed	A term failed the occurs check (it was cyclic).

Instances

Show UnificationError #
Instance details Defined in Generic.Unification.Unification Methods showsPrec :: Int -> UnificationError -> ShowS # show :: UnificationError -> String # showList :: [UnificationError] -> ShowS #
MonadError UnificationError Logic #
Instance details Defined in Generic.Unification.Hinze Methods throwError :: UnificationError -> Logic a # catchError :: Logic a -> (UnificationError -> Logic a) -> Logic a #
Monad m => MonadError UnificationError (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods throwError :: UnificationError -> UnificationT m a # catchError :: UnificationT m a -> (UnificationError -> UnificationT m a) -> UnificationT m a #

A concrete transformer

newtype UnificationT m a #

A monad transformer to capture the threading of a substitution and the errors that can happen during unification. This is a monad transformer because you may want to change the monads at the bottom of the stack, for example to put there a non-determinism monad.

Constructors

Unification
Fields unUnificationT :: StateT Substitution (ExceptT UnificationError m) a

Instances

Monad m => MonadState Substitution (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods get :: UnificationT m Substitution # put :: Substitution -> UnificationT m () # state :: (Substitution -> (a, Substitution)) -> UnificationT m a #
Monad m => MonadError UnificationError (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods throwError :: UnificationError -> UnificationT m a # catchError :: UnificationT m a -> (UnificationError -> UnificationT m a) -> UnificationT m a #
Monad m => Monad (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods (>>=) :: UnificationT m a -> (a -> UnificationT m b) -> UnificationT m b # (>>) :: UnificationT m a -> UnificationT m b -> UnificationT m b # return :: a -> UnificationT m a # fail :: String -> UnificationT m a #
Functor m => Functor (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods fmap :: (a -> b) -> UnificationT m a -> UnificationT m b # (<$) :: a -> UnificationT m b -> UnificationT m a #
Monad m => Applicative (UnificationT m) #
Instance details Defined in Generic.Unification.Unification Methods pure :: a -> UnificationT m a # (<>) :: UnificationT m (a -> b) -> UnificationT m a -> UnificationT m b # liftA2 :: (a -> b -> c) -> UnificationT m a -> UnificationT m b -> UnificationT m c # (>) :: UnificationT m a -> UnificationT m b -> UnificationT m b # (<*) :: UnificationT m a -> UnificationT m b -> UnificationT m a #

evalUnificationT :: Monad m => UnificationT m a -> m (Either UnificationError a) #

Calculate the result of an UnificationT computation.

runUnificationT :: Monad m => UnificationT m a -> Substitution -> m (Either UnificationError (a, Substitution)) #

Unwrap UnificationT to its meaning.