compdata-0.5.2: Compositional Data Types

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

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