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


-- | Making de Bruijn Succ Less
--   
--   We represent the target language itself as an ideal monad supplied by
--   the user, and provide a <a>Scope</a> monad transformer for introducing
--   bound variables in user supplied terms. Users supply a <a>Monad</a>
--   and <a>Traversable</a> instance, and we traverse to find free
--   variables, and use the Monad to perform substitution that avoids bound
--   variables.
--   
--   Slides describing and motivating this approach to name binding are
--   available online at:
--   
--   
--   <a>http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less</a>
--   
--   The goal of this package is to make it as easy as possible to deal
--   with name binding without forcing an awkward monadic style on the
--   user.
--   
--   With generalized de Bruijn term you can <a>lift</a> whole trees
--   instead of just applying <a>succ</a> to individual variables,
--   weakening the all variables bound by a scope and greatly speeding up
--   instantiation. By giving binders more structure we permit easy
--   simultaneous substitution and further speed up instantiation.
@package bound
@version 2.0.1


-- | This module provides the <a>Bound</a> class, for performing
--   substitution into things that are not necessarily full monad
--   transformers.
module Bound.Class

-- | Instances of <a>Bound</a> generate left modules over monads.
--   
--   This means they should satisfy the following laws:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> <a>return</a> ≡ m
--   m <a>&gt;&gt;&gt;=</a> (λ x → k x <a>&gt;&gt;=</a> h) ≡ (m <a>&gt;&gt;&gt;=</a> k) <a>&gt;&gt;&gt;=</a> h
--   </pre>
--   
--   This guarantees that a typical Monad instance for an expression type
--   where Bound instances appear will satisfy the Monad laws (see
--   doc/BoundLaws.hs).
--   
--   If instances of <a>Bound</a> are monad transformers, then <tt>m
--   <a>&gt;&gt;&gt;=</a> f ≡ m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a>
--   f</tt> implies the above laws, and is in fact the default definition.
--   
--   This is useful for types like expression lists, case alternatives,
--   schemas, etc. that may not be expressions in their own right, but
--   often contain expressions.
--   
--   <i>Note:</i> <a>Free</a> isn't "really" a monad transformer, even if
--   the kind matches. Therefore there isn't <tt><a>Bound</a>
--   <a>Free</a></tt> instance.
class Bound t

-- | Perform substitution
--   
--   If <tt>t</tt> is an instance of <tt>MonadTrans</tt> and you are
--   compiling on GHC &gt;= 7.4, then this gets the default definition:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> f = m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a> f
--   </pre>
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c

