compdata-0.5.2: Compositional Data Types

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

Data.Comp.Param.Term

Description

This module defines the central notion of parametrised 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

In :: f a (Cxt h f a b) -> Cxt h f a b 
Hole :: b -> Cxt Hole f a b 
Var :: a -> Cxt h f a b 

Instances

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.

(Difunctor f, 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 Name a) 
(OrdD f, POrd a) => POrd (Cxt h f Name a) 

data Hole Source

Phantom type used to define Context.

data NoHole Source

Phantom type used to define Term.

newtype Term f Source

A term is a context with no holes, where all occurrences of the contravariant parameter is fully parametric.

Constructors

Term 

Fields

unTerm :: forall a. Trm f a
 

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.

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

"Preterms"

type Context = Cxt HoleSource

A context may contain holes.

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

Convert a difunctorial value into a context.

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

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

Methods

termM :: (forall a. m (Trm f a)) -> m (Term f)Source