Data.Comp.Param.Multi.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.Param.Multi.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.

Defined in Data.Comp.Param.Multi.Show

Methods

showHD :: Cxt h f Name (K (FreshM String)) i -> FreshM String

EqHD f => EqHD (Cxt h f)

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

Defined in Data.Comp.Param.Multi.Equality

Methods

eqHD :: PEq a => Cxt h f Name a i -> Cxt h f Name a j -> FreshM Bool

OrdHD f => OrdHD (Cxt h f)

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

Defined in Data.Comp.Param.Multi.Ordering

Methods

compareHD :: POrd a => Cxt h f Name a i -> Cxt h f Name a j -> FreshM Ordering

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

Defined in Data.Comp.Param.Multi.Equality

Methods

peq :: Cxt h f Name a i -> Cxt h f Name a j -> FreshM Bool

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

Defined in Data.Comp.Param.Multi.Ordering

Methods

pcompare :: Cxt h f Name a i -> Cxt h f Name a j -> FreshM Ordering

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.

Defined in Data.Comp.Param.Multi.Equality

Methods

(==) :: Term f i -> Term f i -> Bool

(/=) :: Term f i -> Term f i -> Bool

(HDifunctor f, OrdHD f) => Ord (Term f i)

Ordering of terms.

Defined in Data.Comp.Param.Multi.Ordering

Methods

compare :: Term f i -> Term f i -> Ordering

(<) :: Term f i -> Term f i -> Bool

(<=) :: Term f i -> Term f i -> Bool

(>) :: Term f i -> Term f i -> Bool

(>=) :: Term f i -> Term f i -> Bool

max :: Term f i -> Term f i -> Term f i

min :: Term f i -> Term f i -> Term f i

(HDifunctor f, ShowHD f) => Show (Term f i)

Printing of terms.

Defined in Data.Comp.Param.Multi.Show

Methods

showsPrec :: Int -> Term f i -> ShowS

show :: Term f i -> String

showList :: [Term f i] -> ShowS

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

Minimal complete definition

termM

Methods

termM :: (forall a. m (Trm f a i)) -> m (Term f i)

Instances

ParamFunctor []

Defined in Data.Comp.Param.Multi.Term

Methods

termM :: (forall (a :: * -> *). [Trm f a i]) -> [Term f i]

ParamFunctor Maybe

Defined in Data.Comp.Param.Multi.Term

Methods

termM :: (forall (a :: * -> *). Maybe (Trm f a i)) -> Maybe (Term f i)

ParamFunctor (Either a)

Defined in Data.Comp.Param.Multi.Term

Methods

termM :: (forall (a0 :: * -> *). Either a (Trm f a0 i)) -> Either a (Term f i)