{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UnicodeSyntax #-}

module Data.Congruence.Decidable where

import Data.Array
import Data.Int
import Data.Map
import Data.Sequence
import Data.Set
import Data.Tree
import Data.Word

-- | 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.
--
class Eq α ⇒ Congruence α where

instance Congruence α ⇒ Congruence [α]
instance Congruence α ⇒ Congruence (Maybe α)
instance (Congruence α, Congruence β) ⇒ Congruence (Either α β)

instance Congruence α ⇒ Congruence (Set α)
instance Congruence α ⇒ Congruence (Seq α)
instance Congruence α ⇒ Congruence (Tree α)
instance (Congruence α, Congruence β) ⇒ Congruence (Map α β)
instance (Ix i, Congruence i, Congruence α) ⇒ Congruence (Array i α)

instance Congruence ()
instance Congruence Bool
instance Congruence Char
instance Congruence Int
instance Congruence Int16
instance Congruence Int32
instance Congruence Int64
instance Congruence Int8
instance Congruence Integer
instance Congruence Ordering
instance Congruence Word
instance Congruence Word16
instance Congruence Word32
instance Congruence Word64
instance Congruence Word8

instance (Congruence a, Congruence b, Congruence c, Congruence d) ⇒ Congruence (a, b, c, d)
instance (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e) ⇒ Congruence (a, b, c, d, e)
instance (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f) ⇒ Congruence (a, b, c, d, e, f)
instance (Congruence a, Congruence b, Congruence c, Congruence d, Congruence e, Congruence f, Congruence g) ⇒ Congruence (a, b, c, d, e, f, g)
instance (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)
instance (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)
instance (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)
instance (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)
instance (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)
instance (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)
instance (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)
instance (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)