Safe Haskell	None
Language	Haskell2010

Generic.Unification.Hinze

Description

Following the paper "Prolog control constructs in a functional setting" by Hinze, because I only want a clear denotational semantic for now. This is done as an experiment, and will not be part of the final package.

Synopsis

class Monad m => Backtr m where
- flop :: m a
- amb :: m a -> m a -> m a
- once :: m a -> m (Maybe a)
- sols :: m a -> m [a]
class Backtr m => Cut m where
- cut :: m ()
- call :: m a -> m a
naf :: Backtr m => m a -> m ()
naf2 :: Cut m => m a -> m ()
only :: Cut m => a -> m a
newtype BacktrT m a = BacktrT {
- (>>-) :: forall ans. CPS a (m ans -> m ans)
}
newtype CutT m a = CutT {
- (>>--) :: forall ans. CPS a (m (Answer m ans) -> m (Answer m ans))
}
newtype Logic a = Logic {
- unLogic :: UnificationT (CutT Identity) a
}
runLogic :: Logic a -> [Either UnificationError (a, Substitution)]
evalLogic :: Logic a -> [a]
(===) :: Unifiable a => Term a -> Term a -> Logic (Term a)

Documentation

class Monad m => Backtr m where #

Important classes

Methods

flop :: m a #

No solutions, corresponds to fail in prolog

amb :: m a -> m a -> m a #

Non-deterministing choice between two branches

once :: m a -> m (Maybe a) #

Encapsulation, find one solution

sols :: m a -> m [a] #

Encapsulation, find all solutions

Instances

