Data.Comp.Equality

This module defines equality for signatures, which lifts to equality for terms and contexts.

Documentation

class EqF f where

Signature equality. An instance EqF f gives rise to an instance Eq (Term f).

Methods

eqF :: Eq a => f a -> f a -> Bool

Instances

EqF []

EqF Maybe

Eq a[12] => EqF ((,) a[12])

(Eq a[12], Eq b[13]) => EqF ((,,) a[12] b[13])

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

EqF is propagated through sums.

EqF f => EqF (Cxt h f)

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

(Eq a[12], Eq b[13], Eq c[14]) => EqF ((,,,) a[12] b[13] c[14])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15]) => EqF ((,,,,) a[12] b[13] c[14] d[15])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16]) => EqF ((,,,,,) a[12] b[13] c[14] d[15] e[16])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17]) => EqF ((,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18]) => EqF ((,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19]) => EqF ((,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19])

(Eq a[12], Eq b[13], Eq c[14], Eq d[15], Eq e[16], Eq f[17], Eq g[18], Eq h[19], Eq i[1a]) => EqF ((,,,,,,,,,) a[12] b[13] c[14] d[15] e[16] f[17] g[18] h[19] i[1a])

eqMod :: (EqF f, Functor f, Foldable f) => f a -> f b -> Maybe [(a, b)]

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.