compdata-0.1: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
MaintainerPatrick Bahr <>



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 HCxt h f a i whereSource

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 HHole and HNoHole. 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.


HTerm :: f (HCxt h f a) i -> HCxt h f a i 
HHole :: a i -> HCxt HHole f a i 


(Ord v, HasVars f v, HFunctor f) => SubstVars v (HCxt h f a) (HCxt h f a) 
HFunctor f => HFunctor (HCxt h f) 
HEqF f => HEqF (HCxt h f)

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

(HShowF f, HFunctor f) => HShowF (HCxt h f) 
HasVars f v => HasVars (HCxt h f) v 
(HEqF f, KEq a) => KEq (HCxt h f a) 
(HShowF f, HFunctor f, KShow a) => KShow (HCxt h f a) 

data HHole Source

Phantom type that signals that a HCxt might contain holes.

data HNoHole Source

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

type HContext = HCxt HHoleSource

A context might contain holes.

data HNothing Source

Phantom type family used to define HTerm.

type HTerm f = HCxt HNoHole f HNothingSource

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

type HConst f = f (K ())Source

constHTerm :: HFunctor f => HConst f :-> HTerm fSource

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.

unHTerm :: HTerm f t -> f (HTerm f) tSource

This function unravels the given term at the topmost layer.

toHCxt :: HTerm f i -> HContext f a iSource

simpHCxt :: HFunctor f => f a i -> HContext f a iSource