blanks-0.4.1: Fill-in-the-blanks - A library factoring out substitution from ASTs

Blanks.Interface

Synopsis

Documentation

class (Adjunction (BlankLeft g) (BlankRight g), Applicative (BlankRight g), Functor (BlankFunctor g), NatNewtype (ScopeW (BlankLeft g) (BlankInfo g) (BlankFunctor g) g) g) => Blank (g :: Type -> Type) Source #

Indicates that g is a "scope" functor we can use for name-binding. (Behind-the-scenes, g must be a newtype wrapper over the ScopeW datatype.) Most of the time you will use Scope or LocScope directly, which are instances of this class.

We use the pair of adjoint functors indexed by g to shift the burden of operating in context where it is more convenient. For example, LocScope uses a pair of functors that are essentially Env and Reader. The left adjoint Env lets us annotate every level of our expression tree with a location, and the right adjoint Reader informs us of that location so we don't have to make one up out of thin air!

Scope uses the pair of functors Identity and Identity, which means there is no ability to store any additional information in the tree, but there's also no additional burden to provide that information.

Instances
 Functor f => Blank (Scope n f) Source # Instance detailsDefined in Blanks.Scope Functor f => Blank (LocScope l n f) Source # Instance detailsDefined in Blanks.LocScope

type family BlankLeft (g :: Type -> Type) :: Type -> Type Source #

The left adjoint functor used by g.

Instances
 type BlankLeft (Scope n f) Source # Instance detailsDefined in Blanks.Scope type BlankLeft (Scope n f) = Identity type BlankLeft (LocScope l n f) Source # Instance detailsDefined in Blanks.LocScope type BlankLeft (LocScope l n f) = Located l

type family BlankRight (g :: Type -> Type) :: Type -> Type Source #

The right adjoint functor used by g

Instances
 type BlankRight (Scope n f) Source # Instance detailsDefined in Blanks.Scope type BlankRight (Scope n f) = Identity type BlankRight (LocScope l n f) Source # Instance detailsDefined in Blanks.LocScope type BlankRight (LocScope l n f) = Colocated l

type family BlankInfo (g :: Type -> Type) :: Type Source #

The binder info used by g.

Instances
 type BlankInfo (Scope n f) Source # Instance detailsDefined in Blanks.Scope type BlankInfo (Scope n f) = n type BlankInfo (LocScope l n f) Source # Instance detailsDefined in Blanks.LocScope type BlankInfo (LocScope l n f) = n

type family BlankFunctor (g :: Type -> Type) :: Type -> Type Source #

The expression functor used by g.

Instances
 type BlankFunctor (Scope n f) Source # Instance detailsDefined in Blanks.Scope type BlankFunctor (Scope n f) = f type BlankFunctor (LocScope l n f) Source # Instance detailsDefined in Blanks.LocScope type BlankFunctor (LocScope l n f) = f

type BlankRawFold (g :: Type -> Type) (a :: Type) (r :: Type) = UnderScopeFold (BlankInfo g) (BlankFunctor g) (g a) a r Source #

type BlankFold (g :: Type -> Type) (a :: Type) (r :: Type) = BlankRawFold g a (BlankRight g r) Source #

type BlankPair g h = (Blank g, Blank h, BlankInfo g ~ BlankInfo h, BlankFunctor g ~ BlankFunctor h) Source #

A pair of Blank functors that index the same info and embedded functors. Used to change adjoint functors.

Arguments

 :: Blank g => a The name of the free variable -> BlankRight g (g a)

Creates a free variable in context.

Arguments

 :: Blank g => BlankFunctor g (g a) An expression -> BlankRight g (g a)

Embeds an expression functor in context.

Arguments

 :: (Blank g, Eq a) => BlankInfo g Annotation specific to your expression functor. Might contain original variable names and types, or might mark this as a "let" vs a "lambda". -> Seq a Free variables to bind, like the names of function parameters -> g a The expression to bind in, like the body of a function -> BlankRight g (g a)

Binds free variables in an expression and returns a binder.

blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a) Source #

blankAbstract for a single argument.

Arguments

 :: Blank g => Seq a The names of the variables you're freeing -> g a The expression to substitutue in (typically a binder) -> g a

Un-bind free variables in an expression. Basically the inverse of blankAbstract. Take care to match the arity of the binder! (blankApply is safer.)

blankUnAbstract1 :: Blank g => a -> g a -> g a Source #

Arguments

 :: Blank g => Seq (BlankRight g (g a)) Expressions to substitute in place of bound vars -> g a The expression to substitute in (typically a binder) -> g a

Instantiate the bound variables in an expression with other expressions. Take care to match the arity of the binder! (blankApply is safer.)

blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a Source #

blankInstantiate for a single argument.

Arguments

 :: Blank g => Seq (BlankRight g (g a)) Expressions to substitute in place of bound vars -> g a The binder expression to substitute in -> Either SubError (g a)

Instantiates the bound variables in an expression with other expressions. Throws errors on mismatched arity, non binder expression, unbound vars, etc. A version of blankInstantiate that fails loudly instead of silently!

blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a) Source #

blankApply for a single argument.

blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a) Source #

A ThrowSub version of blankApply.

blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a) Source #

A ThrowSub version of blankApply1.

blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b Source #

Substitution as a kind of monadic bind.

blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a Source #

Optional substitution as another kind of monadic bind.

blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a) Source #

Lift an expression functor into the scope functor.

blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r Source #

Pattern match all cases of the scope functor.

blankFold :: Blank g => BlankFold g a r -> g a -> r Source #

Pattern match all cases of the scope functor, and eliminate the adjoints.

blankLiftAnno :: Blank g => BlankLeft g a -> g a Source #