Blanks.Interface

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)

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)

Defined in Blanks.Scope

Functor f => Blank (LocScope l n f)

Defined in Blanks.LocScope

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

The left adjoint functor used by g.

Instances

type BlankLeft (Scope n f)

Defined in Blanks.Scope

type BlankLeft (Scope n f) = Identity

type BlankLeft (LocScope l n f)

Defined in Blanks.LocScope

type BlankLeft (LocScope l n f) = Located l

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

The right adjoint functor used by g

Instances

type BlankRight (Scope n f)

Defined in Blanks.Scope

type BlankRight (Scope n f) = Identity

type BlankRight (LocScope l n f)

Defined in Blanks.LocScope

type BlankRight (LocScope l n f) = Colocated l

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

The binder info used by g.

Instances

type BlankInfo (Scope n f)

Defined in Blanks.Scope

type BlankInfo (Scope n f) = n

type BlankInfo (LocScope l n f)

Defined in Blanks.LocScope

type BlankInfo (LocScope l n f) = n

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

The expression functor used by g.

Instances

type BlankFunctor (Scope n f)

Defined in Blanks.Scope

type BlankFunctor (Scope n f) = f

type BlankFunctor (LocScope l n f)

Defined 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

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

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

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

blankFree

Arguments

:: Blank g

=> a

The name of the free variable

-> BlankRight g (g a)

Creates a free variable in context.

blankEmbed

Arguments

:: Blank g

=> BlankFunctor g (g a)

An expression

-> BlankRight g (g a)

Embeds an expression functor in context.

blankAbstract

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)

blankAbstract for a single argument.

blankUnAbstract

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

blankInstantiate

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

blankInstantiate for a single argument.

blankApply

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)

blankApply for a single argument.

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

A ThrowSub version of blankApply.

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

A ThrowSub version of blankApply1.

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

Substitution as a kind of monadic bind.

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

Optional substitution as another kind of monadic bind.

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

Lift an expression functor into the scope functor.

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

Pattern match all cases of the scope functor.

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

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

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

Lift a value of your left adjoint functor (annotating the tree) into your scope functor.

blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a

Apply a natural transformation to your left adjoint functor (annotating the tree) to change scope functors.

blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b

Apply a function to the free variables in scope in the context of the left adjoint functor. (Allows you to read annotations when fmapping.)