Data.Comp.MultiParam.Term

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

Documentation

data Cxt :: * -> ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> (* -> *) -> * -> * where

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

Phantom type used to define Context.

data NoHole

Phantom type used to define Term.

newtype Term f i

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

"Preterms" |

type Context = Cxt Hole

A context may contain holes.

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

Convert a difunctorial value into a context.

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

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

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

This is an instance of hdimapM for Cxt.

class ParamFunctor m where

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)

Instances

ParamFunctor []

ParamFunctor Maybe

ParamFunctor (Either a)