-- | Perform substitution
--   
--   If <tt>t</tt> is an instance of <tt>MonadTrans</tt> and you are
--   compiling on GHC &gt;= 7.4, then this gets the default definition:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> f = m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a> f
--   </pre>
(>>>=) :: (Bound t, MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c
infixl 1 >>>=

-- | A flipped version of (<a>&gt;&gt;&gt;=</a>).
--   
--   <pre>
--   (<a>=&lt;&lt;&lt;</a>) = <a>flip</a> (<a>&gt;&gt;&gt;=</a>)
--   </pre>
(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
infixr 1 =<<<
instance Bound.Class.Bound (Control.Monad.Trans.Cont.ContT c)
instance Control.Monad.Trans.Error.Error e => Bound.Class.Bound (Control.Monad.Trans.Error.ErrorT e)
instance Bound.Class.Bound Control.Monad.Trans.Identity.IdentityT
instance Bound.Class.Bound Control.Monad.Trans.List.ListT
instance Bound.Class.Bound Control.Monad.Trans.Maybe.MaybeT
instance GHC.Base.Monoid w => Bound.Class.Bound (Control.Monad.Trans.RWS.Lazy.RWST r w s)
instance Bound.Class.Bound (Control.Monad.Trans.Reader.ReaderT r)
instance Bound.Class.Bound (Control.Monad.Trans.State.Lazy.StateT s)
instance GHC.Base.Monoid w => Bound.Class.Bound (Control.Monad.Trans.Writer.Lazy.WriterT w)


-- | This is a Template Haskell module for deriving <a>Applicative</a> and
--   <a>Monad</a> instances for data types.
module Bound.TH

-- | Use to automatically derive <a>Applicative</a> and <a>Monad</a>
--   instances for your datatype.
--   
--   Also works for components that are lists or instances of
--   <a>Functor</a>, but still does not work for a great deal of other
--   things.
--   
--   <tt>deriving-compat</tt> package may be used to derive the
--   <tt>Show1</tt> and <tt>Read1</tt> instances
--   
--   <pre>
--   {-# LANGUAGE DeriveFunctor      #-}
--   {-# LANGUAGE TemplateHaskell    #-}
--   
--   import Bound                (Scope, makeBound)
--   import Data.Functor.Classes (Show1, Read1, shosPrec1, readsPrec1)
--   import Data.Deriving        (deriveShow1, deriveRead1)
--   
--   data Exp a
--     = V a
--     | App (Exp a) (Exp a)
--     | Lam (Scope () Exp a)
--     | ND [Exp a]
--     | I Int
--     deriving (Functor)
--   
--   makeBound ''Exp
--   deriveShow1 ''Exp
--   deriveRead1 ''Exp
--   instance Read a =&gt; Read (Exp a) where readsPrec = readsPrec1
--   instance Show a =&gt; Show (Exp a) where showsPrec = showsPrec1
--   </pre>
--   
--   and in GHCi
--   
--   <pre>
--   ghci&gt; :set -XDeriveFunctor
--   ghci&gt; :set -XTemplateHaskell
--   ghci&gt; import Bound                (Scope, makeBound)
--   ghci&gt; import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
--   ghci&gt; import Data.Deriving        (deriveShow1, deriveRead1)
--   ghci&gt; :{
--   ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)
--   ghci| makeBound ''Exp
--   ghci| deriveShow1 ''Exp
--   ghci| deriveRead1 ''Exp
--   ghci| instance Read a =&gt; Read (Exp a) where readsPrec = readsPrec1
--   ghci| instance Show a =&gt; Show (Exp a) where showsPrec = showsPrec1
--   ghci| :}
--   </pre>
--   
--   <a>Eq</a> and <a>Ord</a> instances can be derived similarly
--   
--   <pre>
--   import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   import Data.Deriving        (deriveEq1, deriveOrd1)
--   
--   deriveEq1 ''Exp
--   deriveOrd1 ''Exp
--   instance Eq a =&gt; Eq (Exp a) where (==) = eq1
--   instance Ord a =&gt; Ord (Exp a) where compare = compare1
--   </pre>
--   
--   or in GHCi:
--   
--   <pre>
--   ghci&gt; import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   ghci&gt; import Data.Deriving        (deriveEq1, deriveOrd1)
--   ghci&gt; :{
--   ghci| deriveEq1 ''Exp
--   ghci| deriveOrd1 ''Exp
--   ghci| instance Eq a =&gt; Eq (Exp a) where (==) = eq1
--   ghci| instance Ord a =&gt; Ord (Exp a) where compare = compare1
--   ghci| :}
--   </pre>
--   
--   We cannot automatically derive <a>Eq</a> and <a>Ord</a> using the
--   standard GHC mechanism, because instances require <tt>Exp</tt> to be a
--   <a>Monad</a>:
--   
--   <pre>
--   instance (Monad f, Eq b, Eq1 f, Eq a)    =&gt; Eq (Scope b f a)
--   instance (Monad f, Ord b, Ord1 f, Ord a) =&gt; Ord (Scope b f a)
--   </pre>
makeBound :: Name -> DecsQ
instance GHC.Show.Show Bound.TH.Components
instance GHC.Show.Show Bound.TH.Prop


module Bound.Term

-- | <tt><a>substitute</a> a p w</tt> replaces the free variable <tt>a</tt>
--   with <tt>p</tt> in <tt>w</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
--   ["goodnight","Gracie","!!!"]
--   </pre>
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a

-- | <tt><a>substituteVar</a> a b w</tt> replaces a free variable
--   <tt>a</tt> with another free variable <tt>b</tt> in <tt>w</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
--   ["Bob","Bob","Charlie"]
--   </pre>
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a

-- | A closed term has no free variables.
--   
--   <pre>
--   &gt;&gt;&gt; isClosed []
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isClosed [1,2,3]
--   False
--   </pre>
isClosed :: Foldable f => f a -> Bool

-- | If a term has no free variables, you can freely change the type of
--   free variables it is parameterized on.
--   
--   <pre>
--   &gt;&gt;&gt; closed [12]
--   Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; closed ""
--   Just []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :t closed ""
--   closed "" :: Maybe [b]
--   </pre>
closed :: Traversable f => f a -> Maybe (f b)


module Bound.Var

-- | "I am not a number, I am a <i>free monad</i>!"
--   
--   A <tt><a>Var</a> b a</tt> is a variable that may either be "bound"
--   (<a>B</a>) or "free" (<a>F</a>).
--   
--   (It is also technically a free monad in the same near-trivial sense as
--   <a>Either</a>.)
data Var b a

-- | this is a bound variable
B :: b -> Var b a

-- | this is a free variable
F :: a -> Var b a
unvar :: (b -> r) -> (a -> r) -> Var b a -> r

-- | This provides a <tt>Prism</tt> that can be used with <tt>lens</tt>
--   library to access a bound <a>Var</a>.
--   
--   <pre>
--   <a>_B</a> :: <tt>Prism</tt> (Var b a) (Var b' a) b b'@
--   </pre>
_B :: (Choice p, Applicative f) => p b (f b') -> p (Var b a) (f (Var b' a))

-- | This provides a <tt>Prism</tt> that can be used with <tt>lens</tt>
--   library to access a free <a>Var</a>.
--   
--   <pre>
--   <a>_F</a> :: <tt>Prism</tt> (Var b a) (Var b a') a a'@
--   </pre>
_F :: (Choice p, Applicative f) => p a (f a') -> p (Var b a) (f (Var b a'))
instance GHC.Generics.Generic1 (Bound.Var.Var b)
instance GHC.Generics.Generic (Bound.Var.Var b a)
instance (Data.Data.Data b, Data.Data.Data a) => Data.Data.Data (Bound.Var.Var b a)
instance (GHC.Read.Read b, GHC.Read.Read a) => GHC.Read.Read (Bound.Var.Var b a)
instance (GHC.Show.Show b, GHC.Show.Show a) => GHC.Show.Show (Bound.Var.Var b a)
instance (GHC.Classes.Ord b, GHC.Classes.Ord a) => GHC.Classes.Ord (Bound.Var.Var b a)
instance (GHC.Classes.Eq b, GHC.Classes.Eq a) => GHC.Classes.Eq (Bound.Var.Var b a)
instance Data.Hashable.Class.Hashable2 Bound.Var.Var
instance Data.Hashable.Class.Hashable b => Data.Hashable.Class.Hashable1 (Bound.Var.Var b)
instance (Data.Hashable.Class.Hashable b, Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Bound.Var.Var b a)
instance Data.Bytes.Serial.Serial2 Bound.Var.Var
instance Data.Bytes.Serial.Serial b => Data.Bytes.Serial.Serial1 (Bound.Var.Var b)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial a) => Data.Bytes.Serial.Serial (Bound.Var.Var b a)
instance (Data.Binary.Class.Binary b, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Bound.Var.Var b a)
instance (Data.Serialize.Serialize b, Data.Serialize.Serialize a) => Data.Serialize.Serialize (Bound.Var.Var b a)
instance GHC.Base.Functor (Bound.Var.Var b)
instance Data.Foldable.Foldable (Bound.Var.Var b)
instance Data.Traversable.Traversable (Bound.Var.Var b)
instance GHC.Base.Applicative (Bound.Var.Var b)
instance GHC.Base.Monad (Bound.Var.Var b)
instance Data.Bifunctor.Bifunctor Bound.Var.Var
instance Data.Bifoldable.Bifoldable Bound.Var.Var
instance Data.Bitraversable.Bitraversable Bound.Var.Var
instance Data.Functor.Classes.Eq2 Bound.Var.Var
instance Data.Functor.Classes.Ord2 Bound.Var.Var
instance Data.Functor.Classes.Show2 Bound.Var.Var
instance Data.Functor.Classes.Read2 Bound.Var.Var
instance GHC.Classes.Eq b => Data.Functor.Classes.Eq1 (Bound.Var.Var b)
instance GHC.Classes.Ord b => Data.Functor.Classes.Ord1 (Bound.Var.Var b)
instance GHC.Show.Show b => Data.Functor.Classes.Show1 (Bound.Var.Var b)
instance GHC.Read.Read b => Data.Functor.Classes.Read1 (Bound.Var.Var b)
instance (Control.DeepSeq.NFData a, Control.DeepSeq.NFData b) => Control.DeepSeq.NFData (Bound.Var.Var b a)


-- | <a>Scope</a> provides a single traditional de Bruijn level and is
--   often used inside of the definition of binders.
module Bound.Scope.Simple

-- | <tt><a>Scope</a> b f a</tt> is an <tt>f</tt> expression with bound
--   variables in <tt>b</tt>, and free variables in <tt>a</tt>
--   
--   This implements traditional de Bruijn indices, while <a>Scope</a>
--   implements generalized de Bruijn indices.
--   
--   These traditional indices can be used to test the performance gain of
--   generalized indices.
--   
--   While this type <a>Scope</a> is identical to <a>EitherT</a> this
--   module focuses on a drop-in replacement for <a>Scope</a>.
--   
--   Another use case is for syntaxes not stable under substitution,
--   therefore with only a <a>Functor</a> instance and no <a>Monad</a>
--   instance.
newtype Scope b f a
Scope :: f (Var b a) -> Scope b f a
[unscope] :: Scope b f a -> f (Var b a)

-- | Capture some free variables in an expression to yield a <a>Scope</a>
--   with bound variables in <tt>b</tt>
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; abstract (`elemIndex` "bar") "barry"
--   Scope [B 0,B 1,B 2,B 2,F 'y']
--   </pre>
abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a

-- | Abstract over a single variable
--   
--   <pre>
--   &gt;&gt;&gt; abstract1 'x' "xyz"
--   Scope [B (),F 'y',F 'z']
--   </pre>
abstract1 :: (Functor f, Eq a) => a -> f a -> Scope () f a

-- | Enter a scope, instantiating all bound variables
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; instantiate (\x -&gt; [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
--   "abccy"
--   </pre>
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

-- | Enter a <a>Scope</a> that binds one variable, instantiating it
--   
--   <pre>
--   &gt;&gt;&gt; instantiate1 "x" $ Scope [B (),F 'y',F 'z']
--   "xyz"
--   </pre>
instantiate1 :: Monad f => f a -> Scope n f a -> f a

-- | <tt><a>fromScope</a></tt> is just another name for <a>unscope</a> and
--   is exported to mimick <a>fromScope</a>. In particular no <a>Monad</a>
--   constraint is required.
fromScope :: Scope b f a -> f (Var b a)

-- | <tt><a>toScope</a></tt> is just another name for <a>Scope</a> and is
--   exported to mimick <a>toScope</a>. In particular no <a>Monad</a>
--   constraint is required.
toScope :: f (Var b a) -> Scope b f a

-- | Perform substitution on both bound and free variables in a
--   <a>Scope</a>.
splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c

-- | Return a list of occurences of the variables bound by this
--   <a>Scope</a>.
bindings :: Foldable f => Scope b f a -> [b]

-- | Perform a change of variables on bound variables.
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a

-- | Perform a change of variables, reassigning both bound and free
--   variables.
mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c

-- | Perform a change of variables on bound variables given only a
--   <a>Monad</a> instance
liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a

-- | A version of <a>mapScope</a> that can be used when you only have the
--   <a>Monad</a> instance
liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c

-- | Obtain a result by collecting information from both bound and free
--   variables
foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r

-- | Obtain a result by collecting information from both bound and free
--   variables
foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> r

-- | <a>traverse_</a> the bound variables in a <a>Scope</a>.
traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()

-- | <a>traverse</a> both the variables bound by this scope and any free
--   variables.
traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()

-- | mapM_ over the variables bound by this scope
mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()

-- | A <a>traverseScope_</a> that can be used when you only have a
--   <a>Monad</a> instance
mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()

-- | Traverse both bound and free variables
traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)

-- | Traverse both bound and free variables
traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)

-- | mapM over both bound and free variables
mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)

-- | A <a>traverseScope</a> that can be used when you only have a
--   <a>Monad</a> instance
mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)
hoistScope :: (f (Var b a) -> g (Var b a)) -> Scope b f a -> Scope b g a