Backtr Logic #
Instance details Defined in Generic.Unification.Hinze Methods flop :: Logic a # amb :: Logic a -> Logic a -> Logic a # once :: Logic a -> Logic (Maybe a) # sols :: Logic a -> Logic [a] #
Monad m => Backtr (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: CutT m a # amb :: CutT m a -> CutT m a -> CutT m a # once :: CutT m a -> CutT m (Maybe a) # sols :: CutT m a -> CutT m [a] #
Monad m => Backtr (BacktrT m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: BacktrT m a # amb :: BacktrT m a -> BacktrT m a -> BacktrT m a # once :: BacktrT m a -> BacktrT m (Maybe a) # sols :: BacktrT m a -> BacktrT m [a] #
Backtr m => Backtr (ExceptT e m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: ExceptT e m a # amb :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a # once :: ExceptT e m a -> ExceptT e m (Maybe a) # sols :: ExceptT e m a -> ExceptT e m [a] #
Backtr m => Backtr (StateT s m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: StateT s m a # amb :: StateT s m a -> StateT s m a -> StateT s m a # once :: StateT s m a -> StateT s m (Maybe a) # sols :: StateT s m a -> StateT s m [a] #

class Backtr m => Cut m where #

Methods

cut :: m () #

like in prolog, cut discards choicepoints

call :: m a -> m a #

to delimit the effect of a cut in a region

Instances

Cut Logic #
Instance details Defined in Generic.Unification.Hinze Methods cut :: Logic () # call :: Logic a -> Logic a #
Monad m => Cut (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods cut :: CutT m () # call :: CutT m a -> CutT m a #
Cut m => Cut (ExceptT e m) #
Instance details Defined in Generic.Unification.Hinze Methods cut :: ExceptT e m () # call :: ExceptT e m a -> ExceptT e m a #
Cut m => Cut (StateT s m) #
Instance details Defined in Generic.Unification.Hinze Methods cut :: StateT s m () # call :: StateT s m a -> StateT s m a #

naf :: Backtr m => m a -> m () #

Negation as failure

naf2 :: Cut m => m a -> m () #

Subtly different negation as failure

only :: Cut m => a -> m a #

Equivalent to once/1 in prolog. Note, the once function in the typeclass is the encapsulated version of this operation.

newtype BacktrT m a #

Constructors

BacktrT
Fields (>>-) :: forall ans. CPS a (m ans -> m ans)

Instances

Monad (BacktrT m) #
Instance details Defined in Generic.Unification.Hinze Methods (>>=) :: BacktrT m a -> (a -> BacktrT m b) -> BacktrT m b # (>>) :: BacktrT m a -> BacktrT m b -> BacktrT m b # return :: a -> BacktrT m a # fail :: String -> BacktrT m a #
Functor (BacktrT m) #
Instance details Defined in Generic.Unification.Hinze Methods fmap :: (a -> b) -> BacktrT m a -> BacktrT m b # (<$) :: a -> BacktrT m b -> BacktrT m a #
Applicative (BacktrT m) #
Instance details Defined in Generic.Unification.Hinze Methods pure :: a -> BacktrT m a # (<>) :: BacktrT m (a -> b) -> BacktrT m a -> BacktrT m b # liftA2 :: (a -> b -> c) -> BacktrT m a -> BacktrT m b -> BacktrT m c # (>) :: BacktrT m a -> BacktrT m b -> BacktrT m b # (<*) :: BacktrT m a -> BacktrT m b -> BacktrT m a #
Monad m => Backtr (BacktrT m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: BacktrT m a # amb :: BacktrT m a -> BacktrT m a -> BacktrT m a # once :: BacktrT m a -> BacktrT m (Maybe a) # sols :: BacktrT m a -> BacktrT m [a] #

newtype CutT m a #

Constructors

CutT
Fields (>>--) :: forall ans. CPS a (m (Answer m ans) -> m (Answer m ans))

Instances

Monad (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods (>>=) :: CutT m a -> (a -> CutT m b) -> CutT m b # (>>) :: CutT m a -> CutT m b -> CutT m b # return :: a -> CutT m a # fail :: String -> CutT m a #
Functor (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods fmap :: (a -> b) -> CutT m a -> CutT m b # (<$) :: a -> CutT m b -> CutT m a #
Applicative (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods pure :: a -> CutT m a # (<>) :: CutT m (a -> b) -> CutT m a -> CutT m b # liftA2 :: (a -> b -> c) -> CutT m a -> CutT m b -> CutT m c # (>) :: CutT m a -> CutT m b -> CutT m b # (<*) :: CutT m a -> CutT m b -> CutT m a #
Monad m => Cut (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods cut :: CutT m () # call :: CutT m a -> CutT m a #
Monad m => Backtr (CutT m) #
Instance details Defined in Generic.Unification.Hinze Methods flop :: CutT m a # amb :: CutT m a -> CutT m a -> CutT m a # once :: CutT m a -> CutT m (Maybe a) # sols :: CutT m a -> CutT m [a] #

newtype Logic a #

Constructors

Logic
Fields unLogic :: UnificationT (CutT Identity) a

Instances

Monad Logic #
Instance details Defined in Generic.Unification.Hinze Methods (>>=) :: Logic a -> (a -> Logic b) -> Logic b # (>>) :: Logic a -> Logic b -> Logic b # return :: a -> Logic a # fail :: String -> Logic a #
Functor Logic #
Instance details Defined in Generic.Unification.Hinze Methods fmap :: (a -> b) -> Logic a -> Logic b # (<$) :: a -> Logic b -> Logic a #
Applicative Logic #
Instance details Defined in Generic.Unification.Hinze Methods pure :: a -> Logic a # (<>) :: Logic (a -> b) -> Logic a -> Logic b # liftA2 :: (a -> b -> c) -> Logic a -> Logic b -> Logic c # (>) :: Logic a -> Logic b -> Logic b # (<*) :: Logic a -> Logic b -> Logic a #
Cut Logic #
Instance details Defined in Generic.Unification.Hinze Methods cut :: Logic () # call :: Logic a -> Logic a #
Backtr Logic #
Instance details Defined in Generic.Unification.Hinze Methods flop :: Logic a # amb :: Logic a -> Logic a -> Logic a # once :: Logic a -> Logic (Maybe a) # sols :: Logic a -> Logic [a] #
MonadState Substitution Logic #
Instance details Defined in Generic.Unification.Hinze Methods get :: Logic Substitution # put :: Substitution -> Logic () # state :: (Substitution -> (a, Substitution)) -> Logic a #
MonadError UnificationError Logic #
Instance details Defined in Generic.Unification.Hinze Methods throwError :: UnificationError -> Logic a # catchError :: Logic a -> (UnificationError -> Logic a) -> Logic a #

runLogic :: Logic a -> [Either UnificationError (a, Substitution)] #

evalLogic :: Logic a -> [a] #

(===) :: Unifiable a => Term a -> Term a -> Logic (Term a) #