Data.Comp.Param.Term

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

Phantom type used to define Context.

data NoHole

Phantom type used to define Term.

newtype Term f

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

"Preterms"

type Context = Cxt Hole

A context may contain holes.

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

Convert a difunctorial value into a context.

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

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

Instances

ParamFunctor []

ParamFunctor Maybe

ParamFunctor (Either a)