-- 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 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.
--
-- Slides describing and motivating this approach to name binding are
-- available online at:
--
--
-- http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less
--
-- 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 greatly speeding up
-- instantiation. By giving binders more structure we permit easy
-- simultaneous substitution and further speed up instantiation.
@package bound
@version 0.7
module Bound.Term
-- | substitute a p w replaces the free variable a
-- with p in w.
--
--
-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
-- ["goodnight","Gracie","!!!"]
--
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
-- | substituteVar a b w replaces a free variable
-- a with another free variable b in w.
--
--
-- >>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
-- ["Bob","Bob","Charlie"]
--
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
-- | A closed term has no free variables.
--
--
-- >>> isClosed []
-- True
--
--
--
-- >>> isClosed [1,2,3]
-- False
--
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 [12]
-- Nothing
--
--
--
-- >>> closed ""
-- Just []
--
--
--
-- >>> :t closed ""
-- closed "" :: Maybe [b]
--
closed :: Traversable f => f a -> Maybe (f b)
-- | This module provides the Bound class, for performing
-- substitution into things that are not necessarily full monad
-- transformers.
module Bound.Class
-- | Instances of Bound may or may not be monad transformers.
--
-- If they are, then m >>>= f ≡ m >>=
-- lift . f is required to hold, and is in fact the
-- default definition. If it is not a MonadTrans instance, then
-- you have greater flexibility in how to implement this class.
--
-- 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.
class Bound t where m >>>= f = m >>= lift . f
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c
-- | A flipped version of (>>>=).
--
--
-- (=<<<) = flip (>>>=)
--
(=<<<) :: (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"
-- (B) or "free" (F).
--
-- (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
unvar :: (b -> r) -> (a -> r) -> Var b a -> r
instance Typeable2 Var
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 (Data b, Data a) => Data (Var b a)
instance Generic (Var b a)
instance Datatype D1Var
instance Constructor C1_0Var
instance Constructor C1_1Var
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)
instance (Hashable b, Hashable a) => Hashable (Var b a)
instance Hashable b => Hashable1 (Var b)
instance Hashable2 Var
-- | This is the work-horse of the bound library.
--
-- Scope provides a single generalized de Bruijn level and is
-- often used inside of the definition of binders.
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
--
--
-- >>> :m + Data.List
--
-- >>> abstract (`elemIndex` "bar") "barry"
-- Scope [B 0,B 1,B 2,B 2,F "y"]
--
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
-- | Abstract over a single variable
--
--
-- >>> abstract1 'x' "xyz"
-- Scope [B (),F "y",F "z"]
--
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
-- | Enter a scope, instantiating all bound variables
--
--
-- >>> :m + Data.List
--
-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
-- "abccy"
--
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
-- | Enter a Scope that binds one variable, instantiating it
--
--
-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
-- "xyz"
--
instantiate1 :: Monad f => f a -> Scope n 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.
--
-- Since,
--
--
-- fromScope . toScope ≡ id
--
--
-- we know that
--
--
-- fromScope . toScope . fromScope ≡ fromScope
--
--
-- and therefore (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
-- | Return a list of occurences of the variables bound by this
-- Scope.
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
-- | traverse_ the bound variables in a Scope.
traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()
-- | traverse 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 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 ()
-- | 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 traverseScope that can be used when you only have a
-- Monad instance
mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)
instance (Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a)
instance (Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f)
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)
-- | 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
-- Name n b is a value b 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 not exported from Bound by default. You
-- need to explicitly import it, due to the fact that Name is a
-- pretty common term in other people's code.
module Bound.Name
-- | We track the choice of Name n as a forgettable
-- property that does not affect the result of (==) or
-- compare.
--
-- To compare names rather than values, use (on compare
-- name) instead.
data Name n b
Name :: n -> b -> Name n b
-- | This provides an Iso that can be used to access the parts of
-- a Name.
--
--
-- _Name :: Iso (Name n a) (Name m b) (n, a) (m, b)
--
_Name :: (Profunctor p, Functor f) => p (n, a) (f (m, b)) -> p (Name n a) (f (Name m b))
-- | Extract the name.
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
-- | 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 Scope that binds one (named) variable, instantiating
-- it.
--
--
-- instantiate1Name = instantiate1
--
instantiate1Name :: Monad f => f a -> Scope n f a -> f a
instance Typeable2 Name
instance (Show n, Show b) => Show (Name n b)
instance (Read n, Read b) => Read (Name n b)
instance (Data n, Data b) => Data (Name n b)
instance Generic (Name n b)
instance Datatype D1Name
instance Constructor C1_0Name
instance Read2 Name
instance Show2 Name
instance Ord2 Name
instance Eq2 Name
instance Read b => Read1 (Name b)
instance Show b => Show1 (Name b)
instance Ord1 (Name b)
instance Eq1 (Name b)
instance Comonad (Name n)
instance Bitraversable Name
instance Bifoldable Name
instance Bifunctor Name
instance Traversable (Name n)
instance Foldable (Name n)
instance Functor (Name n)
instance Ord b => Ord (Name n b)
instance Hashable a => Hashable (Name n a)
instance Hashable1 (Name n)
instance Hashable2 Name
instance Eq b => Eq (Name n b)
-- | 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:
--
--
-- {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-- import Bound
-- import Control.Applicative
-- import Control.Monad (ap)
-- import Prelude.Extras
-- import Data.Foldable
-- import Data.Traverable
--
--
--
-- 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
-- instance Ord1 Exp
-- instance Show1 Exp
-- instance Read1 Exp
-- 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.
--
-- You can also retain names in your bound variables by using Name
-- and the related combinators from Bound.Name. 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
-- 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.
--
module Bound
-- | substitute a p w replaces the free variable a
-- with p in w.
--
--
-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
-- ["goodnight","Gracie","!!!"]
--
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
-- | A closed term has no free variables.
--
--
-- >>> isClosed []
-- True
--
--
--
-- >>> isClosed [1,2,3]
-- False
--
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 [12]
-- Nothing
--
--
--
-- >>> closed ""
-- Just []
--
--
--
-- >>> :t closed ""
-- closed "" :: Maybe [b]
--
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
--
--
-- >>> :m + Data.List
--
-- >>> abstract (`elemIndex` "bar") "barry"
-- Scope [B 0,B 1,B 2,B 2,F "y"]
--
abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a
-- | Abstract over a single variable
--
--
-- >>> abstract1 'x' "xyz"
-- Scope [B (),F "y",F "z"]
--
abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a
-- | Enter a scope, instantiating all bound variables
--
--
-- >>> :m + Data.List
--
-- >>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
-- "abccy"
--
instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a
-- | Enter a Scope that binds one variable, instantiating it
--
--
-- >>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
-- "xyz"
--
instantiate1 :: Monad f => f a -> Scope n f a -> f a
-- | Instances of Bound may or may not be monad transformers.
--
-- If they are, then m >>>= f ≡ m >>=
-- lift . f is required to hold, and is in fact the
-- default definition. If it is not a MonadTrans instance, then
-- you have greater flexibility in how to implement this class.
--
-- 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.
class Bound t where m >>>= f = m >>= lift . f
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c
-- | A flipped version of (>>>=).
--
--
-- (=<<<) = flip (>>>=)
--
(=<<<) :: (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"
-- (B) or "free" (F).
--
-- (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.
--
-- Since,
--
--
-- fromScope . toScope ≡ id
--
--
-- we know that
--
--
-- fromScope . toScope . fromScope ≡ fromScope
--
--
-- and therefore (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