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

Term :: f a (Cxt h f a b) i -> Cxt h f a b i

Hole :: b i -> Cxt Hole f a b i

Place :: a i -> Cxt h f a b 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.

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.

(ShowHD f, PShow a) => PShow (Cxt h f Var a)

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

(EqHD f, PEq a) => PEq (Cxt h f Var a)

(OrdHD f, POrd a) => POrd (Cxt h f Var a)

data Hole

Phantom type used to define Context.

data NoHole

Phantom type used to define Term.

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.

data Any

The empty data type Any is used to emulate parametricity ("poor mans parametricity").

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 Term f = Trm f Any

A term is a context with no holes, where all occurrences of the contravariant parameter is fully parametric. Parametricity is "emulated" using the empty functor Any, e.g. a function of type Any :-> T[Any] is equivalent with forall b. b :-> T[b], but the former avoids the impredicative typing extension, and works also in the cases where the codomain type is not a type constructor, e.g. Any i -> (Any i,Any i).

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

type Context = Cxt Hole

A context may contain holes, but must be parametric in the bound parameters. Parametricity is "emulated" using the empty functor Any, e.g. a function of type Any :-> T[Any] is equivalent with forall b. b :-> T[b], but the former avoids the impredicative typing extension, and works also in the cases where the codomain type is not a type constructor, e.g. Any i -> (Any i,Any i).

type Const f i = f Any (K ()) i

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

Convert a difunctorial value into a context.

coerceCxt :: Cxt h f Any b i -> forall a. Cxt h f a b i

Cast a "pseudo-parametric" context over a signature to a parametric context over the same signature. The usage of unsafeCoerce is safe, because the empty functor Any witnesses that all uses of the contravariant argument are parametric.

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

constTerm :: HDifunctor f => Const f :-> Term f

This function converts a constant to a term. This assumes that the argument is indeed a constant, i.e. does not have a value for the argument type of the higher-order difunctor f.

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 m a => NatM m b b' -> NatM m (Cxt h f a b) (Cxt h f a b')

This is an instance of hdimapM for Cxt.