-- | This allows you to <a>bitraverse</a> a <a>Scope</a>.
bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> forall a a'. (a -> f a') -> Scope b t a -> f (Scope b u a')

-- | This is a higher-order analogue of <a>traverse</a>.
transverseScope :: Functor f => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a)

-- | instantiate bound variables using a list of new variables
instantiateVars :: Monad t => [a] -> Scope Int t a -> t a
instance GHC.Generics.Generic (Bound.Scope.Simple.Scope b f a)
instance GHC.Base.Functor f => GHC.Generics.Generic1 (Bound.Scope.Simple.Scope b f)
instance (Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable f, Data.Data.Data a, Data.Data.Data (f (Bound.Var.Var b a))) => Data.Data.Data (Bound.Scope.Simple.Scope b f a)
instance Control.DeepSeq.NFData (f (Bound.Var.Var b a)) => Control.DeepSeq.NFData (Bound.Scope.Simple.Scope b f a)
instance GHC.Base.Functor f => GHC.Base.Functor (Bound.Scope.Simple.Scope b f)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Bound.Scope.Simple.Scope b f)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Bound.Scope.Simple.Scope b f)
instance GHC.Base.Monad f => GHC.Base.Applicative (Bound.Scope.Simple.Scope b f)
instance GHC.Base.Monad f => GHC.Base.Monad (Bound.Scope.Simple.Scope b f)
instance Control.Monad.Trans.Class.MonadTrans (Bound.Scope.Simple.Scope b)
instance Control.Monad.Morph.MFunctor (Bound.Scope.Simple.Scope b)
instance (GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f) => Data.Functor.Classes.Eq1 (Bound.Scope.Simple.Scope b f)
instance (GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f) => Data.Functor.Classes.Ord1 (Bound.Scope.Simple.Scope b f)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f) => Data.Functor.Classes.Show1 (Bound.Scope.Simple.Scope b f)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f) => Data.Functor.Classes.Read1 (Bound.Scope.Simple.Scope b f)
instance (GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f, GHC.Classes.Eq a) => GHC.Classes.Eq (Bound.Scope.Simple.Scope b f a)
instance (GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f, GHC.Classes.Ord a) => GHC.Classes.Ord (Bound.Scope.Simple.Scope b f a)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f, GHC.Show.Show a) => GHC.Show.Show (Bound.Scope.Simple.Scope b f a)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f, GHC.Read.Read a) => GHC.Read.Read (Bound.Scope.Simple.Scope b f a)
instance Bound.Class.Bound (Bound.Scope.Simple.Scope b)
instance (Data.Hashable.Class.Hashable b, Data.Hashable.Class.Hashable1 f) => Data.Hashable.Class.Hashable1 (Bound.Scope.Simple.Scope b f)
instance (Data.Hashable.Class.Hashable b, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Bound.Scope.Simple.Scope b f a)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial1 f) => Data.Bytes.Serial.Serial1 (Bound.Scope.Simple.Scope b f)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial1 f, Data.Bytes.Serial.Serial a) => Data.Bytes.Serial.Serial (Bound.Scope.Simple.Scope b f a)
instance (Data.Binary.Class.Binary b, Data.Bytes.Serial.Serial1 f, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Bound.Scope.Simple.Scope b f a)
instance (Data.Serialize.Serialize b, Data.Bytes.Serial.Serial1 f, Data.Serialize.Serialize a) => Data.Serialize.Serialize (Bound.Scope.Simple.Scope b f a)


