Data.Comp.Term

This module defines the central notion of terms and its generalisation to contexts.

Documentation

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

This data type represents contexts over a signature. Contexts are terms containing zero or more holes. The first type parameter is supposed to be one of the phantom types Hole and NoHole. The second parameter is the signature of the context. The third parameter is the type of the holes.

Constructors

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

Hole :: a -> Cxt Hole f a

Instances

Functor f => Monad (Context f)

Functor f => Applicative (Context f)

Functor f => Functor (Cxt h f)

Foldable f => Foldable (Cxt h f)

Traversable f => Traversable (Cxt h f)

data Hole

Phantom type that signals that a Cxt might contain holes.

Instances

Functor f => Monad (Context f)

Functor f => Applicative (Context f)

data NoHole

Phantom type that signals that a Cxt does not contain holes.

type Context = Cxt Hole

type Term f = Cxt NoHole f ()

A term is a context with no holes.

type PTerm f = forall h a. Cxt h f a

Polymorphic definition of a term. This formulation is more natural than Term, it leads to impredicative types in some cases, though.

type Const f = f ()

unTerm :: Cxt NoHole f a -> f (Cxt NoHole f a)

This function unravels the given term at the topmost layer.

simpCxt :: Functor f => f a -> Context f a

Convert a functorial value into a context.

toCxt :: Functor f => Term f -> Cxt h f a

Cast a term over a signature to a context over the same signature.

constTerm :: Functor 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 functor f.