Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Tom Hvitved <hvitved@diku.dk> |
Safe Haskell | None |
This module defines the central notion of generalised parametrised terms and their generalisation to generalised parametrised contexts.
- data Cxt where
- data Hole
- data NoHole
- newtype Term f i = Term {}
- type Trm f a = Cxt NoHole f a (K ())
- type Context = Cxt Hole
- simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a b
- toCxt :: HDifunctor f => Trm f a :-> Cxt h f a b
- hfmapCxt :: forall h f a b b'. HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'
- hdimapMCxt :: forall h f a b b' m. (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')
- class ParamFunctor m where
Documentation
This data type represents contexts over a signature. Contexts are terms containing zero or more holes, and zero or more parameters. The first parameter is a phantom type indicating whether the context has holes. The second paramater is the signature of the context, in the form of a Data.Comp.MultiParam.HDifunctor. The third parameter is the type of parameters, the fourth parameter is the type of holes, and the fifth parameter is the GADT type.
In :: f a (Cxt h f a b) i -> Cxt h f a b i | |
Hole :: b i -> Cxt Hole f a b i | |
Var :: a i -> Cxt h f a b i |
(HDifunctor f, ShowHD f) => ShowHD (Cxt h f) | From an |
EqHD f => EqHD (Cxt h f) | From an |
OrdHD f => OrdHD (Cxt h f) | From an |
(EqHD f, PEq a) => PEq (Cxt h f Name a) | |
(OrdHD f, POrd a) => POrd (Cxt h f Name a) |
A term is a context with no holes, where all occurrences of the contravariant parameter is fully parametric.
(HDifunctor f, EqHD f) => Eq (Term f i) | Equality on terms. |
(HDifunctor f, OrdHD f) => Ord (Term f i) | Ordering of terms. |
(HDifunctor f, ShowHD f) => Show (Term f i) | Printing of terms. |
simpCxt :: HDifunctor f => f a b :-> Cxt Hole f a bSource
Convert a difunctorial value into a context.
hdimapMCxt :: forall h f a b b' m. (HDitraversable f, Monad m) => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')Source
class ParamFunctor m whereSource
Monads for which embedded Trm
values, which are parametric at top level,
can be made into monadic Term
values, i.e. "pushing the parametricity
inwards".