-- | This is the work-horse of the <tt>bound</tt> library.
--   
--   <a>Scope</a> provides a single generalized de Bruijn level and is
--   often used inside of the definition of binders.
module Bound.Scope

-- | <tt><a>Scope</a> b f a</tt> is an <tt>f</tt> expression with bound
--   variables in <tt>b</tt>, and free variables in <tt>a</tt>
--   
--   We store bound variables as their generalized de Bruijn representation
--   in that we're allowed to <a>lift</a> (using <a>F</a>) an entire tree
--   rather than only succ individual variables, but we're still only
--   allowed to do so once per <a>Scope</a>. Weakening trees permits
--   <i>O(1)</i> weakening and permits more sharing opportunities. Here the
--   deBruijn 0 is represented by the <a>B</a> constructor of <a>Var</a>,
--   while the de Bruijn <a>succ</a> (which may be applied to an entire
--   tree!) is handled by <a>F</a>.
--   
--   NB: equality and comparison quotient out the distinct <a>F</a>
--   placements allowed by the generalized de Bruijn representation and
--   return the same result as a traditional de Bruijn representation
--   would.
--   
--   Logically you can think of this as if the shape were the traditional
--   <tt>f (Var b a)</tt>, but the extra <tt>f a</tt> inside permits us a
--   cheaper <a>lift</a>.
newtype Scope b f a
Scope :: f (Var b (f a)) -> Scope b f a
[unscope] :: Scope b f a -> f (Var b (f a))

-- | Capture some free variables in an expression to yield a <a>Scope</a>
--   with bound variables in <tt>b</tt>
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; abstract (`elemIndex` "bar") "barry"
--   Scope [B 0,B 1,B 2,B 2,F "y"]
--   </pre>
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

-- | Abstract over a single variable
--   
--   <pre>
--   &gt;&gt;&gt; abstract1 'x' "xyz"
--   Scope [B (),F "y",F "z"]
--   </pre>
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a

-- | Capture some free variables in an expression to yield a <a>Scope</a>
--   with bound variables in <tt>b</tt>. Optionally change the types of the
--   remaining free variables.
abstractEither :: Monad f => (a -> Either b c) -> f a -> Scope b f c

-- | Enter a scope, instantiating all bound variables
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; instantiate (\x -&gt; [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
--   "abccy"
--   </pre>
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

-- | Enter a <a>Scope</a> that binds one variable, instantiating it
--   
--   <pre>
--   &gt;&gt;&gt; instantiate1 "x" $ Scope [B (),F "y",F "z"]
--   "xyz"
--   </pre>
instantiate1 :: Monad f => f a -> Scope n f a -> f a

-- | Enter a scope, and instantiate all bound and free variables in one go.
instantiateEither :: Monad f => (Either b a -> f c) -> Scope b f a -> f c

-- | <tt><a>fromScope</a></tt> quotients out the possible placements of
--   <a>F</a> in <a>Scope</a> by distributing them all to the leaves. This
--   yields a more traditional de Bruijn indexing scheme for bound
--   variables.
--   
--   Since,
--   
--   <pre>
--   <a>fromScope</a> <a>.</a> <a>toScope</a> ≡ <a>id</a>
--   </pre>
--   
--   we know that
--   
--   <pre>
--   <a>fromScope</a> <a>.</a> <a>toScope</a> <a>.</a> <a>fromScope</a> ≡ <a>fromScope</a>
--   </pre>
--   
--   and therefore <tt>(<a>toScope</a> . <a>fromScope</a>)</tt> is
--   idempotent.
fromScope :: Monad f => Scope b f a -> f (Var b a)

-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
--   
--   This requires a full tree traversal
toScope :: Monad f => f (Var b a) -> Scope b f a

-- | Perform substitution on both bound and free variables in a
--   <a>Scope</a>.
splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c

-- | Return a list of occurences of the variables bound by this
--   <a>Scope</a>.
bindings :: Foldable f => Scope b f a -> [b]

-- | Perform a change of variables on bound variables.
mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a

-- | Perform a change of variables, reassigning both bound and free
--   variables.
mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c

-- | Perform a change of variables on bound variables given only a
--   <a>Monad</a> instance
liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a

-- | A version of <a>mapScope</a> that can be used when you only have the
--   <a>Monad</a> instance
liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c

-- | Obtain a result by collecting information from bound variables
foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r

-- | Obtain a result by collecting information from both bound and free
--   variables
foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> r

-- | <a>traverse_</a> the bound variables in a <a>Scope</a>.
traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()

-- | <a>traverse</a> both the variables bound by this scope and any free
--   variables.
traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()

-- | mapM_ over the variables bound by this scope
mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()

-- | A <a>traverseScope_</a> that can be used when you only have a
--   <a>Monad</a> instance
mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()

-- | <a>traverse</a> the bound variables in a <a>Scope</a>.
traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)

-- | Traverse both bound and free variables
traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)

