-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Haskell 98/2010 Locally-Nameless Generalized de Bruijn Terms
--
-- We represent the target language itself as an ideal monad supplied by
-- the user, and provide a Scope monad transformer for introducing
-- bound variables in user supplied terms. Users supply a Monad
-- and Traversable instance, and we traverse to find free
-- variables, and use the Monad to perform substitution that avoids bound
-- variables.
--
-- An untyped lambda calculus:
--
--
-- import Bound
-- import Prelude.Extras
--
--
--
-- infixl 9 :@
-- data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
-- deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
--
--
--
-- instance Eq1 Exp where (==#) = (==)
-- instance Ord1 Exp where compare1 = compare
-- instance Show1 Exp where showsPrec1 = showsPrec
-- instance Read1 Exp where readsPrec1 = readsPrec
-- instance Applicative Exp where pure = V; (<*>) = ap
--
--
--
-- instance Monad Exp where
-- return = V
-- V a >>= f = f a
-- (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
-- Lam e >>= f = Lam (e >>>= f)
--
-- lam :: Eq a => a -> Exp a -> Exp a
-- lam v b = Lam (abstract1 v b)
--
--
--
-- whnf :: Exp a -> Exp a
-- whnf (f :@ a) = case whnf f of
-- Lam b -> whnf (instantiate1 a b)
-- f' -> f' :@ a
-- whnf e = e
--
--
-- The classes from Prelude.Extras are used to facilitate the automatic
-- deriving of Eq, Ord, Show, and Read in the
-- presence of polymorphic recursion used inside Scope.
--
-- 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 lift whole trees
-- instead of just applying succ to individual variables,
-- weakening the all variables bound by a scope. and by giving binders
-- more structure we can permit easy simultaneous substitution.
--
-- The approach was first elaborated upon by Richard Bird and Ross
-- Patterson in "de Bruijn notation as a nested data type", available
-- from
-- http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf
--
-- However, the combinators they used required higher rank types. Here we
-- demonstrate that the higher rank gfold 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 Scope 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
-- http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf, but
-- since the set of variables is visible in the type, we can provide
-- stronger type safety guarantees.
--
-- There are longer examples in the examples/ folder:
--
-- https://github.com/ekmett/bound/tree/master/examples
--
--
-- - Simple.hs 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
-- http://www.augustsson.net/Darcs/Lambda/top.pdf
-- - Derived.hs shows how much of the API can be automated with
-- DeriveTraversable and adds combinators for building binders that
-- support pattern matching.
-- - Overkill.hs 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.
--
@package bound
@version 0.3.2
module Bound.Term
-- | substitute p a w replaces the free variable a
-- with p in w
substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a
-- | A closed term has no free variables.
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.
closed :: Traversable f => f a -> Maybe (f b)
module Bound.Class
-- | Instances may or may not be monad transformers.
--
-- If they are, then you can use m >>>= f = m >>= lift
-- . f
--
-- 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 where m >>>= f = m >>= lift . f
(>>>=) :: (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 free monad!"
--
-- A Var b a is a variable that may either be "bound" or "free".
--
-- (It is also technically a free monad in the same near trivial sense as
-- Either.)
data Var b a
-- | this is a bound variable
B :: b -> Var b a
-- | this is a free variable
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
-- | Scope b f a is an f expression with bound
-- variables in b, and free variables in a
--
-- We store bound variables as their generalized de Bruijn representation
-- in that we're allowed to lift (using F) an entire tree
-- rather than only succ individual variables, but we're still only
-- allowed to do so once per Scope. Weakening trees permits
-- O(1) weakening and permits more sharing opportunities. Here the
-- deBruijn 0 is represented by the B constructor of Var,
-- while the de Bruijn succ (which may be applied to an entire
-- tree!) is handled by F.
--
-- NB: equality and comparison quotient out the distinct F
-- 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
-- f (Var b a), but the extra f a inside permits us a
-- cheaper lift.
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 Scope
-- with bound variables in b
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 that binds one variable, instantiating it
instantiate1 :: Monad f => f a -> Scope () f a -> f a
-- | fromScope quotients out the possible placements of
-- F in Scope by distributing them all to the leaves. This
-- yields a more traditional de Bruijn indexing scheme for bound
-- variables.
--
--
-- fromScope . toScope = id
-- fromScope . toScope . fromScope = fromScope
--
--
-- (toScope . fromScope) 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
-- Scope
splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c
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
-- Monad instance
liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a
-- | A version of mapScope that can be used when you only have the
-- Monad 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
traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()
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 traverseScope_ that can be used when you only have a
-- Monad instance
mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()
traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)
traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)
mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)
mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
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)
-- | We represent the target language itself as an ideal monad supplied by
-- the user, and provide a Scope monad transformer for introducing
-- bound variables in user supplied terms. Users supply a Monad
-- and Traversable instance, and we traverse to find free
-- variables, and use the Monad to perform substitution that
-- avoids bound variables.
--
-- An untyped lambda calculus:
--
--
-- import Bound
-- import Prelude.Extras
--
--
--
-- infixl 9 :@
-- data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
-- deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
--
--
--
-- instance Eq1 Exp where (==#) = (==)
-- instance Ord1 Exp where compare1 = compare
-- instance Show1 Exp where showsPrec1 = showsPrec
-- instance Read1 Exp where readsPrec1 = readsPrec
-- instance Applicative Exp where pure = V; (<*>) = ap
--
--
--
-- instance Monad Exp where
-- return = V
-- V a >>= f = f a
-- (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
-- Lam e >>= f = Lam (e >>>= f)
--
-- lam :: Eq a => a -> Exp a -> Exp a
-- lam v b = Lam (abstract1 v b)
--
--
--
-- whnf :: Exp a -> Exp a
-- whnf (f :@ a) = case whnf f of
-- Lam b -> whnf (instantiate1 a b)
-- f' -> f' :@ a
-- whnf e = e
--
--
-- More exotic combinators for manipulating a Scope can be
-- imported from Bound.Scope.
module Bound
-- | substitute p a w replaces the free variable a
-- with p in w
substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a
-- | A closed term has no free variables.
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.
closed :: Traversable f => f a -> Maybe (f b)
-- | Scope b f a is an f expression with bound
-- variables in b, and free variables in a
--
-- We store bound variables as their generalized de Bruijn representation
-- in that we're allowed to lift (using F) an entire tree
-- rather than only succ individual variables, but we're still only
-- allowed to do so once per Scope. Weakening trees permits
-- O(1) weakening and permits more sharing opportunities. Here the
-- deBruijn 0 is represented by the B constructor of Var,
-- while the de Bruijn succ (which may be applied to an entire
-- tree!) is handled by F.
--
-- NB: equality and comparison quotient out the distinct F
-- 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
-- f (Var b a), but the extra f a inside permits us a
-- cheaper lift.
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 Scope
-- with bound variables in b
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 that binds one variable, instantiating it
instantiate1 :: Monad f => f a -> Scope () f a -> f a
-- | Instances may or may not be monad transformers.
--
-- If they are, then you can use m >>>= f = m >>= lift
-- . f
--
-- 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 where m >>>= f = m >>= lift . f
(>>>=) :: (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
-- | "I am not a number, I am a free monad!"
--
-- A Var b a is a variable that may either be "bound" or "free".
--
-- (It is also technically a free monad in the same near trivial sense as
-- Either.)
data Var b a
-- | this is a bound variable
B :: b -> Var b a
-- | this is a free variable
F :: a -> Var b a
-- | fromScope quotients out the possible placements of
-- F in Scope by distributing them all to the leaves. This
-- yields a more traditional de Bruijn indexing scheme for bound
-- variables.
--
--
-- fromScope . toScope = id
-- fromScope . toScope . fromScope = fromScope
--
--
-- (toScope . fromScope) 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