-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Simple generic unification algorithms.
--   
--   Simple generic unification algorithms.
@package unification-fd
@version 0.10.0.1


-- | This module provides a fixed point operator on functor types. For
--   Haskell the least and greatest fixed points coincide, so we needn't
--   distinguish them. This abstract nonsense is helpful in conjunction
--   with other category theoretic tricks like Swierstra's functor
--   coproducts (not provided by this package). For more on the utility of
--   two-level recursive types, see:
--   
--   <ul>
--   <li>Tim Sheard (2001) <i>Generic Unification via Two-Level Types</i>
--   <i>and Paramterized Modules</i>, Functional Pearl, ICFP.</li>
--   <li>Tim Sheard &amp; Emir Pasalic (2004) <i>Two-Level Types and</i>
--   <i>Parameterized Modules</i>. JFP 14(5): 547--587. This is an expanded
--   version of Sheard (2001) with new examples.</li>
--   <li>Wouter Swierstra (2008) <i>Data types a la carte</i>, Functional
--   Pearl. JFP 18: 423--436.</li>
--   </ul>
module Data.Functor.Fixedpoint

-- | <tt>Fix f</tt> is a fix point of the <a>Functor</a> <tt>f</tt>. Note
--   that in Haskell the least and greatest fixed points coincide, so we
--   don't need to distinguish between <tt>Mu f</tt> and <tt>Nu f</tt>.
--   This type used to be called <tt>Y</tt>, hence the naming convention
--   for all the <tt>yfoo</tt> functions.
--   
--   This type lets us invoke category theory to get recursive types and
--   operations over them without the type checker complaining about
--   infinite types. The <a>Show</a> instance doesn't print the
--   constructors, for legibility.
newtype Fix f
Fix :: f (Fix f) -> Fix f
[unFix] :: Fix f -> f (Fix f)

-- | A higher-order map taking a natural transformation <tt>(f -&gt;
--   g)</tt> and lifting it to operate on <tt>Fix</tt>.
hmap :: (Functor f, Functor g) => (forall a. f a -> g a) -> Fix f -> Fix g

-- | A monadic variant of <a>hmap</a>.
hmapM :: (Functor f, Traversable g, Monad m) => (forall a. f a -> m (g a)) -> Fix f -> m (Fix g)

-- | A version of <a>fmap</a> for endomorphisms on the fixed point. That
--   is, this maps the function over the first layer of recursive
--   structure.
ymap :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f

-- | A monadic variant of <a>ymap</a>.
ymapM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)

-- | Take a Church encoding of a fixed point into the data representation
--   of the fixed point.
build :: (Functor f) => (forall r. (f r -> r) -> r) -> Fix f

-- | A pure catamorphism over the least fixed point of a functor. This
--   function applies the <tt>f</tt>-algebra from the bottom up over
--   <tt>Fix f</tt> to create some residual value.
cata :: (Functor f) => (f a -> a) -> (Fix f -> a)

-- | A catamorphism for monadic <tt>f</tt>-algebras. Alas, this isn't
--   wholly generic to <tt>Functor</tt> since it requires distribution of
--   <tt>f</tt> over <tt>m</tt> (provided by <a>sequence</a> or <a>mapM</a>
--   in <a>Traversable</a>).
--   
--   N.B., this orders the side effects from the bottom up.
cataM :: (Traversable f, Monad m) => (f a -> m a) -> (Fix f -> m a)

-- | A variant of <a>cata</a> which restricts the return type to being a
--   new fixpoint. Though more restrictive, it can be helpful when you
--   already have an algebra which expects the outermost <tt>Fix</tt>.
--   
--   If you don't like either <tt>fmap</tt> or <tt>cata</tt>, then maybe
--   this is what you were thinking?
ycata :: (Functor f) => (Fix f -> Fix f) -> Fix f -> Fix f

-- | Monadic variant of <a>ycata</a>.
ycataM :: (Traversable f, Monad m) => (Fix f -> m (Fix f)) -> Fix f -> m (Fix f)

-- | A pure anamorphism generating the greatest fixed point of a functor.
--   This function applies an <tt>f</tt>-coalgebra from the top down to
--   expand a seed into a <tt>Fix f</tt>.
ana :: (Functor f) => (a -> f a) -> (a -> Fix f)

-- | An anamorphism for monadic <tt>f</tt>-coalgebras. Alas, this isn't
--   wholly generic to <tt>Functor</tt> since it requires distribution of
--   <tt>f</tt> over <tt>m</tt> (provided by <a>sequence</a> or <a>mapM</a>
--   in <a>Traversable</a>).
--   
--   N.B., this orders the side effects from the top down.
anaM :: (Traversable f, Monad m) => (a -> m (f a)) -> (a -> m (Fix f))

-- | <pre>
--   hylo phi psi == cata phi . ana psi
--   </pre>
hylo :: (Functor f) => (f b -> b) -> (a -> f a) -> (a -> b)

