-- 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 2.0.3 -- | This module provides the Bound class, for performing -- substitution into things that are not necessarily full monad -- transformers. module Bound.Class -- | Instances of Bound generate left modules over monads. -- -- This means they should satisfy the following laws: -- --
--   m >>>= return ≡ m
--   m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h
--   
-- -- 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 Bound are monad transformers, then m -- >>>= f ≡ m >>= lift . -- f 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. -- -- Note: Free isn't "really" a monad transformer, even if -- the kind matches. Therefore there isn't Bound -- Free instance. class Bound t -- | Perform substitution -- -- If t is an instance of MonadTrans and you are -- compiling on GHC >= 7.4, then this gets the default definition: -- --
--   m >>>= f = m >>= lift . f
--   
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c -- | Perform substitution -- -- If t is an instance of MonadTrans and you are -- compiling on GHC >= 7.4, then this gets the default definition: -- --
--   m >>>= f = m >>= lift . f
--   
(>>>=) :: (Bound t, MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c infixl 1 >>>= -- | A flipped version of (>>>=). -- --
--   (=<<<) = flip (>>>=)
--   
(=<<<) :: (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 Applicative and -- Monad instances for data types. module Bound.TH -- | Use to automatically derive Applicative and Monad -- instances for your datatype. -- -- Also works for components that are lists or instances of -- Functor, but still does not work for a great deal of other -- things. -- -- deriving-compat package may be used to derive the -- Show1 and Read1 instances -- --
--   {-# LANGUAGE DeriveFunctor      #-}
--   {-# LANGUAGE TemplateHaskell    #-}
--   
--   import Bound                (Scope, makeBound)
--   import Data.Functor.Classes (Show1, Read1, showsPrec1, 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 => Read (Exp a) where readsPrec = readsPrec1
--   instance Show a => Show (Exp a) where showsPrec = showsPrec1
--   
-- -- and in GHCi -- --
--   ghci> :set -XDeriveFunctor
--   ghci> :set -XTemplateHaskell
--   ghci> import Bound                (Scope, makeBound)
--   ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
--   ghci> import Data.Deriving        (deriveShow1, deriveRead1)
--   ghci> :{
--   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 => Read (Exp a) where readsPrec = readsPrec1
--   ghci| instance Show a => Show (Exp a) where showsPrec = showsPrec1
--   ghci| :}
--   
-- -- Eq and Ord instances can be derived similarly -- --
--   import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   import Data.Deriving        (deriveEq1, deriveOrd1)
--   
--   deriveEq1 ''Exp
--   deriveOrd1 ''Exp
--   instance Eq a => Eq (Exp a) where (==) = eq1
--   instance Ord a => Ord (Exp a) where compare = compare1
--   
-- -- or in GHCi: -- --
--   ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   ghci> import Data.Deriving        (deriveEq1, deriveOrd1)
--   ghci> :{
--   ghci| deriveEq1 ''Exp
--   ghci| deriveOrd1 ''Exp
--   ghci| instance Eq a => Eq (Exp a) where (==) = eq1
--   ghci| instance Ord a => Ord (Exp a) where compare = compare1
--   ghci| :}
--   
-- -- We cannot automatically derive Eq and Ord using the -- standard GHC mechanism, because instances require Exp to be a -- Monad: -- --
--   instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
--   instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
--   
makeBound :: Name -> DecsQ instance GHC.Show.Show Bound.TH.Prop instance GHC.Show.Show Bound.TH.Components 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) 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 -- | This provides a Prism that can be used with lens -- library to access a bound Var. -- --
--   _B :: Prism (Var b a) (Var b' a) b b'@
--   
_B :: (Choice p, Applicative f) => p b (f b') -> p (Var b a) (f (Var b' a)) -- | This provides a Prism that can be used with lens -- library to access a free Var. -- --
--   _F :: Prism (Var b a) (Var b a') a a'@
--   
_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) -- | Scope provides a single traditional de Bruijn level and is -- often used inside of the definition of binders. module Bound.Scope.Simple -- | Scope b f a is an f expression with bound -- variables in b, and free variables in a -- -- This implements traditional de Bruijn indices, while Scope -- implements generalized de Bruijn indices. -- -- These traditional indices can be used to test the performance gain of -- generalized indices. -- -- While this type Scope is identical to EitherT this -- module focuses on a drop-in replacement for Scope. -- -- Another use case is for syntaxes not stable under substitution, -- therefore with only a Functor instance and no Monad -- 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 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 :: Functor 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 :: (Functor 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 is just another name for unscope and -- is exported to mimick fromScope. In particular no Monad -- constraint is required. fromScope :: Scope b f a -> f (Var b a) -- | toScope is just another name for Scope and is -- exported to mimick toScope. In particular no Monad -- constraint is required. toScope :: 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) 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 bitraverse a Scope. 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 traverse. 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 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 -- | Capture some free variables in an expression to yield a Scope -- with bound variables in b. 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 -- --
--   >>> :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 -- | 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 -- | 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 . toScopeid
--   
-- -- we know that -- --
--   fromScope . toScope . fromScopefromScope
--   
-- -- 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 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 -- | 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 the bound variables in a Scope. 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) 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 f to g 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 bitraverse a Scope. 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 traverse. 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 -- 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 -- | Capture some free variables in an expression to yield a Scope -- 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 Scope that binds one (named) variable, instantiating -- it. -- --
--   instantiate1Name = instantiate1
--   
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 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, TemplateHaskell #-}
--   import Bound
--   import Control.Applicative
--   import Control.Monad (ap)
--   import Data.Functor.Classes
--   import Data.Foldable
--   import Data.Traversable
--   -- This is from deriving-compat package
--   import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) 
--   
-- --
--   infixl 9 :@
--   data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
--     deriving (Functor,Foldable,Traversable)
--   
-- --
--   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)
--   
-- --
--   deriveEq1   ''Exp
--   deriveOrd1  ''Exp
--   deriveRead1 ''Exp
--   deriveShow1 ''Exp
--   
--   instance Eq a   => Eq   (Exp a) where (==) = eq1
--   instance Ord a  => Ord  (Exp a) where compare = compare1
--   instance Show a => Show (Exp a) where showsPrec = showsPrec1
--   instance Read a => Read (Exp a) where readsPrec = readsPrec1
--   
-- --
--   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.ru.nl/~james/RESEARCH/haskell2004.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 -- --
    --
  1. 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://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf
  2. --
  3. Derived.hs shows how much of the API can be automated with -- DeriveTraversable and adds combinators for building binders that -- support pattern matching.
  4. --
  5. 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.
  6. --
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 generate left modules over monads. -- -- This means they should satisfy the following laws: -- --
--   m >>>= return ≡ m
--   m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h
--   
-- -- 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 Bound are monad transformers, then m -- >>>= f ≡ m >>= lift . -- f 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. -- -- Note: Free isn't "really" a monad transformer, even if -- the kind matches. Therefore there isn't Bound -- Free instance. class Bound t -- | Perform substitution -- -- If t is an instance of MonadTrans and you are -- compiling on GHC >= 7.4, then this gets the default definition: -- --
--   m >>>= f = m >>= lift . f
--   
(>>>=) :: (Bound t, Monad f) => t f a -> (a -> f c) -> t f c -- | Perform substitution -- -- If t is an instance of MonadTrans and you are -- compiling on GHC >= 7.4, then this gets the default definition: -- --
--   m >>>= f = m >>= lift . f
--   
(>>>=) :: (Bound t, MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c infixl 1 >>>= -- | A flipped version of (>>>=). -- --
--   (=<<<) = flip (>>>=)
--   
(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c infixr 1 =<<< -- | "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 . toScopeid
--   
-- -- we know that -- --
--   fromScope . toScope . fromScopefromScope
--   
-- -- 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 -- | Use to automatically derive Applicative and Monad -- instances for your datatype. -- -- Also works for components that are lists or instances of -- Functor, but still does not work for a great deal of other -- things. -- -- deriving-compat package may be used to derive the -- Show1 and Read1 instances -- --
--   {-# LANGUAGE DeriveFunctor      #-}
--   {-# LANGUAGE TemplateHaskell    #-}
--   
--   import Bound                (Scope, makeBound)
--   import Data.Functor.Classes (Show1, Read1, showsPrec1, 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 => Read (Exp a) where readsPrec = readsPrec1
--   instance Show a => Show (Exp a) where showsPrec = showsPrec1
--   
-- -- and in GHCi -- --
--   ghci> :set -XDeriveFunctor
--   ghci> :set -XTemplateHaskell
--   ghci> import Bound                (Scope, makeBound)
--   ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
--   ghci> import Data.Deriving        (deriveShow1, deriveRead1)
--   ghci> :{
--   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 => Read (Exp a) where readsPrec = readsPrec1
--   ghci| instance Show a => Show (Exp a) where showsPrec = showsPrec1
--   ghci| :}
--   
-- -- Eq and Ord instances can be derived similarly -- --
--   import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   import Data.Deriving        (deriveEq1, deriveOrd1)
--   
--   deriveEq1 ''Exp
--   deriveOrd1 ''Exp
--   instance Eq a => Eq (Exp a) where (==) = eq1
--   instance Ord a => Ord (Exp a) where compare = compare1
--   
-- -- or in GHCi: -- --
--   ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
--   ghci> import Data.Deriving        (deriveEq1, deriveOrd1)
--   ghci> :{
--   ghci| deriveEq1 ''Exp
--   ghci| deriveOrd1 ''Exp
--   ghci| instance Eq a => Eq (Exp a) where (==) = eq1
--   ghci| instance Ord a => Ord (Exp a) where compare = compare1
--   ghci| :}
--   
-- -- We cannot automatically derive Eq and Ord using the -- standard GHC mechanism, because instances require Exp to be a -- Monad: -- --
--   instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
--   instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)
--   
makeBound :: Name -> DecsQ