-- | mapM over both bound and free variables
mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)

-- | A <a>traverseScope</a> that can be used when you only have a
--   <a>Monad</a> instance
mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
serializeScope :: (Serial1 f, MonadPut m) => (b -> m ()) -> (v -> m ()) -> Scope b f v -> m ()
deserializeScope :: (Serial1 f, MonadGet m) => m b -> m v -> m (Scope b f v)

-- | Lift a natural transformation from <tt>f</tt> to <tt>g</tt> into one
--   between scopes.
hoistScope :: Functor f => (forall x. f x -> g x) -> Scope b f a -> Scope b g a

-- | This allows you to <a>bitraverse</a> a <a>Scope</a>.
bitraverseScope :: (Bitraversable t, Applicative f) => (k -> f k') -> (a -> f a') -> Scope b (t k) a -> f (Scope b (t k') a')
bitransverseScope :: Applicative f => (forall a a'. (a -> f a') -> t a -> f (u a')) -> (c -> f c') -> Scope b t c -> f (Scope b u c')

-- | This is a higher-order analogue of <a>traverse</a>.
transverseScope :: (Applicative f, Monad f, Traversable g) => (forall r. g r -> f (h r)) -> Scope b g a -> f (Scope b h a)

-- | instantiate bound variables using a list of new variables
instantiateVars :: Monad t => [a] -> Scope Int t a -> t a
instance GHC.Generics.Generic (Bound.Scope.Scope b f a)
instance GHC.Base.Functor f => GHC.Generics.Generic1 (Bound.Scope.Scope b f)
instance (Data.Typeable.Internal.Typeable b, Data.Typeable.Internal.Typeable f, Data.Data.Data a, Data.Data.Data (f (Bound.Var.Var b (f a)))) => Data.Data.Data (Bound.Scope.Scope b f a)
instance GHC.Base.Functor f => GHC.Base.Functor (Bound.Scope.Scope b f)
instance Data.Foldable.Foldable f => Data.Foldable.Foldable (Bound.Scope.Scope b f)
instance Data.Traversable.Traversable f => Data.Traversable.Traversable (Bound.Scope.Scope b f)
instance (GHC.Base.Functor f, GHC.Base.Monad f) => GHC.Base.Applicative (Bound.Scope.Scope b f)
instance GHC.Base.Monad f => GHC.Base.Monad (Bound.Scope.Scope b f)
instance Control.Monad.Trans.Class.MonadTrans (Bound.Scope.Scope b)
instance Control.Monad.Morph.MFunctor (Bound.Scope.Scope b)
instance (GHC.Base.Monad f, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f, GHC.Classes.Eq a) => GHC.Classes.Eq (Bound.Scope.Scope b f a)
instance (GHC.Base.Monad f, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f, GHC.Classes.Ord a) => GHC.Classes.Ord (Bound.Scope.Scope b f a)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f, GHC.Read.Read a) => GHC.Read.Read (Bound.Scope.Scope b f a)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f, GHC.Show.Show a) => GHC.Show.Show (Bound.Scope.Scope b f a)
instance (GHC.Base.Monad f, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f) => Data.Functor.Classes.Eq1 (Bound.Scope.Scope b f)
instance (GHC.Base.Monad f, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f) => Data.Functor.Classes.Ord1 (Bound.Scope.Scope b f)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f) => Data.Functor.Classes.Show1 (Bound.Scope.Scope b f)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f) => Data.Functor.Classes.Read1 (Bound.Scope.Scope b f)
instance Bound.Class.Bound (Bound.Scope.Scope b)
instance (Data.Hashable.Class.Hashable b, GHC.Base.Monad f, Data.Hashable.Class.Hashable1 f) => Data.Hashable.Class.Hashable1 (Bound.Scope.Scope b f)
instance (Data.Hashable.Class.Hashable b, GHC.Base.Monad f, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Bound.Scope.Scope b f a)
instance Control.DeepSeq.NFData (f (Bound.Var.Var b (f a))) => Control.DeepSeq.NFData (Bound.Scope.Scope b f a)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial1 f) => Data.Bytes.Serial.Serial1 (Bound.Scope.Scope b f)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial1 f, Data.Bytes.Serial.Serial a) => Data.Bytes.Serial.Serial (Bound.Scope.Scope b f a)
instance (Data.Binary.Class.Binary b, Data.Bytes.Serial.Serial1 f, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Bound.Scope.Scope b f a)
instance (Data.Serialize.Serialize b, Data.Bytes.Serial.Serial1 f, Data.Serialize.Serialize a) => Data.Serialize.Serialize (Bound.Scope.Scope b f a)


-- | The problem with locally nameless approaches is that original names
--   are often useful for error reporting, or to allow for the user in an
--   interactive theorem prover to convey some hint about the domain. A
--   <tt><a>Name</a> n b</tt> is a value <tt>b</tt> supplemented with a
--   (discardable) name that may be useful for error reporting purposes. In
--   particular, this name does not participate in comparisons for
--   equality.
--   
--   This module is <i>not</i> exported from <a>Bound</a> by default. You
--   need to explicitly import it, due to the fact that <a>Name</a> is a
--   pretty common term in other people's code.
module Bound.Name

-- | We track the choice of <a>Name</a> <tt>n</tt> as a forgettable
--   property that does <i>not</i> affect the result of (<a>==</a>) or
--   <a>compare</a>.
--   
--   To compare names rather than values, use <tt>(<a>on</a> <a>compare</a>
--   <a>name</a>)</tt> instead.
data Name n b
Name :: n -> b -> Name n b

-- | This provides an <tt>Iso</tt> that can be used to access the parts of
--   a <a>Name</a>.
--   
--   <pre>
--   <a>_Name</a> :: Iso (<a>Name</a> n a) (<a>Name</a> m b) (n, a) (m, b)
--   </pre>
_Name :: (Profunctor p, Functor f) => p (n, a) (f (m, b)) -> p (Name n a) (f (Name m b))

