compdata-0.5: Compositional Data Types

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

Data.Comp.MultiParam.Term

Description

This module defines the central notion of generalised parametrised terms and their generalisation to generalised 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.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.

Constructors

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 

Instances

(HDifunctor f, ShowHD f) => ShowHD (Cxt h f)

From an ShowHD higher-order difunctor an ShowHD instance of the corresponding term type can be derived.

EqHD f => EqHD (Cxt h f)

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

OrdHD f => OrdHD (Cxt h f)

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

(EqHD f, PEq a) => PEq (Cxt h f Name a) 
(OrdHD 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 i 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 i
 

Instances

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

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

"Preterms" |

type Context = Cxt HoleSource

A context may contain holes.

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

Convert a difunctorial value into a context.

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

hfmapCxt :: forall h f a b b'. HDifunctor f => (b :-> b') -> Cxt h f a b :-> Cxt h f a b'Source

This is an instance of hfmap for Cxt.

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

This is an instance of hdimapM for Cxt.

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 i)) -> m (Term f i)Source