Data.Congruence.Decidable

Documentation

class Eq α => Congruence α

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)