-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | ScopeH and ScopeT extras for bound
--
-- Provides more complex Scope variants; ScopeT and
-- ScopeH:
--
--
-- Scope b f a ~ ScopeT b IdentityT f a ~ ScopeH b f f a
-- ScopeT b t f a ~ ScopeH b (t f) f a
--
--
-- ScopeH probably should be preferred over ScopeT. Latter
-- is left here for completeness.
--
-- Simple implementations of ScopeH and ScopeT would be
-- similar (sans type arguments) to Bound.Scope.Simple.
--
-- Look into examples/ directory for System F and
-- Bidirectional STLC implemented with a help of ScopeH.
@package bound-extras
@version 0
-- | Right monad Module type-class.
--
-- Most possible instances are omitted. The primary use-case for
-- Module is to power ScopeH.
module Control.Monad.Module
-- | f is right m-module. (according to
-- https://ncatlab.org/nlab/show/module+over+a+monad#modules
-- definitions). We have Compose f m ~> f natural
-- transformation.
--
-- Laws
--
--
-- fma >>== return = fma
-- fma >>== (f >=> g) = (fma >>== f) >>== g
--
--
-- Properties
--
-- For all Monad m we can write associated instance
-- Module m m where (>>==) = (>>=).
--
-- mjoin and >>== are equivalent in power:
--
--
-- fa >>== amb = mjoin (fmap amb fa)
--
class (Functor f, Monad m) => Module f m
-- | Called action.
(>>==) :: Module f m => f a -> (a -> m b) -> f b
-- | Module's join variant.
mjoin :: Module f m => f (m a) -> f a
-- | Module m (t m) action's implementation.
transAction :: (MonadTrans t, Monad m, Monad (t m)) => t m a -> (a -> m b) -> t m b
-- | Module m (Compose f m) action's implementation.
composeAction :: (Functor f, Monad m) => Compose f m a -> (a -> m b) -> Compose f m b
instance GHC.Base.Monad m => Control.Monad.Module.Module m Data.Functor.Identity.Identity
instance GHC.Base.Monad m => Control.Monad.Module.Module (Bound.Scope.Scope b m) m
-- | ScopeT scope, which allows substitute f into 't f' to
-- get new 't f'.
--
-- Consider using ScopeH, it might be clearer.
module Bound.ScopeT
-- | Scope b f a is a t f expression abstracted
-- over f, with bound variables in b, and free
-- variables in a.
--
--
-- Scope n f a ~ ScopeT n IdentityT f a
-- ScopeT n t f a ~ t (Scope n f) a
--
newtype ScopeT b t f a
ScopeT :: t f (Var b (f a)) -> ScopeT b t f a
[unscopeT] :: ScopeT b t f a -> t f (Var b (f a))
-- | We cannot write Bound (ScopeT n t) pre-GHC-8.6
-- (without an auxiliary type class).
(>>>>=) :: (Monad f, Functor (t f)) => ScopeT b t f a -> (a -> f c) -> ScopeT b t f c
-- | Capture some free variables in an expression to yield a ScopeT
-- with bound variables in b.
abstractT :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT b t f a
-- | Abstract over a single variable.
--
--
-- >>> abstract1T 'x' (MaybeT (Nothing : map Just "xyz"))
-- ScopeT (MaybeT [Nothing,Just (B ()),Just (F "y"),Just (F "z")])
--
abstract1T :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT () t f a
-- | Capture some free variables in an expression to yield a ScopeT
-- with bound variables in b. Optionally change the types of the
-- remaining free variables.
abstractTEither :: (Functor (t f), Monad f) => (a -> Either b c) -> t f a -> ScopeT b t f c
-- | Abstraction, capturing named bound variables.
abstractTName :: (Functor (t f), Monad f) => (a -> Maybe b) -> t f a -> ScopeT (Name a b) t f a
-- | Abstract over a single variable
abstract1TName :: (Functor (t f), Monad f, Eq a) => a -> t f a -> ScopeT (Name a ()) t f a
-- | Enter a ScopeT, instantiating all bound variables
instantiateT :: (Bound t, Monad f) => (b -> f a) -> ScopeT b t f a -> t f a
-- | Enter a ScopeT that binds one variable, instantiating it
instantiate1T :: (Bound t, Monad f) => f a -> ScopeT b t f a -> t f a
-- | Enter a ScopeT, and instantiate all bound and free variables in
-- one go.
instantiateTEither :: (Bound t, Monad f) => (Either b a -> f c) -> ScopeT b t f a -> t f c
-- | Convert to traditional de Bruijn.
fromScopeT :: (Bound t, Monad f) => ScopeT b t f a -> t f (Var b a)
-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
toScopeT :: (Functor (t f), Monad f) => t f (Var b a) -> ScopeT b t f a
-- | Convert to Scope.
lowerScopeT :: (Functor (t f), Functor f) => (forall x. t f x -> g x) -> (forall x. f x -> g x) -> ScopeT b t f a -> Scope b g a
-- | Perform substitution on both bound and free variables in a
-- ScopeT.
splatT :: (Bound t, Monad f) => (a -> f c) -> (b -> f c) -> ScopeT b t f a -> t f c
-- | Return a list of occurences of the variables bound by this
-- ScopeT.
bindingsT :: Foldable (t f) => ScopeT b t f a -> [b]
-- | Perform a change of variables on bound variables.
mapBoundT :: Functor (t f) => (b -> b') -> ScopeT b t f a -> ScopeT b' t f a
-- | Perform a change of variables, reassigning both bound and free
-- variables.
mapScopeT :: (Functor (t f), Functor f) => (b -> d) -> (a -> c) -> ScopeT b t f a -> ScopeT d t f c
-- | Obtain a result by collecting information from bound variables
foldMapBoundT :: (Foldable (t f), Monoid r) => (b -> r) -> ScopeT b t f a -> r
-- | Obtain a result by collecting information from both bound and free
-- variables
foldMapScopeT :: (Foldable f, Foldable (t f), Monoid r) => (b -> r) -> (a -> r) -> ScopeT b t f a -> r
-- | traverse_ the bound variables in a Scope.
traverseBoundT_ :: (Applicative g, Foldable (t f)) => (b -> g d) -> ScopeT b t f a -> g ()
-- | traverse_ both the variables bound by this scope and any free
-- variables.
traverseScopeT_ :: (Applicative g, Foldable f, Foldable (t f)) => (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g ()
-- | traverse the bound variables in a Scope.
traverseBoundT :: (Applicative g, Traversable (t f)) => (b -> g c) -> ScopeT b t f a -> g (ScopeT c t f a)
-- | traverse both bound and free variables
traverseScopeT :: (Applicative g, Traversable f, Traversable (t f)) => (b -> g d) -> (a -> g c) -> ScopeT b t f a -> g (ScopeT d t f c)
-- | If you are looking for bitraverseScopeT, this is the monster
-- you need.
bitransverseScopeT :: Applicative f => (forall x x'. (x -> f x') -> t s x -> f (t' s' x')) -> (forall x x'. (x -> f x') -> s x -> f (s' x')) -> (a -> f a') -> ScopeT b t s a -> f (ScopeT b t' s' a')
instance (GHC.Base.Functor (t f), GHC.Base.Functor f) => GHC.Base.Functor (Bound.ScopeT.ScopeT b t f)
instance (Data.Foldable.Foldable (t f), Data.Foldable.Foldable f) => Data.Foldable.Foldable (Bound.ScopeT.ScopeT b t f)
instance (Data.Traversable.Traversable (t f), Data.Traversable.Traversable f) => Data.Traversable.Traversable (Bound.ScopeT.ScopeT b t f)
instance (GHC.Base.Monad f, GHC.Base.Functor (t f)) => Control.Monad.Module.Module (Bound.ScopeT.ScopeT b t f) f
instance (Data.Hashable.Class.Hashable b, Bound.Class.Bound t, GHC.Base.Monad f, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable1 (t f)) => Data.Hashable.Class.Hashable1 (Bound.ScopeT.ScopeT b t f)
instance (Data.Hashable.Class.Hashable b, Bound.Class.Bound t, GHC.Base.Monad f, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable1 (t f), Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Bound.ScopeT.ScopeT b t f a)
instance Control.DeepSeq.NFData (t f (Bound.Var.Var b (f a))) => Control.DeepSeq.NFData (Bound.ScopeT.ScopeT b t f a)
instance (GHC.Base.Monad f, Bound.Class.Bound t, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 (t f), Data.Functor.Classes.Eq1 f, GHC.Classes.Eq a) => GHC.Classes.Eq (Bound.ScopeT.ScopeT b t f a)
instance (GHC.Base.Monad f, Bound.Class.Bound t, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 (t f), Data.Functor.Classes.Ord1 f, GHC.Classes.Ord a) => GHC.Classes.Ord (Bound.ScopeT.ScopeT b t f a)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 (t f), Data.Functor.Classes.Show1 f, GHC.Show.Show a) => GHC.Show.Show (Bound.ScopeT.ScopeT b t f a)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 (t f), Data.Functor.Classes.Read1 f, GHC.Read.Read a) => GHC.Read.Read (Bound.ScopeT.ScopeT b t f a)
instance (GHC.Base.Monad f, Bound.Class.Bound t, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 (t f), Data.Functor.Classes.Eq1 f) => Data.Functor.Classes.Eq1 (Bound.ScopeT.ScopeT b t f)
instance (GHC.Base.Monad f, Bound.Class.Bound t, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 (t f), Data.Functor.Classes.Ord1 f) => Data.Functor.Classes.Ord1 (Bound.ScopeT.ScopeT b t f)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 (t f), Data.Functor.Classes.Show1 f) => Data.Functor.Classes.Show1 (Bound.ScopeT.ScopeT b t f)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 (t f), Data.Functor.Classes.Read1 f) => Data.Functor.Classes.Read1 (Bound.ScopeT.ScopeT b t f)
-- | ScopeH scope, which allows substitute f into
-- g to get new g.
--
-- Compare following signatures:
--
--
-- instantiate1 :: ... => m a -> Scope b m a -> m a
-- instantiate1H :: ... => m a -> ScopeH b f m a -> f a
--
--
-- ScopeH variant allows to encode e.g. Hindley-Milner types,
-- where we diffentiate between Poly and Mono-morphic
-- types.
--
--
-- specialise :: Poly a -> Mono a -> Poly a
-- specialise (Forall p) m = instantiate1H m p
-- specialise _ _ = error "ill-kinded"
--
--
-- Another applications are bidirectional type-systems or
-- representing normal forms with normal and neutral terms,
-- aka introduction and elimination terms.
--
-- Look into examples/ directory for System F and
-- Bidirectional STLC implemented with a help of ScopeH.
module Bound.ScopeH
-- | ScopeH b f m a is a f expression abstracted
-- over g, with bound variables in b, and free
-- variables in a.
--
--
-- Scope b f a ~ ScopeH n f f a
-- ScopeT b t f a ~ ScopeH b (t f) f a
--
newtype ScopeH b f m a
ScopeH :: f (Var b (m a)) -> ScopeH b f m a
[unscopeH] :: ScopeH b f m a -> f (Var b (m a))
-- | Capture some free variables in an expression to yield a ScopeH
-- with bound variables in b.
abstractH :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH b f m a
-- | Abstract over a single variable.
abstract1H :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH () f m a
-- | Capture some free variables in an expression to yield a ScopeH
-- with bound variables in b. Optionally change the types of the
-- remaining free variables.
abstractHEither :: (Functor f, Monad m) => (a -> Either b c) -> f a -> ScopeH b f m c
-- | Abstraction, capturing named bound variables.
abstractHName :: (Functor f, Monad m) => (a -> Maybe b) -> f a -> ScopeH (Name a b) f m a
-- | Abstract over a single variable
abstract1HName :: (Functor f, Monad m, Eq a) => a -> f a -> ScopeH (Name a ()) f m a
-- | Enter a ScopeH, instantiating all bound variables
instantiateH :: Module f m => (b -> m a) -> ScopeH b f m a -> f a
-- | Enter a ScopeH that binds one variable, instantiating it
instantiate1H :: Module f m => m a -> ScopeH b f m a -> f a
-- | Enter a ScopeH, and instantiate all bound and free variables in
-- one go.
instantiateHEither :: Module f m => (Either b a -> m c) -> ScopeH b f m a -> f c
-- | Convert to traditional de Bruijn.
fromScopeH :: Module f m => ScopeH b f m a -> f (Var b a)
-- | Convert from traditional de Bruijn to generalized de Bruijn indices.
toScopeH :: (Functor f, Monad m) => f (Var b a) -> ScopeH b f m a
-- | Convert to Scope.
lowerScopeH :: (Functor f, Functor f) => (forall x. f x -> h x) -> (forall x. m x -> h x) -> ScopeH b f m a -> Scope b h a
convertFromScope :: Scope b f a -> ScopeH b f f a
-- | Perform substitution on both bound and free variables in a
-- ScopeH.
splatH :: Module f m => (a -> m c) -> (b -> m c) -> ScopeH b f m a -> f c
-- | Return a list of occurences of the variables bound by this
-- ScopeH.
bindingsH :: Foldable f => ScopeH b f m a -> [b]
-- | Perform a change of variables on bound variables.
mapBoundH :: Functor f => (b -> b') -> ScopeH b f m a -> ScopeH b' f m a
-- | Perform a change of variables, reassigning both bound and free
-- variables.
mapScopeH :: (Functor f, Functor m) => (b -> d) -> (a -> c) -> ScopeH b f m a -> ScopeH d f m c
-- | Obtain a result by collecting information from bound variables
foldMapBoundH :: (Foldable f, Monoid r) => (b -> r) -> ScopeH b f m a -> r
-- | Obtain a result by collecting information from both bound and free
-- variables
foldMapScopeH :: (Foldable f, Foldable m, Monoid r) => (b -> r) -> (a -> r) -> ScopeH b f m a -> r
-- | traverse_ the bound variables in a Scope.
traverseBoundH_ :: (Applicative g, Foldable f) => (b -> g d) -> ScopeH b f m a -> g ()
-- | traverse_ both the variables bound by this scope and any free
-- variables.
traverseScopeH_ :: (Applicative g, Foldable f, Foldable m) => (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g ()
-- | traverse the bound variables in a Scope.
traverseBoundH :: (Applicative g, Traversable f) => (b -> g c) -> ScopeH b f m a -> g (ScopeH c f m a)
-- | traverse both bound and free variables
traverseScopeH :: (Applicative g, Traversable f, Traversable m) => (b -> g d) -> (a -> g c) -> ScopeH b f m a -> g (ScopeH d f m c)
bitraverseScopeH :: (Applicative g, Bitraversable f, Bitraversable m) => (k -> g k') -> (l -> g l') -> (a -> g a') -> ScopeH b (f k) (m l) a -> g (ScopeH b (f k') (m l') a')
bitransverseScopeH :: Applicative g => (forall x x'. (x -> g x') -> f x -> g (f' x')) -> (forall x x'. (x -> g x') -> m x -> g (m' x')) -> (a -> g a') -> ScopeH b f m a -> g (ScopeH b f' m' a')
instance (GHC.Base.Functor f, GHC.Base.Monad m) => Control.Monad.Module.Module (Bound.ScopeH.ScopeH b f m) m
instance (GHC.Base.Functor f, GHC.Base.Functor m) => GHC.Base.Functor (Bound.ScopeH.ScopeH b f m)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable m) => Data.Foldable.Foldable (Bound.ScopeH.ScopeH b f m)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable m) => Data.Traversable.Traversable (Bound.ScopeH.ScopeH b f m)
instance (Data.Hashable.Class.Hashable b, Control.Monad.Module.Module f m, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable1 m) => Data.Hashable.Class.Hashable1 (Bound.ScopeH.ScopeH b f m)
instance (Data.Hashable.Class.Hashable b, Control.Monad.Module.Module f m, Data.Hashable.Class.Hashable1 f, Data.Hashable.Class.Hashable1 m, Data.Hashable.Class.Hashable a) => Data.Hashable.Class.Hashable (Bound.ScopeH.ScopeH b f m a)
instance Control.DeepSeq.NFData (f (Bound.Var.Var b (m a))) => Control.DeepSeq.NFData (Bound.ScopeH.ScopeH b f m a)
instance (Control.Monad.Module.Module f m, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f, Data.Functor.Classes.Eq1 m, GHC.Classes.Eq a) => GHC.Classes.Eq (Bound.ScopeH.ScopeH b f m a)
instance (Control.Monad.Module.Module f m, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f, Data.Functor.Classes.Ord1 m, GHC.Classes.Ord a) => GHC.Classes.Ord (Bound.ScopeH.ScopeH b f m a)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f, Data.Functor.Classes.Show1 m, GHC.Show.Show a) => GHC.Show.Show (Bound.ScopeH.ScopeH b f m a)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f, Data.Functor.Classes.Read1 m, GHC.Read.Read a) => GHC.Read.Read (Bound.ScopeH.ScopeH b f m a)
instance (Control.Monad.Module.Module f m, GHC.Classes.Eq b, Data.Functor.Classes.Eq1 f, Data.Functor.Classes.Eq1 m) => Data.Functor.Classes.Eq1 (Bound.ScopeH.ScopeH b f m)
instance (Control.Monad.Module.Module f m, GHC.Classes.Ord b, Data.Functor.Classes.Ord1 f, Data.Functor.Classes.Ord1 m) => Data.Functor.Classes.Ord1 (Bound.ScopeH.ScopeH b f m)
instance (GHC.Show.Show b, Data.Functor.Classes.Show1 f, Data.Functor.Classes.Show1 m) => Data.Functor.Classes.Show1 (Bound.ScopeH.ScopeH b f m)
instance (GHC.Read.Read b, Data.Functor.Classes.Read1 f, Data.Functor.Classes.Read1 m) => Data.Functor.Classes.Read1 (Bound.ScopeH.ScopeH b f m)