Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- 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)
- type family BlankLeft (g :: Type -> Type) :: Type -> Type
- type family BlankRight (g :: Type -> Type) :: Type -> Type
- type family BlankInfo (g :: Type -> Type) :: Type
- type family BlankFunctor (g :: Type -> Type) :: Type -> Type
- 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)
- blankFree :: Blank g => a -> BlankRight g (g a)
- blankEmbed :: Blank g => BlankFunctor g (g a) -> BlankRight g (g a)
- blankAbstract :: (Blank g, Eq a) => BlankInfo g -> Seq a -> g a -> BlankRight g (g a)
- blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a)
- blankUnAbstract :: Blank g => Seq a -> g a -> g a
- blankUnAbstract1 :: Blank g => a -> g a -> g a
- blankInstantiate :: Blank g => Seq (BlankRight g (g a)) -> g a -> g a
- blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a
- blankApply :: Blank g => Seq (BlankRight g (g a)) -> g a -> Either SubError (g a)
- blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a)
- blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a)
- blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a)
- blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b
- blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a
- blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a)
- blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r
- blankFold :: Blank g => BlankFold g a r -> g a -> r
- blankLiftAnno :: Blank g => BlankLeft g a -> g a
- blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a
- blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b

# 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.

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

The left adjoint functor used by `g`

.

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

The right adjoint functor used by `g`

## Instances

type BlankRight (Scope n f) Source # | |

Defined in Blanks.Scope | |

type BlankRight (LocScope l n f) Source # | |

Defined in Blanks.LocScope |

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

The expression functor used by `g`

.

## Instances

type BlankFunctor (Scope n f) Source # | |

Defined in Blanks.Scope | |

type BlankFunctor (LocScope l n f) Source # | |

Defined in Blanks.LocScope |

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.

:: Blank g | |

=> a | The name of the free variable |

-> BlankRight g (g a) |

Creates a free variable in context.

:: Blank g | |

=> BlankFunctor g (g a) | An expression |

-> BlankRight g (g a) |

Embeds an expression functor in context.

:: (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.

:: 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 #

:: 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.

:: 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 #

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