-- | Extract the <a>name</a>.
name :: Name n b -> n

-- | Abstraction, capturing named bound variables.
abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a

-- | Abstract over a single variable
abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a

-- | Capture some free variables in an expression to yield a <a>Scope</a>
--   with named bound variables. Optionally change the types of the
--   remaining free variables.
abstractEitherName :: Monad f => (a -> Either b c) -> f a -> Scope (Name a b) f c

-- | Enter a scope, instantiating all bound variables, but discarding
--   (comonadic) meta data, like its name
instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a

-- | Enter a <a>Scope</a> that binds one (named) variable, instantiating
--   it.
--   
--   <pre>
--   <a>instantiate1Name</a> = <a>instantiate1</a>
--   </pre>
instantiate1Name :: Monad f => f a -> Scope n f a -> f a
instantiateEitherName :: (Monad f, Comonad n) => (Either b a -> f c) -> Scope (n b) f a -> f c
instance GHC.Generics.Generic1 (Bound.Name.Name n)
instance GHC.Generics.Generic (Bound.Name.Name n b)
instance (Data.Data.Data n, Data.Data.Data b) => Data.Data.Data (Bound.Name.Name n b)
instance (GHC.Read.Read n, GHC.Read.Read b) => GHC.Read.Read (Bound.Name.Name n b)
instance (GHC.Show.Show n, GHC.Show.Show b) => GHC.Show.Show (Bound.Name.Name n b)
instance GHC.Classes.Eq b => GHC.Classes.Eq (Bound.Name.Name n b)
instance Data.Hashable.Class.Hashable2 Bound.Name.Name
instance Data.Hashable.Class.Hashable1 (Bound.Name.Name n)
instance Data.Hashable.Class.Hashable a => Data.Hashable.Class.Hashable (Bound.Name.Name n a)
instance GHC.Classes.Ord b => GHC.Classes.Ord (Bound.Name.Name n b)
instance GHC.Base.Functor (Bound.Name.Name n)
instance Data.Foldable.Foldable (Bound.Name.Name n)
instance Data.Traversable.Traversable (Bound.Name.Name n)
instance Data.Bifunctor.Bifunctor Bound.Name.Name
instance Data.Bifoldable.Bifoldable Bound.Name.Name
instance Data.Bitraversable.Bitraversable Bound.Name.Name
instance Control.Comonad.Comonad (Bound.Name.Name n)
instance Data.Functor.Classes.Eq2 Bound.Name.Name
instance Data.Functor.Classes.Ord2 Bound.Name.Name
instance Data.Functor.Classes.Show2 Bound.Name.Name
instance Data.Functor.Classes.Read2 Bound.Name.Name
instance Data.Functor.Classes.Eq1 (Bound.Name.Name b)
instance Data.Functor.Classes.Ord1 (Bound.Name.Name b)
instance GHC.Show.Show b => Data.Functor.Classes.Show1 (Bound.Name.Name b)
instance GHC.Read.Read b => Data.Functor.Classes.Read1 (Bound.Name.Name b)
instance Data.Bytes.Serial.Serial2 Bound.Name.Name
instance Data.Bytes.Serial.Serial b => Data.Bytes.Serial.Serial1 (Bound.Name.Name b)
instance (Data.Bytes.Serial.Serial b, Data.Bytes.Serial.Serial a) => Data.Bytes.Serial.Serial (Bound.Name.Name b a)
instance (Data.Binary.Class.Binary b, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Bound.Name.Name b a)
instance (Data.Serialize.Serialize b, Data.Serialize.Serialize a) => Data.Serialize.Serialize (Bound.Name.Name b a)
instance (Control.DeepSeq.NFData b, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Bound.Name.Name b a)


