compdata- Compositional Data Types

Copyright(c) 2011 Patrick Bahr
MaintainerPatrick Bahr <>
Portabilitynon-portable (GHC Extensions)
Safe HaskellNone



This module defines the central notion of mutual recursive (or, higher-order) terms and its generalisation to (higher-order) contexts. All definitions are generalised versions of those in Data.Comp.Term.



data Cxt h f a i where Source

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 family of the holes. The last parameter is the index/label.


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


HFunctor f => HFunctor (Cxt h f) 
HFoldable f => HFoldable (Cxt h f) 
HTraversable f => HTraversable (Cxt h f) 
(ShowHF f, HFunctor f) => ShowHF (Cxt h f) 
EqHF f => EqHF (Cxt h f) 
(HFunctor f, OrdHF f) => OrdHF (Cxt h f)

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

(ShowHF f, HFunctor f, KShow a) => KShow (Cxt h f a) 
(EqHF f, KEq a) => KEq (Cxt h f a) 
(HFunctor f, OrdHF f, KOrd a) => KOrd (Cxt h f a) 
(EqHF f, KEq a) => Eq (Cxt h f a i)

From an EqF functor an Eq instance of the corresponding term type can be derived.

(HFunctor f, OrdHF f, KOrd a) => Ord (Cxt h f a i)

Ordering of terms.

KShow (Cxt h f a) => Show (Cxt h f a i) 

data Hole Source

Phantom type that signals that a Cxt might contain holes.

data NoHole Source

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

type Context = Cxt Hole Source

A context might contain holes.

type Term f = Cxt NoHole f (K ()) Source

A (higher-order) term is a context with no holes.

type Const f = f (K ()) Source

constTerm :: HFunctor f => Const f :-> Term f Source

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.

unTerm :: Term f t -> f (Term f) t Source

This function unravels the given term at the topmost layer.

toCxt :: HFunctor f => Term f :-> Context f a Source

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

simpCxt :: HFunctor f => f a i -> Context f a i Source