compdata-0.3: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerTom Hvitved <hvitved@diku.dk>

Data.Comp.Param.Term

Description

This module defines the central notion of parametrized terms and their generalisation to parametrised contexts.

Synopsis

Documentation

data Cxt whereSource

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.

Constructors

Term :: f a (Cxt h f a b) -> Cxt h f a b 
Hole :: b -> Cxt Hole f a b 
Place :: a -> Cxt h f a b 

Instances

(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 EqD difunctor an Eq instance of the corresponding term type can be derived.

OrdD f => OrdD (Cxt h f)

From an OrdD difunctor an Ord instance of the corresponding term type can be derived.

ShowD f => ShowD (Cxt h f)

From an ShowD difunctor an ShowD instance of the corresponding term type can be derived.

(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) 

data Hole Source

Phantom type used to define Context.

data NoHole Source

Phantom type used to define Term.

Instances

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

data Any Source

The empty data type Any is used to emulate parametricity ("poor mans parametricity").

Instances

Ditraversable (->) [] Any 
Ditraversable (->) Maybe Any

Functions of the type Any -> Maybe a can be turned into functions of type Maybe (Any -> a). The empty type Any ensures that the function is parametric in the input, and hence the Maybe monad can be pulled out.

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.

type Term f = Trm f AnySource

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

type Trm f a = Cxt NoHole f a ()Source

type Context = Cxt HoleSource

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

type Const f = f Any ()Source

simpCxt :: Difunctor f => f a b -> Cxt Hole f a bSource

Convert a difunctorial value into a context.

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.

toCxt :: Difunctor f => Trm f a -> Cxt h f a bSource

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.

fmapCxt :: Difunctor f => (b -> b') -> Cxt h f a b -> Cxt h f a b'Source

This is an instance of fmap for Cxt.

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.

dimapMCxt :: Ditraversable f m a => (b -> m b') -> Cxt h f a b -> m (Cxt h f a b')Source

This is an instance of dimamM for Cxt.