-- | We represent the target language itself as an ideal monad supplied by
--   the user, and provide a <a>Scope</a> monad transformer for introducing
--   bound variables in user supplied terms. Users supply a <a>Monad</a>
--   and <a>Traversable</a> instance, and we traverse to find free
--   variables, and use the <a>Monad</a> to perform substitution that
--   avoids bound variables.
--   
--   An untyped lambda calculus:
--   
--   <pre>
--   {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell #-}
--   import Bound
--   import Control.Applicative
--   import Control.Monad (<a>ap</a>)
--   import Data.Functor.Classes
--   import Data.Foldable
--   import Data.Traversable
--   -- This is from deriving-compat package
--   import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) 
--   </pre>
--   
--   <pre>
--   infixl 9 :@
--   data Exp a = V a | Exp a :@ Exp a | Lam (<a>Scope</a> () Exp a)
--     deriving (<a>Functor</a>,<a>Foldable</a>,<a>Traversable</a>)
--   </pre>
--   
--   <pre>
--   instance <a>Applicative</a> Exp where <a>pure</a> = V; (<a>&lt;*&gt;</a>) = <a>ap</a>
--   instance <a>Monad</a> Exp where
--     <a>return</a> = V
--     V a      <a>&gt;&gt;=</a> f = f a
--     (x :@ y) <a>&gt;&gt;=</a> f = (x <a>&gt;&gt;=</a> f) :@ (y <a>&gt;&gt;=</a> f)
--     Lam e    <a>&gt;&gt;=</a> f = Lam (e <a>&gt;&gt;&gt;=</a> f)
--   </pre>
--   
--   <pre>
--   deriveEq1   ''Exp
--   deriveOrd1  ''Exp
--   deriveRead1 ''Exp
--   deriveShow1 ''Exp
--   
--   instance <a>Eq</a> a   =&gt; <a>Eq</a>   (Exp a) where (==) = eq1
--   instance <a>Ord</a> a  =&gt; <a>Ord</a>  (Exp a) where compare = compare1
--   instance <a>Show</a> a =&gt; <a>Show</a> (Exp a) where showsPrec = showsPrec1
--   instance <a>Read</a> a =&gt; <a>Read</a> (Exp a) where readsPrec = readsPrec1
--   </pre>
--   
--   <pre>
--   lam :: <a>Eq</a> a =&gt; a -&gt; <tt>Exp</tt> a -&gt; <tt>Exp</tt> a
--   lam v b = Lam (<a>abstract1</a> v b)
--   </pre>
--   
--   <pre>
--   whnf :: <tt>Exp</tt> a -&gt; <tt>Exp</tt> a
--   whnf (f :@ a) = case whnf f of
--     Lam b -&gt; whnf (<a>instantiate1</a> a b)
--     f'    -&gt; f' :@ a
--   whnf e = e
--   </pre>
--   
--   More exotic combinators for manipulating a <a>Scope</a> can be
--   imported from <a>Bound.Scope</a>.
--   
--   You can also retain names in your bound variables by using <a>Name</a>
--   and the related combinators from <a>Bound.Name</a>. They are not
--   re-exported from this module by default.
--   
--   The approach used in this package was first elaborated upon by Richard
--   Bird and Ross Patterson in "de Bruijn notation as a nested data type",
--   available from
--   <a>http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf</a>
--   
--   However, the combinators they used required higher rank types. Here we
--   demonstrate that the higher rank <tt>gfold</tt> combinator they used
--   isn't necessary to build the monad and use a monad transformer to
--   encapsulate the novel recursion pattern in their generalized de Bruijn
--   representation. It is named <a>Scope</a> to match up with the
--   terminology and usage pattern from Conor McBride and James McKinna's
--   "I am not a number: I am a free variable", available from
--   <a>http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf</a>, but since
--   the set of variables is visible in the type, we can provide stronger
--   type safety guarantees.
--   
--   There are longer examples in the <tt>examples/</tt> folder:
--   
--   <a>https://github.com/ekmett/bound/tree/master/examples</a>
--   
--   <ol>
--   <li><i>Simple.hs</i> provides an untyped lambda calculus with
--   recursive let bindings and includes an evaluator for the untyped
--   lambda calculus and a longer example taken from Lennart Augustsson's
--   "λ-calculus cooked four ways" available from
--   <a>http://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf</a></li>
--   <li><i>Derived.hs</i> shows how much of the API can be automated with
--   DeriveTraversable and adds combinators for building binders that
--   support pattern matching.</li>
--   <li><i>Overkill.hs</i> provides very strongly typed pattern matching
--   many modern language extensions, including polymorphic kinds to ensure
--   type safety. In general, the approach taken by Derived seems to
--   deliver a better power to weight ratio.</li>
--   </ol>
module Bound

-- | <tt><a>substitute</a> a p w</tt> replaces the free variable <tt>a</tt>
--   with <tt>p</tt> in <tt>w</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
--   ["goodnight","Gracie","!!!"]
--   </pre>
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a

-- | A closed term has no free variables.
--   
--   <pre>
--   &gt;&gt;&gt; isClosed []
--   True
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; isClosed [1,2,3]
--   False
--   </pre>
isClosed :: Foldable f => f a -> Bool

-- | If a term has no free variables, you can freely change the type of
--   free variables it is parameterized on.
--   
--   <pre>
--   &gt;&gt;&gt; closed [12]
--   Nothing
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; closed ""
--   Just []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; :t closed ""
--   closed "" :: Maybe [b]
--   </pre>
closed :: Traversable f => f a -> Maybe (f b)

-- | <tt><a>Scope</a> b f a</tt> is an <tt>f</tt> expression with bound
--   variables in <tt>b</tt>, and free variables in <tt>a</tt>
--   
--   We store bound variables as their generalized de Bruijn representation
--   in that we're allowed to <a>lift</a> (using <a>F</a>) an entire tree
--   rather than only succ individual variables, but we're still only
--   allowed to do so once per <a>Scope</a>. Weakening trees permits
--   <i>O(1)</i> weakening and permits more sharing opportunities. Here the
--   deBruijn 0 is represented by the <a>B</a> constructor of <a>Var</a>,
--   while the de Bruijn <a>succ</a> (which may be applied to an entire
--   tree!) is handled by <a>F</a>.
--   
--   NB: equality and comparison quotient out the distinct <a>F</a>
--   placements allowed by the generalized de Bruijn representation and
--   return the same result as a traditional de Bruijn representation
--   would.
--   
--   Logically you can think of this as if the shape were the traditional
--   <tt>f (Var b a)</tt>, but the extra <tt>f a</tt> inside permits us a
--   cheaper <a>lift</a>.
newtype Scope b f a
Scope :: f (Var b (f a)) -> Scope b f a
[unscope] :: Scope b f a -> f (Var b (f a))

-- | Capture some free variables in an expression to yield a <a>Scope</a>
--   with bound variables in <tt>b</tt>
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; abstract (`elemIndex` "bar") "barry"
--   Scope [B 0,B 1,B 2,B 2,F "y"]
--   </pre>
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

-- | Abstract over a single variable
--   
--   <pre>
--   &gt;&gt;&gt; abstract1 'x' "xyz"
--   Scope [B (),F "y",F "z"]
--   </pre>
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a

