Portability | non-portable (GHC Extensions) |
---|---|
Stability | experimental |
Maintainer | Tom Hvitved <hvitved@diku.dk> |
This module defines the central notion of parametrized terms and their generalisation to parametrised contexts.
- data Cxt where
- data Hole
- data NoHole
- data Any
- type Term f = Trm f Any
- type Trm f a = Cxt NoHole f a ()
- type Context = Cxt Hole
- type Const f = f Any ()
- simpCxt :: Difunctor f => f a b -> Cxt Hole f a b
- coerceCxt :: Cxt h f Any b -> forall a. Cxt h f a b
- toCxt :: Difunctor f => Trm f a -> Cxt h f a b
- constTerm :: Difunctor f => Const f -> Term f
- fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'
- disequenceCxt :: Ditraversable f m a => Cxt h f a (m b) -> m (Cxt h f a b)
- dimapMCxt :: Ditraversable f m a => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')
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.Param.Difunctor. The third parameter is the type of parameters, and the fourth parameter is the type of holes.
(Difunctor f, EqD f) => Eq (Term f) | Equality on terms. |
(Difunctor f, OrdD f) => Ord (Term f) | Ordering of terms. |
(Difunctor f, ShowD f) => Show (Term f) | Printing of terms. |
EqD f => EqD (Cxt h f) | From an |
OrdD f => OrdD (Cxt h f) | From an |
ShowD f => ShowD (Cxt h f) | From an |
(EqD f, PEq a) => PEq (Cxt h f Var a) | |
(OrdD f, POrd a) => POrd (Cxt h f Var a) | |
(ShowD f, PShow a) => PShow (Cxt h f Var a) |
Phantom type used to define Term
.
The empty data type Any
is used to emulate parametricity
("poor mans parametricity").
Ditraversable (->) [] Any | |
Ditraversable (->) Maybe Any | Functions of the type |
Ditraversable (->) (Either e) Any | |
Ditraversable (->) m Any => Ditraversable (->) (ListT m) Any | |
(Error e, Ditraversable (->) m Any) => Ditraversable (->) (ErrorT e m) Any | |
Ditraversable (->) m Any => Ditraversable (->) (StateT s m) Any | |
(Monoid w, Ditraversable (->) m Any) => Ditraversable (->) (WriterT w m) Any | |
(Monoid w, Ditraversable (->) m Any) => Ditraversable (->) (RWST r w s m) Any | |
(Difunctor f, EqD f) => Eq (Term f) | Equality on terms. |
(Difunctor f, OrdD f) => Ord (Term f) | Ordering of terms. |
(Difunctor f, ShowD f) => Show (Term f) | Printing of terms. |
A term is a context with no holes, where all occurrences of the
contravariant parameter is fully parametric. Parametricity is "emulated"
using the empty type Any
, e.g. a function of type Any -> T[Any]
is
equivalent with forall b. b -> T[b]
, but the former avoids the impredicative
typing extension, and works also in the cases where the codomain type is not a
type constructor, e.g. Any -> (Any,Any)
.
A context may contain holes, but must be parametric in the bound
parameters. Parametricity is "emulated" using the empty type Any
, e.g. a
function of type Any -> T[Any]
is equivalent with forall b. b -> T[b]
,
but the former avoids the impredicative typing extension, and works also in
the cases where the codomain type is not a type constructor, e.g.
Any -> (Any,Any)
.
coerceCxt :: Cxt h f Any b -> forall a. Cxt h f a bSource
Cast a "pseudo-parametric" context over a signature to a parametric
context over the same signature. The usage of unsafeCoerce
is safe, because
the empty type Any
witnesses that all uses of the contravariant argument are
parametric.
constTerm :: Difunctor f => Const f -> Term fSource
This function converts a constant to a term. This assumes that the
argument is indeed a constant, i.e. does not have a value for the
argument type of the difunctor f
.
disequenceCxt :: Ditraversable f m a => Cxt h f a (m b) -> m (Cxt h f a b)Source
This is an instance of disequence
for Cxt
.