Control.Monad.Unify

Documentation

newtype Unknown

Untyped unification variables

Constructors

Unknown

Fields

runUnknown :: Int

The underlying integer representing the unification variable

Instances

Eq Unknown

Data Unknown

Ord Unknown

Show Unknown

Typeable Unknown

class (Typeable t, Data t) => Partial t where

A type which can contain unification variables

Methods

unknown :: Unknown -> t

isUnknown :: t -> Maybe Unknown

class Partial t => Unifiable m t | t -> m where

Identifies types which support unification

Methods

(=?=) :: t -> t -> UnifyT t m ()

data Substitution t

A substitution maintains a mapping from unification variables to their values

Constructors

Substitution

Fields

runSubstitution :: HashMap Int t

Instances

Partial t => Monoid (Substitution t)

($?) :: Partial t => Substitution t -> t -> t

Apply a substitution to a value

data UnifyState t

State required for type checking

Constructors

UnifyState

Fields

unifyNextVar :: Int

The next fresh unification variable

unifyCurrentSubstitution :: Substitution t

The current substitution

defaultUnifyState :: Partial t => UnifyState t

An empty UnifyState

newtype UnifyT t m a

The type checking monad, which provides the state of the type checker, and error reporting capabilities

Constructors

UnifyT

Fields

unUnify :: StateT (UnifyState t) (ErrorT String m) a

Instances

Monad m => MonadError String (UnifyT t m)

MonadState s m => MonadState s (UnifyT t m)

Monad m => Monad (UnifyT t m)

Functor m => Functor (UnifyT t m)

Monad m => MonadPlus (UnifyT t m)

(Monad m, Functor m) => Applicative (UnifyT t m)

unknowns :: Data d => d -> [Unknown]

Collect all unknowns occurring inside a value

runUnify :: UnifyState t -> UnifyT t m a -> m (Either String (a, UnifyState t))

Run a computation in the Unify monad, failing with an error, or succeeding with a return value and the new next unification variable

substituteOne :: Partial t => Unknown -> t -> Substitution t

Substitute a single unification variable

(=:=) :: (Monad m, Unifiable m t) => Unknown -> t -> UnifyT t m ()

Replace a unification variable with the specified value in the current substitution

occursCheck :: (Monad m, Partial t) => Unknown -> t -> UnifyT t m ()

Perform the occurs check, to make sure a unification variable does not occur inside a value

fresh' :: Monad m => UnifyT t m Unknown

Generate a fresh untyped unification variable

fresh :: (Monad m, Partial t) => UnifyT t m t

Generate a fresh unification variable at a specific type