-- | Enter a scope, instantiating all bound variables
--   
--   <pre>
--   &gt;&gt;&gt; :m + Data.List
--   
--   &gt;&gt;&gt; instantiate (\x -&gt; [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
--   "abccy"
--   </pre>
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

-- | Enter a <a>Scope</a> that binds one variable, instantiating it
--   
--   <pre>
--   &gt;&gt;&gt; instantiate1 "x" $ Scope [B (),F "y",F "z"]
--   "xyz"
--   </pre>
instantiate1 :: Monad f => f a -> Scope n f a -> f a

-- | Instances of <a>Bound</a> generate left modules over monads.
--   
--   This means they should satisfy the following laws:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> <a>return</a> ≡ m
--   m <a>&gt;&gt;&gt;=</a> (λ x → k x <a>&gt;&gt;=</a> h) ≡ (m <a>&gt;&gt;&gt;=</a> k) <a>&gt;&gt;&gt;=</a> h
--   </pre>
--   
--   This guarantees that a typical Monad instance for an expression type
--   where Bound instances appear will satisfy the Monad laws (see
--   doc/BoundLaws.hs).
--   
--   If instances of <a>Bound</a> are monad transformers, then <tt>m
--   <a>&gt;&gt;&gt;=</a> f ≡ m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a>
--   f</tt> implies the above laws, and is in fact the default definition.
--   
--   This is useful for types like expression lists, case alternatives,
--   schemas, etc. that may not be expressions in their own right, but
--   often contain expressions.
--   
--   <i>Note:</i> <a>Free</a> isn't "really" a monad transformer, even if
--   the kind matches. Therefore there isn't <tt><a>Bound</a>
--   <a>Free</a></tt> instance.
class Bound t

-- | Perform substitution
--   
--   If <tt>t</tt> is an instance of <tt>MonadTrans</tt> and you are
--   compiling on GHC &gt;= 7.4, then this gets the default definition:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> f = m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a> f
--   </pre>
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c

-- | Perform substitution
--   
--   If <tt>t</tt> is an instance of <tt>MonadTrans</tt> and you are
--   compiling on GHC &gt;= 7.4, then this gets the default definition:
--   
--   <pre>
--   m <a>&gt;&gt;&gt;=</a> f = m <a>&gt;&gt;=</a> <a>lift</a> <a>.</a> f
--   </pre>
(>>>=) :: (Bound t, MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c
infixl 1 >>>=

-- | A flipped version of (<a>&gt;&gt;&gt;=</a>).
--   
--   <pre>
--   (<a>=&lt;&lt;&lt;</a>) = <a>flip</a> (<a>&gt;&gt;&gt;=</a>)
--   </pre>
(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
infixr 1 =<<<

-- | "I am not a number, I am a <i>free monad</i>!"
--   
--   A <tt><a>Var</a> b a</tt> is a variable that may either be "bound"
--   (<a>B</a>) or "free" (<a>F</a>).
--   
--   (It is also technically a free monad in the same near-trivial sense as
--   <a>Either</a>.)
data Var b a

-- | this is a bound variable
B :: b -> Var b a

-- | this is a free variable
F :: a -> Var b a

-- | <tt><a>fromScope</a></tt> quotients out the possible placements of
--   <a>F</a> in <a>Scope</a> by distributing them all to the leaves. This
--   yields a more traditional de Bruijn indexing scheme for bound
--   variables.
--   
--   Since,
--   
--   <pre>
--   <a>fromScope</a> <a>.</a> <a>toScope</a> ≡ <a>id</a>
--   </pre>
--   
--   we know that
--   
--   <pre>
--   <a>fromScope</a> <a>.</a> <a>toScope</a> <a>.</a> <a>fromScope</a> ≡ <a>fromScope</a>
--   </pre>
--   
--   and therefore <tt>(<a>toScope</a> . <a>fromScope</a>)</tt> is
--   idempotent.
fromScope :: Monad f => Scope b f a -> f (Var b a)

-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
--   
--   This requires a full tree traversal
toScope :: Monad f => f (Var b a) -> Scope b f a

-- | Use to automatically derive <a>Applicative</a> and <a>Monad</a>
--   instances for your datatype.
--   
--   Also works for components that are lists or instances of
--   <a>Functor</a>, but still does not work for a great deal of other
--   things.
--   
--   <tt>deriving-compat</tt> package may be used to derive the
--   <tt>Show1</tt> and <tt>Read1</tt> instances
--   
--   <pre>
--   {-# LANGUAGE DeriveFunctor      #-}
--   {-# LANGUAGE TemplateHaskell    #-}
--   
--   import Bound                (Scope, makeBound)
--   import Data.Functor.Classes (Show1, Read1, shosPrec1, readsPrec1)
--   import Data.Deriving        (deriveShow1, deriveRead1)
--   
--   data Exp a
--     = V a
--     | App (Exp a) (Exp a)
--     | Lam (Scope () Exp a)
--     | ND [Exp a]
--     | I Int
--     deriving (Functor)
--   
--   makeBound ''Exp
--   deriveShow1 ''Exp
--   deriveRead1 ''Exp
--   instance Read a =&gt; Read (Exp a) where readsPrec = readsPrec1
--   instance Show a =&gt; Show (Exp a) where showsPrec = showsPrec1
--   </pre>
--   
--   and in GHCi
--   
--   <pre>
--   ghci&gt; :set -XDeriveFunctor
--   ghci&gt; :set -XTemplateHaskell
--   ghci&gt; import Bound                (Scope, makeBound)
--   ghci&gt; import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
--   ghci&gt; import Data.Deriving        (deriveShow1, deriveRead1)
--   ghci&gt; :{
--   ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)
--   ghci| makeBound ''Exp
--   ghci| deriveShow1 ''Exp
--   ghci| deriveRead1 ''Exp
--   ghci| instance Read a =&gt; Read (Exp a) where readsPrec = readsPrec1
--   ghci| instance Show a =&gt; Show (Exp a) where showsPrec = showsPrec1
--   ghci| :}
--   </pre>
--   
--   <a>Eq</a> and <a>Ord</a> instances can be derived similarly
--   
--   <pre>
--   import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   import Data.Deriving        (deriveEq1, deriveOrd1)
--   
--   deriveEq1 ''Exp
--   deriveOrd1 ''Exp
--   instance Eq a =&gt; Eq (Exp a) where (==) = eq1
--   instance Ord a =&gt; Ord (Exp a) where compare = compare1
--   </pre>
--   
--   or in GHCi:
--   
--   <pre>
--   ghci&gt; import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   ghci&gt; import Data.Deriving        (deriveEq1, deriveOrd1)
--   ghci&gt; :{
--   ghci| deriveEq1 ''Exp
--   ghci| deriveOrd1 ''Exp
--   ghci| instance Eq a =&gt; Eq (Exp a) where (==) = eq1
--   ghci| instance Ord a =&gt; Ord (Exp a) where compare = compare1
--   ghci| :}
--   </pre>
--   
--   We cannot automatically derive <a>Eq</a> and <a>Ord</a> using the
--   standard GHC mechanism, because instances require <tt>Exp</tt> to be a
--   <a>Monad</a>:
--   
--   <pre>
--   instance (Monad f, Eq b, Eq1 f, Eq a)    =&gt; Eq (Scope b f a)
--   instance (Monad f, Ord b, Ord1 f, Ord a) =&gt; Ord (Scope b f a)
--   </pre>
makeBound :: Name -> DecsQ
