congruence-relation-0.1.0.0: Decidable congruence relations for Haskell: up to you whether this is a joke

Data.Congruence.Decidable

Synopsis

# Documentation

class Eq α => Congruence α Source

We define a congruence relation to be an equivalence relation which satisfies the following functionality law for for `α,β ∷ *`, `m,n ∷ α` and `f ∷ α → β`:

` `Congruence` α, `Eq` β, (m == n) true ⊢ (f m == f n) true`

One way to look at the `Congruence` class is through the lens of setoids; then it classifies those types for whom "being the domain of an operation" and being the "domain of a function" are synonymous. Another way to look at it is in the following sense: `Congruence α` forces all functions out of `α` to be extensional.

But usually, when developing setoids, you have a separate type of functions which respect value equivalence, and then every function has a proof obligation; then the raw functions of the outer theory are "operations" until they can be shown to be functional. This is tractable in type theory, but in Haskell and ML, it is not: when we can, it is better to rely upon data abstraction and composition to enforce our laws for us, so that proofs come for free.

Instances

 Congruence Bool Congruence Char Congruence Int Congruence Int8 Congruence Int16 Congruence Int32 Congruence Int64 Congruence Integer Congruence Ordering Congruence Word Congruence Word8 Congruence Word16 Congruence Word32 Congruence Word64 Congruence () Congruence α => Congruence [α] Congruence α => Congruence (Maybe α) Congruence α => Congruence (Set α) Congruence α => Congruence (Tree α) Congruence α => Congruence (Seq α) (Congruence α, Congruence β) => Congruence (Either α β) (Ix i, Congruence i, Congruence α) => Congruence (Array i α) (Congruence α, Congruence β) => Congruence (Map α β) (Congruence a, Congruence b, Congruence c, Congruence d) => Congruence (a, b, c, d) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e) => Congruence (a, b, c, d, e) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f) => Congruence (a, b, c, d, e, f) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g) => Congruence (a, b, c, d, e, f, g) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h) => Congruence (a, b, c, d, e, f, g, h) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i) => Congruence (a, b, c, d, e, f, g, h, i) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j) => Congruence (a, b, c, d, e, f, g, h, i, j) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j, Congruence k) => Congruence (a, b, c, d, e, f, g, h, i, j, k) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j, Congruence k, Congruence l) => Congruence (a, b, c, d, e, f, g, h, i, j, k, l) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j, Congruence k, Congruence l, Congruence m) => Congruence (a, b, c, d, e, f, g, h, i, j, k, l, m) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j, Congruence k, Congruence l, Congruence m, Congruence n) => Congruence (a, b, c, d, e, f, g, h, i, j, k, l, m, n) (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g, Congruence h, Congruence i, Congruence j, Congruence k, Congruence l, Congruence m, Congruence n, Congruence o) => Congruence (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)