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


-- | Combinators for manipulating locally-nameless generalized de Bruijn terms
--   
--   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. To that end we provide haskell 98 combinators for manipulating
--   locally-nameless generalized de Bruijn terms, build over user-supplied
--   term types. A generalized de Bruijn term is one where you can
--   <a>succ</a> whole trees instead of just individual variables.
--   
--   The approach was first elaborated in Bird and Patterson, "de Bruijn
--   notation as a nested data type":
--   
--   
--   <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
--   use a monad transformer to encapsulate the novel recursion pattern in
--   their generalized de Bruijn representation. It is named Scope to match
--   up with the terminology from Conor McBride and James McKinna's "I am
--   not a number: I am a free variable", while providing stronger type
--   safety guarantees.
--   
--   <a>http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf</a>
--   
--   There are three worked examples in the examples folder:
--   
--   <ul>
--   <li><i>Simple.hs</i> provides an untyped lambda calculus with
--   recursive let bindings.</li>
--   <li><i>Derived.hs</i> shows how much of the API can be automated with
--   DeriveTraversable and adds combinators for building binders with
--   pattern matching.</li>
--   <li><i>Overkill.hs</i> provides very strongly typed pattern matching
--   many modern type 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>
--   </ul>
@package bound
@version 0.1.3


module Bound.Term

-- | <tt><a>substitute</a> p a w</tt> replaces the free variable <tt>a</tt>
--   with <tt>p</tt> in <tt>w</tt>
substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a
isClosed :: Foldable f => f a -> Bool

-- | If a term has no free variables, you can freely change the type of
--   free variables it uses
closed :: Traversable f => f a -> Maybe (f b)


module Bound.Class

-- | Instantces may or may not be monad transformers.
--   
--   If they are, then you can use <tt>m &gt;&gt;&gt;= f = m &gt;&gt;= lift
--   . f</tt>
--   
--   This is useful for types like expression lists, case alternatives,
--   schemas, etc. that may not be expressions in their own right, but
--   often contain one.
class Bound t
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c
(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c


module Bound.Var

-- | "I am not a number, I am a <i>free monad</i>!"
--   
--   <tt>Var b a</tt> represents variables that may either be <a>bound</a>
--   (<tt>B</tt>) or <a>free</a> (<tt>F</tt>)
data Var b a
B :: b -> Var b a
F :: a -> Var b a
instance (Eq b, Eq a) => Eq (Var b a)
instance (Ord b, Ord a) => Ord (Var b a)
instance (Show b, Show a) => Show (Var b a)
instance (Read b, Read a) => Read (Var b a)
instance Read b => Read1 (Var b)
instance Show b => Show1 (Var b)
instance Ord b => Ord1 (Var b)
instance Eq b => Eq1 (Var b)
instance Read2 Var
instance Show2 Var
instance Ord2 Var
instance Eq2 Var
instance Bitraversable Var
instance Bifoldable Var
instance Bifunctor Var
instance Monad (Var b)
instance Applicative (Var b)
instance Traversable (Var b)
instance Foldable (Var b)
instance Functor (Var b)


module Bound.Scope

-- | <tt><a>Scope</a> b f a</tt> is a an <tt>f</tt> expression with bound
--   variables in <tt>b</tt>, and free variables in <tt>a</tt>
--   
--   This stores bound variables as their generalized de Bruijn
--   representation, in that the succ's for variable ids are allowed to
--   occur anywhere within the tree permitting <i>O(1)</i> weakening and
--   allowing 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 choice of a generalized de Bruijn
--   representation and return the same result as a traditional de Bruijn
--   representation would.
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>
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

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

-- | Enter a scope, instantiating all bound variables
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

-- | Enter a scope with one bound variable, instantiating it
instantiate1 :: Monad f => f a -> Scope () f a -> f a

-- | Perform substitution on both bound and free variables in a scope
splat :: Monad f => (a -> f c) -> (b -> 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.
--   
--   <pre>
--   fromScope . toScope = id
--   fromScope . toScope . fromScope = fromScope
--   </pre>
--   
--   <tt>(<a>toScope</a> . <a>fromScope</a>)</tt> is idempotent
fromScope :: Monad f => Scope b f a -> f (Var b a)
toScope :: Monad f => f (Var b a) -> Scope b f a
instance Bound (Scope b)
instance (Functor f, Read b, Read1 f) => Read1 (Scope b f)
instance (Functor f, Read b, Read1 f, Read a) => Read (Scope b f a)
instance (Functor f, Show b, Show1 f) => Show1 (Scope b f)
instance (Functor f, Show b, Show1 f, Show a) => Show (Scope b f a)
instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f)
instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f)
instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a)
instance MonadTrans (Scope b)
instance Monad f => Monad (Scope b f)
instance Traversable f => Traversable (Scope b f)
instance Foldable f => Foldable (Scope b f)
instance Functor f => Functor (Scope b f)


module Bound