compdata-0.4.1: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
MaintainerPatrick Bahr <>



This module defines equality for (higher-order) signatures, which lifts to equality for (higher-order) terms and contexts. All definitions are generalised versions of those in Data.Comp.Equality.



class HEqF f whereSource

Signature equality. An instance HEqF f gives rise to an instance KEq (HTerm f).


heqF :: KEq g => f g i -> f g j -> BoolSource


HEqF f => HEqF (Cxt h f)

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

(HEqF f, HEqF g) => HEqF (:+: f g)

EqF is propagated through sums.

class KEq f whereSource


keq :: f i -> f j -> BoolSource


KEq Nothing 
Eq a => KEq (K a) 
(HEqF f, KEq a) => KEq (Cxt h f a) 

heqMod :: (HEqF f, HFunctor f, HFoldable f) => f a i -> f b i -> Maybe [(A a, A b)]Source

This function implements equality of values of type f a modulo the equality of a itself. If two functorial values are equal in this sense, eqMod returns a Just value containing a list of pairs consisting of corresponding components of the two functorial values.