-- | <pre>
--   hyloM phiM psiM == cataM phiM &lt;=&lt; anaM psiM
--   </pre>
hyloM :: (Traversable f, Monad m) => (f b -> m b) -> (a -> m (f a)) -> (a -> m b)
instance GHC.Show.Show (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Show.Show (Data.Functor.Fixedpoint.Fix f)
instance GHC.Classes.Eq (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Classes.Eq (Data.Functor.Fixedpoint.Fix f)
instance GHC.Classes.Ord (f (Data.Functor.Fixedpoint.Fix f)) => GHC.Classes.Ord (Data.Functor.Fixedpoint.Fix f)


-- | This module defines the classes and primitive types used by
--   unification and related functions.
module Control.Unification.Types

-- | The type of terms generated by structures <tt>t</tt> over variables
--   <tt>v</tt>. The structure type should implement <a>Unifiable</a> and
--   the variable type should implement <a>Variable</a>.
--   
--   The <a>Show</a> instance doesn't show the constructors, in order to
--   improve legibility for large terms.
--   
--   All the category theoretic instances (<a>Functor</a>, <a>Foldable</a>,
--   <a>Traversable</a>,...) 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.
data UTerm t v

-- | A unification variable.
UVar :: !v -> UTerm t v

-- | Some structure containing subterms.
UTerm :: !(t (UTerm t v)) -> UTerm t v

-- | <i>O(n)</i>. Extract a pure term from a mutable term, or return
--   <tt>Nothing</tt> if the mutable term actually contains variables.
--   N.B., this function is pure, so you should manually apply bindings
--   before calling it.
freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)

-- | <i>O(n)</i>. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> UTerm t v

-- | 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.
--   
--   This is a finally-tagless encoding of the <a>UFailure</a> data type so
--   that we can abstract over clients adding additional domain-specific
--   failure modes, introducing monoid instances, etc.
--   
--   <i>Since: 0.10.0</i>
class Fallible t v a

-- | 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 <tt>a = Foo a</tt>" error.
--   
--   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.
occursFailure :: Fallible t v a => v -> UTerm t v -> a

-- | The top-most level of the terms do not match (according to
--   <a>zipMatch</a>). In logic programming this should simply be treated
--   as unification failure; in type checking this should result in a
--   "could not match expected type <tt>Foo</tt> with inferred type
--   <tt>Bar</tt>" error.
mismatchFailure :: Fallible t v a => t (UTerm t v) -> t (UTerm t v) -> a

-- | A concrete representation for the <a>Fallible</a> type class. Whenever
--   possible, you should prefer to keep the concrete representation
--   abstract by using the <a>Fallible</a> class instead.
--   
--   <i>Updated: 0.10.0</i> Used to be called <tt>UnificationFailure</tt>.
--   Removed the <tt>UnknownError</tt> constructor, and the
--   <tt>Control.Monad.Error.Error</tt> instance associated with it.
--   Renamed <tt>OccursIn</tt> constructor to <tt>OccursFailure</tt>; and
--   renamed <tt>TermMismatch</tt> constructor to <tt>MismatchFailure</tt>.
--   
--   <i>Updated: 0.8.1</i> added <a>Functor</a>, <a>Foldable</a>, and
--   <a>Traversable</a> instances.
data UFailure t v
OccursFailure :: v -> (UTerm t v) -> UFailure t v
MismatchFailure :: (t (UTerm t v)) -> (t (UTerm t v)) -> UFailure t v

-- | An implementation of syntactically unifiable structure. The
--   <tt>Traversable</tt> constraint is there because we also require terms
--   to be functors and require the distributivity of <a>sequence</a> or
--   <a>mapM</a>.
class (Traversable t) => Unifiable t

-- | Perform one level of equality testing for terms. If the term
--   constructors are unequal then return <tt>Nothing</tt>; if they are
--   equal, then return the one-level spine filled with resolved subterms
--   and/or pairs of subterms to be recursively checked.
zipMatch :: Unifiable t => t a -> t a -> Maybe (t (Either a (a, a)))

-- | An implementation of unification variables. The <a>Eq</a> requirement
--   is to determine whether two variables are equal <i>as variables</i>,
--   without considering what they are bound to. We use <a>Eq</a> rather
--   than having our own <tt>eqVar</tt> method so that clients can make use
--   of library functions which commonly assume <a>Eq</a>.
class (Eq v) => Variable v

-- | 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 <a>Eq</a>
--   instance:
--   
--   <tt>x == y</tt> if and only if <tt>getVarID x == getVarID y</tt>
getVarID :: Variable v => v -> Int

-- | 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 <tt>BindingMonad</tt>.
class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> t where newVar t = do { v <- freeVar; bindVar v t; return v }

-- | Given a variable pointing to <tt>UTerm t v</tt>, return the term it's
--   bound to, or <tt>Nothing</tt> if the variable is unbound.
lookupVar :: BindingMonad t v m => v -> m (Maybe (UTerm t v))

-- | Generate a new free variable guaranteed to be fresh in <tt>m</tt>.
freeVar :: BindingMonad t v m => m v

-- | Generate a new variable (fresh in <tt>m</tt>) bound to the given term.
--   The default implementation is:
--   
--   <pre>
--   newVar t = do { v &lt;- freeVar ; bindVar v t ; return v }
--   </pre>
newVar :: BindingMonad t v m => UTerm t v -> m v

-- | Bind a variable to a term, overriding any previous binding.
bindVar :: BindingMonad t v m => v -> UTerm t v -> m ()

-- | The target of variables for <a>RankedBindingMonad</a>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 <tt>log V</tt>, where <tt>V</tt> is the total
--   number of variables in the unification problem. Thus, A <tt>Word8</tt>
--   is sufficient for <tt>2^(2^8)</tt> variables, which is far more than
--   can be indexed by <a>getVarID</a> even on 64-bit architectures.
data Rank t v
Rank :: {-# UNPACK #-} !Word8 -> !(Maybe (UTerm t v)) -> Rank t v

-- | An advanced class for <a>BindingMonad</a>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
--   <a>BindingMonad</a>.
class (BindingMonad t v m) => RankedBindingMonad t v m | m t -> v, v m -> t where incrementBindVar v t = do { incrementRank v; bindVar v t }

-- | Given a variable pointing to <tt>UTerm t v</tt>, return its rank and
--   the term it's bound to.
lookupRankVar :: RankedBindingMonad t v m => v -> m (Rank t v)

-- | Increase the rank of a variable by one.
incrementRank :: RankedBindingMonad t v m => v -> m ()

-- | Bind a variable to a term and increment the rank at the same time. The
--   default implementation is:
--   
--   <pre>
--   incrementBindVar t v = do { incrementRank v ; bindVar v t }
--   </pre>
incrementBindVar :: RankedBindingMonad t v m => v -> UTerm t v -> m ()
instance (GHC.Show.Show v, GHC.Show.Show (t (Control.Unification.Types.UTerm t v))) => GHC.Show.Show (Control.Unification.Types.UTerm t v)
instance GHC.Base.Functor t => GHC.Base.Functor (Control.Unification.Types.UTerm t)
instance Data.Foldable.Foldable t => Data.Foldable.Foldable (Control.Unification.Types.UTerm t)
instance Data.Traversable.Traversable t => Data.Traversable.Traversable (Control.Unification.Types.UTerm t)
instance GHC.Base.Functor t => GHC.Base.Applicative (Control.Unification.Types.UTerm t)
instance GHC.Base.Functor t => GHC.Base.Monad (Control.Unification.Types.UTerm t)
instance GHC.Base.Alternative t => GHC.Base.Alternative (Control.Unification.Types.UTerm t)
instance (GHC.Base.Functor t, GHC.Base.MonadPlus t) => GHC.Base.MonadPlus (Control.Unification.Types.UTerm t)
instance Control.Unification.Types.Fallible t v (Control.Unification.Types.UFailure t v)
instance (GHC.Show.Show (t (Control.Unification.Types.UTerm t v)), GHC.Show.Show v) => GHC.Show.Show (Control.Unification.Types.UFailure t v)
instance GHC.Base.Functor t => GHC.Base.Functor (Control.Unification.Types.UFailure t)
instance Data.Foldable.Foldable t => Data.Foldable.Foldable (Control.Unification.Types.UFailure t)
instance Data.Traversable.Traversable t => Data.Traversable.Traversable (Control.Unification.Types.UFailure t)
instance (GHC.Show.Show v, GHC.Show.Show (t (Control.Unification.Types.UTerm t v))) => GHC.Show.Show (Control.Unification.Types.Rank t v)


-- | This module defines an implementation of unification variables using
--   the <a>ST</a> monad.
module Control.Unification.STVar

-- | Unification variables implemented by <a>STRef</a>s. In addition to the
--   <tt>STRef</tt> for the term itself, we also track the variable's ID
--   (to support visited-sets).
data STVar s t

-- | A monad for handling <a>STVar</a> bindings.
data STBinding s a

-- | Run the <a>ST</a> ranked binding monad. N.B., because <a>STVar</a> are
--   rank-2 quantified, this guarantees that the return value has no such
--   references. However, in order to remove the references from terms,
--   you'll need to explicitly apply the bindings and ground the term.
runSTBinding :: (forall s. STBinding s a) -> a
instance GHC.Show.Show (Control.Unification.STVar.STVar s t)
instance GHC.Classes.Eq (Control.Unification.STVar.STVar s t)
instance Control.Unification.Types.Variable (Control.Unification.STVar.STVar s t)
instance GHC.Base.Functor (Control.Unification.STVar.STBinding s)
instance GHC.Base.Applicative (Control.Unification.STVar.STBinding s)
instance GHC.Base.Monad (Control.Unification.STVar.STBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.BindingMonad t (Control.Unification.STVar.STVar s t) (Control.Unification.STVar.STBinding s)


-- | A ranked variant of <a>Control.Unification.STVar</a>.
module Control.Unification.Ranked.STVar

-- | A ranked unification variable implemented by <a>STRef</a>s. In
--   addition to the <tt>STRef</tt> for the term itself, we also track the
--   variable's ID (to support visited-sets) and rank (to support weighted
--   path compression).
data STRVar s t

-- | A monad for handling <a>STRVar</a> bindings.
data STRBinding s a

-- | Run the <a>ST</a> ranked binding monad. N.B., because <a>STRVar</a>
--   are rank-2 quantified, this guarantees that the return value has no
--   such references. However, in order to remove the references from
--   terms, you'll need to explicitly apply the bindings.
runSTRBinding :: (forall s. STRBinding s a) -> a
instance GHC.Show.Show (Control.Unification.Ranked.STVar.STRVar s t)
instance GHC.Classes.Eq (Control.Unification.Ranked.STVar.STRVar s t)
instance Control.Unification.Types.Variable (Control.Unification.Ranked.STVar.STRVar s t)
instance GHC.Base.Functor (Control.Unification.Ranked.STVar.STRBinding s)
instance GHC.Base.Applicative (Control.Unification.Ranked.STVar.STRBinding s)
instance GHC.Base.Monad (Control.Unification.Ranked.STVar.STRBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.BindingMonad t (Control.Unification.Ranked.STVar.STRVar s t) (Control.Unification.Ranked.STVar.STRBinding s)
instance Control.Unification.Types.Unifiable t => Control.Unification.Types.RankedBindingMonad t (Control.Unification.Ranked.STVar.STRVar s t) (Control.Unification.Ranked.STVar.STRBinding s)


-- | This module defines a state monad for functional pointers represented
--   by integers as keys into an <tt>IntMap</tt>. This technique was
--   independently discovered by Dijkstra et al. This module extends the
--   approach by using a state monad transformer, which can be made into a
--   backtracking state monad by setting the underlying monad to some
--   <a>MonadLogic</a> (part of the <tt>logict</tt> library, described by
--   Kiselyov et al.).
--   
--   <ul>
--   <li>Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)
--   <i>Efficient Functional Unification and Substitution</i>, Technical
--   Report UU-CS-2008-027, Utrecht University.</li>
--   <li>Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry
--   (2005) <i>Backtracking, Interleaving, and</i> <i>Terminating Monad
--   Transformers</i>, ICFP.</li>
--   </ul>
module Control.Unification.IntVar

-- | A "mutable" unification variable implemented by an integer. This
--   provides an entirely pure alternative to truly mutable alternatives
--   (like <tt>STVar</tt>), which can make backtracking easier.
--   
--   N.B., because this implementation is pure, we can use it for both
--   ranked and unranked monads.
newtype IntVar
IntVar :: Int -> IntVar

-- | Binding state for <a>IntVar</a>.
data IntBindingState t

-- | A monad for storing <a>IntVar</a> bindings, implemented as a
--   <a>StateT</a>. For a plain state monad, set <tt>m = Identity</tt>; for
--   a backtracking state monad, set <tt>m = Logic</tt>.
data IntBindingT t m a
runIntBindingT :: IntBindingT t m a -> m (a, IntBindingState t)

-- | N.B., you should explicitly apply bindings before calling this
--   function, or else the bindings will be lost
evalIntBindingT :: (Monad m) => IntBindingT t m a -> m a
execIntBindingT :: (Monad m) => IntBindingT t m a -> m (IntBindingState t)
instance GHC.Classes.Eq Control.Unification.IntVar.IntVar
instance GHC.Show.Show Control.Unification.IntVar.IntVar
instance Control.Unification.Types.Variable Control.Unification.IntVar.IntVar
instance GHC.Show.Show (t (Control.Unification.Types.UTerm t Control.Unification.IntVar.IntVar)) => GHC.Show.Show (Control.Unification.IntVar.IntBindingState t)
instance GHC.Base.Functor m => GHC.Base.Functor (Control.Unification.IntVar.IntBindingT t m)
instance (GHC.Base.Functor m, GHC.Base.Monad m) => GHC.Base.Applicative (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.Monad m => GHC.Base.Monad (Control.Unification.IntVar.IntBindingT t m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Unification.IntVar.IntBindingT t)
instance (GHC.Base.Functor m, GHC.Base.MonadPlus m) => GHC.Base.Alternative (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Control.Unification.IntVar.IntBindingT t m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState (Control.Unification.IntVar.IntBindingState t) (Control.Unification.IntVar.IntBindingT t m)
instance Control.Monad.Logic.Class.MonadLogic m => Control.Monad.Logic.Class.MonadLogic (Control.Unification.IntVar.IntBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.BindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.IntVar.IntBindingT t m)


-- | A ranked variant of <a>Control.Unification.IntVar</a>.
module Control.Unification.Ranked.IntVar

-- | A "mutable" unification variable implemented by an integer. This
--   provides an entirely pure alternative to truly mutable alternatives
--   (like <tt>STVar</tt>), which can make backtracking easier.
--   
--   N.B., because this implementation is pure, we can use it for both
--   ranked and unranked monads.
newtype IntVar
IntVar :: Int -> IntVar

-- | Ranked binding state for <a>IntVar</a>.
data IntRBindingState t

-- | A monad for storing <a>IntVar</a> bindings, implemented as a
--   <a>StateT</a>. For a plain state monad, set <tt>m = Identity</tt>; for
--   a backtracking state monad, set <tt>m = Logic</tt>.
data IntRBindingT t m a
runIntRBindingT :: IntRBindingT t m a -> m (a, IntRBindingState t)

-- | N.B., you should explicitly apply bindings before calling this
--   function, or else the bindings will be lost
evalIntRBindingT :: (Monad m) => IntRBindingT t m a -> m a
execIntRBindingT :: (Monad m) => IntRBindingT t m a -> m (IntRBindingState t)
instance GHC.Show.Show (t (Control.Unification.Types.UTerm t Control.Unification.IntVar.IntVar)) => GHC.Show.Show (Control.Unification.Ranked.IntVar.IntRBindingState t)
instance GHC.Base.Functor m => GHC.Base.Functor (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (GHC.Base.Functor m, GHC.Base.Monad m) => GHC.Base.Applicative (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.Monad m => GHC.Base.Monad (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Unification.Ranked.IntVar.IntRBindingT t)
instance (GHC.Base.Functor m, GHC.Base.MonadPlus m) => GHC.Base.Alternative (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.MonadPlus m => GHC.Base.MonadPlus (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance GHC.Base.Monad m => Control.Monad.State.Class.MonadState (Control.Unification.Ranked.IntVar.IntRBindingState t) (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance Control.Monad.Logic.Class.MonadLogic m => Control.Monad.Logic.Class.MonadLogic (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.BindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.Ranked.IntVar.IntRBindingT t m)
instance (Control.Unification.Types.Unifiable t, GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Unification.Types.RankedBindingMonad t Control.Unification.IntVar.IntVar (Control.Unification.Ranked.IntVar.IntRBindingT t m)


-- | This module defines some extra functions for
--   <a>Control.Monad.State.Lazy</a>. This package really isn't the proper
--   place for these, but we need them to be somewhere.
--   
--   TODO: patch transformers/mtl-2 with these functions.
module Control.Monad.State.UnificationExtras

-- | Lift a reader into a state monad. More particularly, this allows
--   disabling mutability in a local context within <tt>State</tt>.
liftReader :: Reader e a -> State e a

-- | Lift a reader into a state monad. More particularly, this allows
--   disabling mutability in a local context within <tt>StateT</tt>.
liftReaderT :: (Monad m) => ReaderT e m a -> StateT e m a

-- | A strict version of <tt>modify</tt>.
modify' :: (MonadState s m) => (s -> s) -> m ()

-- | Run a state action and undo the state changes at the end.
localState :: (MonadState s m) => m a -> m a


-- | A continuation-passing variant of <a>Maybe</a> for short-circuiting at
--   failure. This is based largely on code from the Haskell Wiki
--   (<a>http://www.haskell.org/haskellwiki/Performance/Monads</a>) which
--   was released under a simple permissive license
--   (<a>http://www.haskell.org/haskellwiki/HaskellWiki:Copyrights</a>).
--   However, various changes and extensions have been made, which are
--   subject to the BSD license of this package.
module Control.Monad.MaybeK

-- | A continuation-passing encoding of <a>Maybe</a>; also known as
--   <tt>Codensity Maybe</tt>, if you're familiar with that terminology.
--   N.B., this is not the 2-continuation implementation based on the
--   Church encoding of <tt>Maybe</tt>. The latter tends to have worse
--   performance than non-continuation based implementations.
--   
--   This is generally more efficient than using <tt>Maybe</tt> for two
--   reasons. First is that it right associates all binds, ensuring that
--   bad associativity doesn't artificially introduce midpoints in
--   short-circuiting to the nearest handler. Second is that it removes the
--   need for intermediate case expressions.
--   
--   N.B., the <a>Alternative</a> and <a>MonadPlus</a> instances are
--   left-biased in <tt>a</tt>. Thus, they are not commutative.
data MaybeK a

-- | Execute the <tt>MaybeK</tt> and return the concrete <tt>Maybe</tt>
--   encoding.
runMaybeK :: MaybeK a -> Maybe a

-- | Lift a <tt>Maybe</tt> into <tt>MaybeK</tt>.
toMaybeK :: Maybe a -> MaybeK a

-- | A version of <a>maybe</a> for convenience. This is almost identical to
--   <a>mplus</a> but allows applying a continuation to <tt>Just</tt>
--   values as well as handling <tt>Nothing</tt> errors. If you only want
--   to handle the errors, use <a>mplus</a> instead.
maybeK :: b -> (a -> b) -> MaybeK a -> b

-- | A monad transformer version of <a>MaybeK</a>.
data MaybeKT m a

-- | Execute a <tt>MaybeKT</tt> and return the concrete <tt>Maybe</tt>
--   encoding.
runMaybeKT :: (Applicative m) => MaybeKT m a -> m (Maybe a)

-- | Lift a <tt>Maybe</tt> into an <tt>MaybeKT</tt>.
toMaybeKT :: (Applicative m) => Maybe a -> MaybeKT m a

-- | Lift an <tt>MaybeK</tt> into an <tt>MaybeKT</tt>.
liftMaybeK :: (Applicative m) => MaybeK a -> MaybeKT m a

-- | Lower an <tt>MaybeKT</tt> into an <tt>MaybeK</tt>.
lowerMaybeK :: (Applicative m) => MaybeKT m a -> m (MaybeK a)
instance GHC.Base.Functor Control.Monad.MaybeK.MaybeK
instance GHC.Base.Applicative Control.Monad.MaybeK.MaybeK
instance GHC.Base.Monad Control.Monad.MaybeK.MaybeK
instance GHC.Base.Alternative Control.Monad.MaybeK.MaybeK
instance GHC.Base.MonadPlus Control.Monad.MaybeK.MaybeK
instance Control.Monad.Error.Class.MonadError () Control.Monad.MaybeK.MaybeK
instance GHC.Base.Functor (Control.Monad.MaybeK.MaybeKT m)
instance GHC.Base.Applicative (Control.Monad.MaybeK.MaybeKT m)
instance GHC.Base.Monad (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => GHC.Base.Alternative (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => GHC.Base.MonadPlus (Control.Monad.MaybeK.MaybeKT m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Monad.Error.Class.MonadError () (Control.Monad.MaybeK.MaybeKT m)
instance Control.Monad.Trans.Class.MonadTrans Control.Monad.MaybeK.MaybeKT


-- | This module provides first-order structural unification over general
--   structure types. It also provides the standard suite of functions
--   accompanying unification (applying bindings, getting free variables,
--   etc.).
--   
--   The implementation makes use of numerous optimization techniques.
--   First, we use path compression everywhere (for weighted path
--   compression see <a>Control.Unification.Ranked</a>). Second, we replace
--   the occurs-check with visited-sets. Third, we use a technique for
--   aggressive opportunistic observable sharing; that is, we track as much
--   sharing as possible in the bindings (without introducing new
--   variables), so that we can compare bound variables directly and
--   therefore eliminate redundant unifications.
module Control.Unification

-- | The type of terms generated by structures <tt>t</tt> over variables
--   <tt>v</tt>. The structure type should implement <a>Unifiable</a> and
--   the variable type should implement <a>Variable</a>.
--   
--   The <a>Show</a> instance doesn't show the constructors, in order to
--   improve legibility for large terms.
--   
--   All the category theoretic instances (<a>Functor</a>, <a>Foldable</a>,
--   <a>Traversable</a>,...) 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.
data UTerm t v

-- | A unification variable.
UVar :: !v -> UTerm t v

-- | Some structure containing subterms.
UTerm :: !(t (UTerm t v)) -> UTerm t v

-- | <i>O(n)</i>. Extract a pure term from a mutable term, or return
--   <tt>Nothing</tt> if the mutable term actually contains variables.
--   N.B., this function is pure, so you should manually apply bindings
--   before calling it.
freeze :: (Traversable t) => UTerm t v -> Maybe (Fix t)

-- | <i>O(n)</i>. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> UTerm t v

-- | 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.
--   
--   This is a finally-tagless encoding of the <a>UFailure</a> data type so
--   that we can abstract over clients adding additional domain-specific
--   failure modes, introducing monoid instances, etc.
--   
--   <i>Since: 0.10.0</i>
class Fallible t v a

-- | 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 <tt>a = Foo a</tt>" error.
--   
--   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.
occursFailure :: Fallible t v a => v -> UTerm t v -> a

-- | The top-most level of the terms do not match (according to
--   <a>zipMatch</a>). In logic programming this should simply be treated
--   as unification failure; in type checking this should result in a
--   "could not match expected type <tt>Foo</tt> with inferred type
--   <tt>Bar</tt>" error.
mismatchFailure :: Fallible t v a => t (UTerm t v) -> t (UTerm t v) -> a

-- | An implementation of syntactically unifiable structure. The
--   <tt>Traversable</tt> constraint is there because we also require terms
--   to be functors and require the distributivity of <a>sequence</a> or
--   <a>mapM</a>.
class (Traversable t) => Unifiable t

-- | Perform one level of equality testing for terms. If the term
--   constructors are unequal then return <tt>Nothing</tt>; if they are
--   equal, then return the one-level spine filled with resolved subterms
--   and/or pairs of subterms to be recursively checked.
zipMatch :: Unifiable t => t a -> t a -> Maybe (t (Either a (a, a)))

-- | An implementation of unification variables. The <a>Eq</a> requirement
--   is to determine whether two variables are equal <i>as variables</i>,
--   without considering what they are bound to. We use <a>Eq</a> rather
--   than having our own <tt>eqVar</tt> method so that clients can make use
--   of library functions which commonly assume <a>Eq</a>.
class (Eq v) => Variable v

-- | 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 <a>Eq</a>
--   instance:
--   
--   <tt>x == y</tt> if and only if <tt>getVarID x == getVarID y</tt>
getVarID :: Variable v => v -> Int

-- | 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 <tt>BindingMonad</tt>.
class (Unifiable t, Variable v, Applicative m, Monad m) => BindingMonad t v m | m t -> v, v m -> t where newVar t = do { v <- freeVar; bindVar v t; return v }

-- | Given a variable pointing to <tt>UTerm t v</tt>, return the term it's
--   bound to, or <tt>Nothing</tt> if the variable is unbound.
lookupVar :: BindingMonad t v m => v -> m (Maybe (UTerm t v))

-- | Generate a new free variable guaranteed to be fresh in <tt>m</tt>.
freeVar :: BindingMonad t v m => m v

-- | Generate a new variable (fresh in <tt>m</tt>) bound to the given term.
--   The default implementation is:
--   
--   <pre>
--   newVar t = do { v &lt;- freeVar ; bindVar v t ; return v }
--   </pre>
newVar :: BindingMonad t v m => UTerm t v -> m v

-- | Bind a variable to a term, overriding any previous binding.
bindVar :: BindingMonad t v m => v -> UTerm t v -> m ()

-- | Walk a term and determine which variables are still free. N.B., this
--   function does not detect cyclic terms (i.e., throw errors), but it
--   will return the correct answer for them in finite time.
getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]

-- | Apply the current bindings from the monad so that any remaining
--   variables in the result must, therefore, be free. N.B., this
--   expensively clones term structure and should only be performed when a
--   pure term is needed, or when <a>occursFailure</a> exceptions must be
--   forced. This function <i>does</i> preserve sharing, however that
--   sharing is no longer observed by the monad.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
applyBindings :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | Freshen all variables in a term, both bound and free. This ensures
--   that the observability of sharing is maintained, while freshening the
--   free variables. N.B., this expensively clones term structure and
--   should only be performed when necessary.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
freshen :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | <a>equals</a>
(===) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 ===

-- | <a>equiv</a>
(=~=) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 =~=

-- | <a>unify</a>
(=:=) :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 =:=

-- | <a>subsumes</a>
(<:=) :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m Bool
infix 4 <:=

-- | Determine if two terms are structurally equal. This is essentially
--   equivalent to <tt>(<a>==</a>)</tt> except that it does not require
--   applying bindings before comparing, so it is more efficient. N.B.,
--   this function does not consider alpha-variance, and thus variables
--   with different names are considered unequal. Cf., <a>equiv</a>.
equals :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 `equals`

-- | Determine if two terms are structurally equivalent; that is,
--   structurally equal modulo renaming of free variables. Returns a
--   mapping from variable IDs of the left term to variable IDs of the
--   right term, indicating the renaming used.
equiv :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 `equiv`

-- | Unify two terms, or throw an error with an explanation of why
--   unification failed. Since bindings are stored in the monad, the two
--   input terms and the output term are all equivalent if unification
--   succeeds. However, the returned value makes use of aggressive
--   opportunistic observable sharing, so it will be more efficient to use
--   it in future calculations than either argument.
unify :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 `unify`

-- | A variant of <a>unify</a> which uses <a>occursIn</a> instead of
--   visited-sets. This should only be used when eager throwing of
--   <a>occursFailure</a> errors is absolutely essential (or for testing
--   the correctness of <tt>unify</tt>). Performing the occurs-check is
--   expensive. Not only is it slow, it's asymptotically slow since it can
--   cause the same subterm to be traversed multiple times.
unifyOccurs :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)

-- | Determine whether the left term subsumes the right term. That is,
--   whereas <tt>(tl =:= tr)</tt> will compute the most general
--   substitution <tt>s</tt> such that <tt>(s tl === s tr)</tt>, <tt>(tl
--   &lt;:= tr)</tt> computes the most general substitution <tt>s</tt> such
--   that <tt>(s tl === tr)</tt>. This means that <tt>tl</tt> is less
--   defined than and consistent with <tt>tr</tt>.
--   
--   <i>N.B.</i>, this function updates the monadic bindings just like
--   <a>unify</a> does. However, while the use cases for unification often
--   want to keep the bindings around, the use cases for subsumption
--   usually do not. Thus, you'll probably want to use a binding monad
--   which supports backtracking in order to undo the changes.
--   Unfortunately, leaving the monadic bindings unaltered and returning
--   the necessary substitution directly imposes a performance penalty or
--   else requires specifying too much about the implementation of
--   variables.
subsumes :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m Bool
infix 4 `subsumes`

-- | Same as <a>getFreeVars</a>, but works on several terms simultaneously.
--   This is more efficient than getting the free variables for each of the
--   terms separately because we can make use of sharing across the whole
--   collection. That is, each time we move to the next term, we still
--   remember the bound variables we've already looked at (and therefore do
--   not need to traverse, since we've already seen whatever free variables
--   there are down there); whereas we would forget between each call to
--   <tt>getFreeVars</tt>.
--   
--   <i>Since: 0.7.0</i>
getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]

-- | Same as <a>applyBindings</a>, but works on several terms
--   simultaneously. This function preserves sharing across the entire
--   collection of terms, whereas applying the bindings to each term
--   separately would only preserve sharing within each term.
--   
--   <i>Since: 0.7.0</i>
applyBindingsAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Same as <a>freshen</a>, but works on several terms simultaneously.
--   This is different from freshening each term separately, because
--   <tt>freshenAll</tt> preserves the relationship between the terms. For
--   instance, the result of
--   
--   <pre>
--   mapM freshen [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 3]</tt> or something alpha-equivalent,
--   whereas the result of
--   
--   <pre>
--   freshenAll [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 2]</tt> or something alpha-equivalent.
--   
--   <i>Since: 0.7.0</i>
freshenAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Canonicalize a chain of variables so they all point directly to the
--   term at the end of the chain (or the free variable, if the chain is
--   unbound), and return that end.
--   
--   N.B., this is almost never the function you want. Cf.,
--   <a>semiprune</a>.
fullprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)

-- | Canonicalize a chain of variables so they all point directly to the
--   last variable in the chain, regardless of whether it is bound or not.
--   This allows detecting many cases where multiple variables point to the
--   same term, thereby allowing us to avoid re-unifying the term they
--   point to.
semiprune :: (BindingMonad t v m) => UTerm t v -> m (UTerm t v)

-- | Determine if a variable appears free somewhere inside a term. Since
--   occurs checks only make sense when we're about to bind the variable to
--   the term, we do not bother checking for the possibility of the
--   variable occuring bound in the term.
occursIn :: (BindingMonad t v m) => v -> UTerm t v -> m Bool


-- | This module provides the API of <a>Control.Unification</a> except
--   using <a>RankedBindingMonad</a> where appropriate. This module (and
--   the binding implementations for it) are highly experimental and
--   subject to change in future versions.
module Control.Unification.Ranked

-- | Walk a term and determine which variables are still free. N.B., this
--   function does not detect cyclic terms (i.e., throw errors), but it
--   will return the correct answer for them in finite time.
getFreeVars :: (BindingMonad t v m) => UTerm t v -> m [v]

-- | Apply the current bindings from the monad so that any remaining
--   variables in the result must, therefore, be free. N.B., this
--   expensively clones term structure and should only be performed when a
--   pure term is needed, or when <a>occursFailure</a> exceptions must be
--   forced. This function <i>does</i> preserve sharing, however that
--   sharing is no longer observed by the monad.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
applyBindings :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | Freshen all variables in a term, both bound and free. This ensures
--   that the observability of sharing is maintained, while freshening the
--   free variables. N.B., this expensively clones term structure and
--   should only be performed when necessary.
--   
--   If any cyclic bindings are detected, then an <a>occursFailure</a>
--   exception will be thrown.
freshen :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> em m (UTerm t v)

-- | <a>equals</a>
(===) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 ===

-- | <a>equiv</a>
(=~=) :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 =~=

-- | <a>unify</a>
(=:=) :: (RankedBindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 =:=

-- | Determine if two terms are structurally equal. This is essentially
--   equivalent to <tt>(<a>==</a>)</tt> except that it does not require
--   applying bindings before comparing, so it is more efficient. N.B.,
--   this function does not consider alpha-variance, and thus variables
--   with different names are considered unequal. Cf., <a>equiv</a>.
equals :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m Bool
infix 4 `equals`

-- | Determine if two terms are structurally equivalent; that is,
--   structurally equal modulo renaming of free variables. Returns a
--   mapping from variable IDs of the left term to variable IDs of the
--   right term, indicating the renaming used.
equiv :: (BindingMonad t v m) => UTerm t v -> UTerm t v -> m (Maybe (IntMap Int))
infix 4 `equiv`

-- | Unify two terms, or throw an error with an explanation of why
--   unification failed. Since bindings are stored in the monad, the two
--   input terms and the output term are all equivalent if unification
--   succeeds. However, the returned value makes use of aggressive
--   opportunistic observable sharing, so it will be more efficient to use
--   it in future calculations than either argument.
unify :: (RankedBindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m)) => UTerm t v -> UTerm t v -> em m (UTerm t v)
infix 4 `unify`

-- | Same as <a>getFreeVars</a>, but works on several terms simultaneously.
--   This is more efficient than getting the free variables for each of the
--   terms separately because we can make use of sharing across the whole
--   collection. That is, each time we move to the next term, we still
--   remember the bound variables we've already looked at (and therefore do
--   not need to traverse, since we've already seen whatever free variables
--   there are down there); whereas we would forget between each call to
--   <tt>getFreeVars</tt>.
--   
--   <i>Since: 0.7.0</i>
getFreeVarsAll :: (BindingMonad t v m, Foldable s) => s (UTerm t v) -> m [v]

-- | Same as <a>applyBindings</a>, but works on several terms
--   simultaneously. This function preserves sharing across the entire
--   collection of terms, whereas applying the bindings to each term
--   separately would only preserve sharing within each term.
--   
--   <i>Since: 0.7.0</i>
applyBindingsAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))

-- | Same as <a>freshen</a>, but works on several terms simultaneously.
--   This is different from freshening each term separately, because
--   <tt>freshenAll</tt> preserves the relationship between the terms. For
--   instance, the result of
--   
--   <pre>
--   mapM freshen [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 3]</tt> or something alpha-equivalent,
--   whereas the result of
--   
--   <pre>
--   freshenAll [UVar 1, UVar 1]
--   </pre>
--   
--   would be <tt>[UVar 2, UVar 2]</tt> or something alpha-equivalent.
--   
--   <i>Since: 0.7.0</i>
freshenAll :: (BindingMonad t v m, Fallible t v e, MonadTrans em, Functor (em m), MonadError e (em m), Traversable s) => s (UTerm t v) -> em m (s (UTerm t v))


-- | A continuation-passing variant of <a>Either</a> for short-circuiting
--   at failure. This code is based on <a>Control.Monad.MaybeK</a>.
module Control.Monad.EitherK

-- | A continuation-passing encoding of <a>Either</a> as an error monad;
--   also known as <tt>Codensity (Either e)</tt>, if you're familiar with
--   that terminology. N.B., this is not the 2-continuation implementation
--   based on the Church encoding of <tt>Either</tt>. The latter tends to
--   have worse performance than non-continuation based implementations.
--   
--   This is generally more efficient than using <tt>Either</tt> (or the
--   MTL's <tt>Error</tt>) for two reasons. First is that it right
--   associates all binds, ensuring that bad associativity doesn't
--   artificially introduce midpoints in short-circuiting to the nearest
--   handler. Second is that it removes the need for intermediate case
--   expressions.
--   
--   Another benefit over MTL's <tt>Error</tt> is that it doesn't
--   artificially restrict the error type. In fact, there's no reason why
--   <tt>e</tt> must denote "errors" per se. This could also denote
--   computations which short-circuit with the final answer, or similar
--   methods of non-local control flow.
--   
--   N.B., the <a>Alternative</a> and <a>MonadPlus</a> instances are
--   left-biased in <tt>a</tt> and monoidal in <tt>e</tt>. Thus, they are
--   not commutative.
data EitherK e a

-- | Execute an <tt>EitherK</tt> and return the concrete <tt>Either</tt>
--   encoding.
runEitherK :: EitherK e a -> Either e a

-- | Lift an <tt>Either</tt> into an <tt>EitherK</tt>.
toEitherK :: Either e a -> EitherK e a

-- | A version of <a>either</a> on <tt>EitherK</tt>, for convenience. N.B.,
--   using this function inserts a case match, reducing the range of
--   short-circuiting.
eitherK :: (e -> b) -> (a -> b) -> EitherK e a -> b

-- | Throw an error in the <tt>EitherK</tt> monad. This is identical to
--   <a>throwError</a>.
throwEitherK :: e -> EitherK e a

-- | Handle errors in the <tt>EitherK</tt> monad. N.B., this type is more
--   general than that of <a>catchError</a>, allowing the type of the
--   errors to change.
catchEitherK :: EitherK e a -> (e -> EitherK f a) -> EitherK f a

-- | A monad transformer version of <a>EitherK</a>.
data EitherKT e m a

-- | Execute an <tt>EitherKT</tt> and return the concrete <tt>Either</tt>
--   encoding.
runEitherKT :: (Applicative m) => EitherKT e m a -> m (Either e a)

-- | Lift an <tt>Either</tt> into an <tt>EitherKT</tt>.
toEitherKT :: (Applicative m) => Either e a -> EitherKT e m a

-- | Lift an <tt>EitherK</tt> into an <tt>EitherKT</tt>.
liftEitherK :: (Applicative m) => EitherK e a -> EitherKT e m a

-- | Lower an <tt>EitherKT</tt> into an <tt>EitherK</tt>.
lowerEitherK :: (Applicative m) => EitherKT e m a -> m (EitherK e a)

-- | Throw an error in the <tt>EitherKT</tt> monad. This is identical to
--   <a>throwError</a>.
throwEitherKT :: (Applicative m) => e -> EitherKT e m a

-- | Handle errors in the <tt>EitherKT</tt> monad. N.B., this type is more
--   general than that of <a>catchError</a>, allowing the type of the
--   errors to change.
catchEitherKT :: (Applicative m, Monad m) => EitherKT e m a -> (e -> EitherKT f m a) -> EitherKT f m a
instance GHC.Base.Functor (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Applicative (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monad (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monoid e => GHC.Base.Alternative (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Monoid e => GHC.Base.MonadPlus (Control.Monad.EitherK.EitherK e)
instance Control.Monad.Error.Class.MonadError e (Control.Monad.EitherK.EitherK e)
instance GHC.Base.Functor (Control.Monad.EitherK.EitherKT e m)
instance GHC.Base.Applicative (Control.Monad.EitherK.EitherKT e m)
instance GHC.Base.Monad (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m, GHC.Base.Monoid e) => GHC.Base.Alternative (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m, GHC.Base.Monoid e) => GHC.Base.MonadPlus (Control.Monad.EitherK.EitherKT e m)
instance (GHC.Base.Applicative m, GHC.Base.Monad m) => Control.Monad.Error.Class.MonadError e (Control.Monad.EitherK.EitherKT e m)
instance Control.Monad.Trans.Class.MonadTrans (Control.Monad.EitherK.EitherKT e)
