Unbound.Generics.Unify

Unification for unbound-generics

Main unification functions

unify' :: (Unification t m, Unify t t) => t -> t -> m (Either UnificationError t)

Tries to unify two terms, giving back a common term, or a unification error.

This variant requires the terms to be of the same type t as the variables within them.

class Subst t a => Unify t a where

Declares the ability to unify values of type a containing variables of type t.

Minimal complete definition

Nothing

Methods

unify :: Unification t m => a -> a -> m (Either UnificationError a)

Tries to unify two terms, giving back a common term, or a unification error.

default unify :: (Generic a, GUnify t (Rep a), Unification t m) => a -> a -> m (Either UnificationError a)

Instances

Unify t String

Defined in Unbound.Generics.Unify

Methods

unify :: Unification t m => String -> String -> m (Either UnificationError String)

Unify t (Name t)

Defined in Unbound.Generics.Unify

Methods

unify :: Unification t m => Name t -> Name t -> m (Either UnificationError (Name t))

Unify t a => Unify t [a]

Defined in Unbound.Generics.Unify

Methods

unify :: Unification t m => [a] -> [a] -> m (Either UnificationError [a])

Information about errors

type UnificationError = (Path, UnificationErrorCause)

Path to navigate to a unification error.

data UnificationErrorCause where

Potential causes for unification errors.

Constructors

OccursCheck :: forall t. Name t -> t -> UnificationErrorCause

DifferentConstructor :: UnificationErrorCause

DifferentListLength :: UnificationErrorCause

Instances

Show UnificationErrorCause

Defined in Unbound.Generics.Unify

Methods

showsPrec :: Int -> UnificationErrorCause -> ShowS

show :: UnificationErrorCause -> String

showList :: [UnificationErrorCause] -> ShowS

type Path = [PathElement]

data PathElement

Ways to navigate within a value.

Constructors

PathConstructor String

PathSelector String

PathIndex Int

Instances

Show PathElement

Defined in Unbound.Generics.Unify

Methods

showsPrec :: Int -> PathElement -> ShowS

show :: PathElement -> String

showList :: [PathElement] -> ShowS

Eq PathElement

Defined in Unbound.Generics.Unify

Methods

(==) :: PathElement -> PathElement -> Bool

(/=) :: PathElement -> PathElement -> Bool

Unification as a monad

class Monad m => Unification t (m :: Type -> Type) where

Stateful storage of substitutions as required for unification.

The substitution operates only on terms and variables of type t.

Methods

currentSubst :: m (Map (Name t) t)

Obtain the current substitution.

recordSubst :: Name t -> t -> m ()

Add a new substitution.

Instances

Monad m => Unification t (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

currentSubst :: UnificationMT t m (Map (Name t) t)

recordSubst :: Name t -> t -> UnificationMT t m ()

Base implementation

type UnificationM t = UnificationMT t Identity

runUnification :: UnificationM t a -> (a, Map (Name t) t)

Including fresh creation

type UnificationFreshM t = UnificationMT t FreshM

runUnificationFresh :: UnificationFreshM t a -> (a, Map (Name t) t)

As a monad transformer

newtype UnificationMT t (m :: Type -> Type) a

Constructors

UnificationMT

Fields

• unUnificationMT :: StateT (Map (Name t) t) m a

Instances

Monad m => Unification t (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

currentSubst :: UnificationMT t m (Map (Name t) t)

recordSubst :: Name t -> t -> UnificationMT t m ()

Monad m => Applicative (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

pure :: a -> UnificationMT t m a

(<*>) :: UnificationMT t m (a -> b) -> UnificationMT t m a -> UnificationMT t m b

liftA2 :: (a -> b -> c) -> UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m c

(*>) :: UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b

(<*) :: UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m a

Functor m => Functor (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

fmap :: (a -> b) -> UnificationMT t m a -> UnificationMT t m b

(<$) :: a -> UnificationMT t m b -> UnificationMT t m a

Monad m => Monad (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

(>>=) :: UnificationMT t m a -> (a -> UnificationMT t m b) -> UnificationMT t m b

(>>) :: UnificationMT t m a -> UnificationMT t m b -> UnificationMT t m b

return :: a -> UnificationMT t m a

Fresh m => Fresh (UnificationMT t m)

Defined in Unbound.Generics.Unify

Methods

fresh :: Name a -> UnificationMT t m (Name a)

runUnificationT :: forall t m a. Monad m => UnificationMT t m a -> m (a, Map (Name t) t)

Generic methods

class GUnify t (f :: k -> Type) where

Implementation of unification using GHC.Generics.

Methods

gunify :: forall m (a :: k). Unification t m => f a -> f a -> m (Either UnificationError (f a))

Instances

GUnify t (U1 :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => U1 a -> U1 a -> m (Either UnificationError (U1 a))

(GUnify t f, GUnify t g) => GUnify t (f :*: g :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => (f :*: g) a -> (f :*: g) a -> m (Either UnificationError ((f :*: g) a))

(GUnify t f, GUnify t g) => GUnify t (f :+: g :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => (f :+: g) a -> (f :+: g) a -> m (Either UnificationError ((f :+: g) a))

(Constructor c, GUnify t f) => GUnify t (C1 c f :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => C1 c f a -> C1 c f a -> m (Either UnificationError (C1 c f a))

GUnify t f => GUnify t (D1 d f :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => D1 d f a -> D1 d f a -> m (Either UnificationError (D1 d f a))

Unify t a => GUnify t (K1 i a :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a0 :: k). Unification t m => K1 i a a0 -> K1 i a a0 -> m (Either UnificationError (K1 i a a0))

(Selector s, GUnify t f) => GUnify t (S1 s f :: k -> Type)

Defined in Unbound.Generics.Unify

Methods

gunify :: forall m (a :: k). Unification t m => S1 s f a -> S1 s f a -> m (Either UnificationError (S1 s f a))