-- --< Header >-- {{{

{-# LANGUAGE TypeFamilyDependencies, DataKinds, PatternSynonyms #-}


{- |

Description : Axiomata for easier use of "Data.Type.Ord"
Copyright   : (c) L. S. Leary, 2025

Axiomata for easier use of "Data.Type.Ord".

\(\newcommand{\ldot}{.\,\,}\)

-}

-- }}}

-- --< Exports >-- {{{

module Data.Type.Ord.Axiomata (

  -- * Relations
  -- $relations
  type (<),  type (==), type (>),
  type (<=), type (/=), type (>=),

  -- * Axiomata

  -- ** Equivalence
  Equivalence(..),

  -- ** Total Order
  TotalOrder(..),
  Reflect,
  minTO, maxTO,
  defaultDecideEq,

  -- ** Bounding
  BoundedBelow(..),
  BoundedAbove(..),

  -- * Miscellaneous Type Families
  Sing,
  Proof,

) where

-- }}}

-- --< Imports >-- {{{

-- GHC/base
import GHC.TypeNats
  ( Nat   , SNat   , pattern SNat   , natSing   , cmpNat
  )
import GHC.TypeLits
  (         SChar  , pattern SChar  , charSing  , cmpChar
  , Symbol, SSymbol, pattern SSymbol, symbolSing, cmpSymbol
  )

-- base
import Unsafe.Coerce (unsafeCoerce)
import Data.Kind (Type, Constraint)
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord
  (OrderingI(..), Compare, OrdCond, Min, Max, type (<=?), type (>=?))
import Data.Void (Void)

-- }}}

-- --< Relations >-- {{{

{- $relations

@'Compare' \@O@ should give rise to an equivalence relation and a total ordering on @O@.
In particular, we can define relations:

\[
\begin{align}
  a  <   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{LT} \\
  a  =   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{EQ} \\
  a  >   b &\iff \mathtt{Compare} \, a \, b \sim \mathtt{GT} \\
  a \leq b &\iff a < b \lor a = b                            \\
  a \neq b &\iff a < b \lor a > b                            \\
  a \geq b &\iff a = b \lor a > b
\end{align}
\]

These aren't consistent by construction, however—that's why we need axiomata.

N.B. We use and provide fixed versions of these relations from "Data.Type.Ord" as per [#26190](https://gitlab.haskell.org/ghc/ghc/-/issues/26190).

-}

type a <  b = Compare a b ~ LT
type a == b = Compare a b ~ EQ
type a >  b = Compare a b ~ GT
type a <= b = (a <=? b)                             ~ True
type a /= b = OrdCond (Compare a b) True False True ~ True
type a >= b = (a >=? b)                             ~ True

-- }}}

-- --< Axiomata: Equivalence >-- {{{

-- | 'Eq' for @'Sing' e@ with @'Compare' \@e@.
--   Due to the inclusion of 'sub', 'Data.Type.Ord.Lemmata.symEq' and 'Data.Type.Ord.Lemmata.transEq' are demoted to lemmata.
class Equivalence e where

  {- |

  Decidability of equivalence.

  \[
    \forall a, b \ldot
      a = b \lor a \neq b
  \]

  Since 'refl' and 'sub' make them interchangeable, however, we actually use regular type equality for better ergonomics:

  \[
    \forall a, b \ldot
      a \sim b \lor a \not\sim b
  \]

  -}
  (=?)
    :: Sing e a -> Sing e b {- ^ -}
    -> Either (a :~: b -> Void) (a :~: b)

  {- |

  Reflexivity of equivalence.

  \[
    \forall a \ldot
      a = a
  \]

  Can also be read as:

  \[
    \forall a, b \ldot
      a \sim b \implies a = b
  \]

  The other direction of 'sub'.

  -}
  refl
    :: Sing e a {- ^ -}
    -> Proof (a == a)

  {- |

  Substitutability: if two types are equivalent, one can be substituted for the other.

  \[
    \forall a, b \ldot
      a = b \implies a \sim b
  \]

  The other direction of 'refl'.

  -}
  sub
    :: a == b
    => Sing e a {- ^ -}
    -> Sing e b
    -> a :~: b

instance Equivalence Nat where
  =? :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Nat a -> Sing Nat b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Nat). Sing Nat a -> Proof (a == a)
refl Sing Nat a
_  = 'EQ :~: 'EQ
Proof (Compare a a ~ 'EQ)
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Nat) (b :: Nat).
(a == b) =>
Sing Nat a -> Sing Nat b -> a :~: b
sub m :: Sing Nat a
m@SNat a
Sing Nat a
SNat n :: Sing Nat b
n@SNat b
Sing Nat b
SNat = case SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
m SNat b
Sing Nat b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance Equivalence Char where
  =? :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Char a -> Sing Char b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Char). Sing Char a -> Proof (a == a)
refl Sing Char a
_  = 'EQ :~: 'EQ
Proof (Compare a a ~ 'EQ)
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Char) (b :: Char).
(a == b) =>
Sing Char a -> Sing Char b -> a :~: b
sub m :: Sing Char a
m@SChar a
Sing Char a
SChar n :: Sing Char b
n@SChar b
Sing Char b
SChar = case SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
m SChar b
Sing Char b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

instance Equivalence Symbol where
  =? :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a
-> Sing Symbol b -> Either ((a :~: b) -> Void) (a :~: b)
(=?) = Sing Symbol a
-> Sing Symbol b -> Either ((a :~: b) -> Void) (a :~: b)
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq
  refl :: forall (a :: Symbol). Sing Symbol a -> Proof (a == a)
refl Sing Symbol a
_  = 'EQ :~: 'EQ
Proof (Compare a a ~ 'EQ)
forall {k} (a :: k). a :~: a
Refl
  sub :: forall (a :: Symbol) (b :: Symbol).
(a == b) =>
Sing Symbol a -> Sing Symbol b -> a :~: b
sub m :: Sing Symbol a
m@SSymbol a
Sing Symbol a
SSymbol n :: Sing Symbol b
n@SSymbol b
Sing Symbol b
SSymbol = case SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
m SSymbol b
Sing Symbol b
n of
    OrderingI a b
EQI -> a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl

-- }}}

-- --< Axiomata: Total Order >-- {{{

-- | 'Ord' for @'Sing' e@ with @'Compare' \@e@.
class Equivalence o => TotalOrder o where

  {- |

  Decidable connectivity of ordering.

  \[
    \forall a, b \ldot
      a < b \lor a = b \lor a > b
  \]

  -}
  (<|=|>)
    :: Sing o a -> Sing o b {- ^ -}
    -> OrderingI a b

  {- |

  Anti-symmetry of ordering.

  \[
    \forall a, b \ldot
      a < b \iff b > a
  \]

  -}
  antiSym
    :: Sing o a -> Sing o b {- ^ -}
    -> Compare a b :~: Reflect (Compare b a)

  {- |

  Transitivity of \( \leq \).

  \[
    \forall a, b, c \ldot
      a \leq b \land b \leq c \implies a \leq c
  \]

  -}
  transLeq
    :: (a <= b, b <= c)
    => Sing o a -> Sing o b -> Sing o c {- ^ -}
    -> Proof (a <= c)

-- | @Reflect@ an 'Ordering' (to express anti-symmetry).
type family Reflect (o :: Ordering) = (p :: Ordering) | p -> o where
  Reflect LT = GT
  Reflect EQ = EQ
  Reflect GT = LT

instance TotalOrder Nat where
  m :: Sing Nat a
m@SNat a
Sing Nat a
SNat <|=|> :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> OrderingI a b
<|=|> n :: Sing Nat b
n@SNat b
Sing Nat b
SNat = SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
m SNat b
Sing Nat b
n
  antiSym :: forall (a :: Nat) (b :: Nat).
Sing Nat a -> Sing Nat b -> Compare a b :~: Reflect (Compare b a)
antiSym = SNat a -> SNat b -> Compare a b :~: Reflect (Compare b a)
Sing Nat a -> Sing Nat b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transLeq :: forall (a :: Nat) (b :: Nat) (c :: Nat).
(a <= b, b <= c) =>
Sing Nat a -> Sing Nat b -> Sing Nat c -> Proof (a <= c)
transLeq l :: Sing Nat a
l@SNat a
Sing Nat a
SNat m :: Sing Nat b
m@SNat b
Sing Nat b
SNat n :: Sing Nat c
n@SNat c
Sing Nat c
SNat = case SNat a -> SNat b -> OrderingI a b
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat a
l SNat b
Sing Nat b
m of
    OrderingI a b
LTI -> case SNat b -> SNat c -> OrderingI b c
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat b
Sing Nat b
m SNat c
Sing Nat c
n of
      OrderingI b c
LTI -> case SNat a -> SNat b -> SNat c -> Proof (a < c)
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(a < b, b < c) =>
sing a -> sing b -> sing c -> Proof (a < c)
unsafeTransLt SNat a
Sing Nat a
l SNat b
Sing Nat b
m SNat c
Sing Nat c
n of
        CmpNat a c :~: 'LT
Proof (a < c)
Refl -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SNat a -> SNat c -> OrderingI a c
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat a
Sing Nat b
m SNat c
Sing Nat c
n of
      OrderingI a c
LTI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl

instance TotalOrder Char where
  m :: Sing Char a
m@SChar a
Sing Char a
SChar <|=|> :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> OrderingI a b
<|=|> n :: Sing Char b
n@SChar b
Sing Char b
SChar = SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
m SChar b
Sing Char b
n
  antiSym :: forall (a :: Char) (b :: Char).
Sing Char a -> Sing Char b -> Compare a b :~: Reflect (Compare b a)
antiSym = SChar a -> SChar b -> Compare a b :~: Reflect (Compare b a)
Sing Char a -> Sing Char b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transLeq :: forall (a :: Char) (b :: Char) (c :: Char).
(a <= b, b <= c) =>
Sing Char a -> Sing Char b -> Sing Char c -> Proof (a <= c)
transLeq l :: Sing Char a
l@SChar a
Sing Char a
SChar m :: Sing Char b
m@SChar b
Sing Char b
SChar n :: Sing Char c
n@SChar c
Sing Char c
SChar = case SChar a -> SChar b -> OrderingI a b
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char a
l SChar b
Sing Char b
m of
    OrderingI a b
LTI -> case SChar b -> SChar c -> OrderingI b c
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar b
Sing Char b
m SChar c
Sing Char c
n of
      OrderingI b c
LTI -> case SChar a -> SChar b -> SChar c -> Proof (a < c)
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(a < b, b < c) =>
sing a -> sing b -> sing c -> Proof (a < c)
unsafeTransLt SChar a
Sing Char a
l SChar b
Sing Char b
m SChar c
Sing Char c
n of
        CmpChar a c :~: 'LT
Proof (a < c)
Refl -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SChar a -> SChar c -> OrderingI a c
forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar SChar a
Sing Char b
m SChar c
Sing Char c
n of
      OrderingI a c
LTI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl

instance TotalOrder Symbol where
  m :: Sing Symbol a
m@SSymbol a
Sing Symbol a
SSymbol <|=|> :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a -> Sing Symbol b -> OrderingI a b
<|=|> n :: Sing Symbol b
n@SSymbol b
Sing Symbol b
SSymbol = SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
m SSymbol b
Sing Symbol b
n
  antiSym :: forall (a :: Symbol) (b :: Symbol).
Sing Symbol a
-> Sing Symbol b -> Compare a b :~: Reflect (Compare b a)
antiSym = SSymbol a -> SSymbol b -> Compare a b :~: Reflect (Compare b a)
Sing Symbol a
-> Sing Symbol b -> Compare a b :~: Reflect (Compare b a)
forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym
  transLeq :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol).
(a <= b, b <= c) =>
Sing Symbol a -> Sing Symbol b -> Sing Symbol c -> Proof (a <= c)
transLeq l :: Sing Symbol a
l@SSymbol a
Sing Symbol a
SSymbol m :: Sing Symbol b
m@SSymbol b
Sing Symbol b
SSymbol n :: Sing Symbol c
n@SSymbol c
Sing Symbol c
SSymbol = case SSymbol a -> SSymbol b -> OrderingI a b
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol a
l SSymbol b
Sing Symbol b
m of
    OrderingI a b
LTI -> case SSymbol b -> SSymbol c -> OrderingI b c
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol b
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
      OrderingI b c
LTI -> case SSymbol a -> SSymbol b -> SSymbol c -> Proof (a < c)
forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(a < b, b < c) =>
sing a -> sing b -> sing c -> Proof (a < c)
unsafeTransLt SSymbol a
Sing Symbol a
l SSymbol b
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
        CmpSymbol a c :~: 'LT
Proof (a < c)
Refl -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI b c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
EQI -> case SSymbol a -> SSymbol c -> OrderingI a c
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol SSymbol a
Sing Symbol b
m SSymbol c
Sing Symbol c
n of
      OrderingI a c
LTI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl
      OrderingI a c
EQI -> 'True :~: 'True
Proof (a <= c)
forall {k} (a :: k). a :~: a
Refl

unsafeAntiSym
  :: forall o (sing :: o -> Type) (a :: o) (b :: o)
  .  sing a -> sing b
  -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym :: forall o (sing :: o -> *) (a :: o) (b :: o).
sing a -> sing b -> Compare a b :~: Reflect (Compare b a)
unsafeAntiSym !sing a
_ !sing b
_ = (Compare a b :~: Compare a b)
-> Compare a b :~: Reflect (Compare b a)
forall a b. a -> b
unsafeCoerce (forall (a :: Ordering). a :~: a
forall {k} (a :: k). a :~: a
Refl @(Compare a b))

unsafeTransLt
  :: (a < b, b < c)
  => sing a -> sing b -> sing c -> Proof (a < c)
unsafeTransLt :: forall {k} (a :: k) (b :: k) (c :: k) (sing :: k -> *).
(a < b, b < c) =>
sing a -> sing b -> sing c -> Proof (a < c)
unsafeTransLt !sing a
_ !sing b
_ !sing c
_ = ('LT :~: 'LT) -> Compare a c :~: 'LT
forall a b. a -> b
unsafeCoerce (forall (a :: Ordering). a :~: a
forall {k} (a :: k). a :~: a
Refl @LT)

-- | The minimum of two totally-ordered singletons.
minTO :: TotalOrder o => Sing o a -> Sing o b -> Sing o (Min a b)
minTO :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Min a b)
minTO Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> Sing o a
Sing o (Min a b)
a
  OrderingI a b
EQI -> Sing o a
Sing o (Min a b)
a
  OrderingI a b
GTI -> Sing o b
Sing o (Min a b)
b

-- | The maximum of two totally-ordered singletons.
maxTO :: TotalOrder o => Sing o a -> Sing o b -> Sing o (Max a b)
maxTO :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Sing o (Max a b)
maxTO Sing o a
a Sing o b
b = case Sing o a
a Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
b of
  OrderingI a b
LTI -> Sing o b
Sing o (Max a b)
b
  OrderingI a b
EQI -> Sing o b
Sing o (Max a b)
b
  OrderingI a b
GTI -> Sing o a
Sing o (Max a b)
a

-- | A default implementation of '=?' in terms of '<|=|>'.
defaultDecideEq
  :: forall o a b. TotalOrder o
  => Sing o a -> Sing o b {- ^ -}
  -> Either (a :~: b -> Void) (a :~: b)
defaultDecideEq :: forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
defaultDecideEq Sing o a
m Sing o b
n = case Sing o a -> Proof (a == a)
forall (a :: o). Sing o a -> Proof (a == a)
forall e (a :: e). Equivalence e => Sing e a -> Proof (a == a)
refl Sing o a
m of
  Compare a a :~: 'EQ
Proof (a == a)
Refl -> case Sing o a
m Sing o a -> Sing o b -> OrderingI a b
forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
forall o (a :: o) (b :: o).
TotalOrder o =>
Sing o a -> Sing o b -> OrderingI a b
<|=|> Sing o b
n of
    OrderingI a b
LTI -> ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left \case{}
    OrderingI a b
EQI -> (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    OrderingI a b
GTI -> ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left \case{}

-- }}}

-- --< Axiomata: Bounding >-- {{{

-- | 'TotalOrder's with 'LowerBound's.
class TotalOrder o => BoundedBelow o where

  type LowerBound o = (l :: o) | l -> o

  -- | Existence of a lower bound \( b_l \).
  lowerBound :: Sing o (LowerBound o)

  {- |

  \( b_l \) is the @least@ element of @o@.

  \[
    \forall a \ldot
      b_l \leq a
  \]

  -}
  least :: Sing o a -> Proof (LowerBound o <= a)

instance BoundedBelow Nat where
  type LowerBound Nat = 0
  lowerBound :: Sing Nat (LowerBound Nat)
lowerBound = SNat 0
Sing Nat (LowerBound Nat)
forall (n :: Nat). KnownNat n => SNat n
natSing
  least :: forall (a :: Nat). Sing Nat a -> Proof (LowerBound Nat <= a)
least = Sing Nat a -> Proof (LowerBound Nat <= a)
forall o (a :: o). Sing o a -> Proof (LowerBound o <= a)
unsafeLeast

instance BoundedBelow Char where
  type LowerBound Char = '\NUL'
  lowerBound :: Sing Char (LowerBound Char)
lowerBound = SChar '\NUL'
Sing Char (LowerBound Char)
forall (n :: Char). KnownChar n => SChar n
charSing
  least :: forall (a :: Char). Sing Char a -> Proof (LowerBound Char <= a)
least = Sing Char a -> Proof (LowerBound Char <= a)
forall o (a :: o). Sing o a -> Proof (LowerBound o <= a)
unsafeLeast

instance BoundedBelow Symbol where
  type LowerBound Symbol = ""
  lowerBound :: Sing Symbol (LowerBound Symbol)
lowerBound = SSymbol ""
Sing Symbol (LowerBound Symbol)
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing
  least :: forall (a :: Symbol).
Sing Symbol a -> Proof (LowerBound Symbol <= a)
least = Sing Symbol a -> Proof (LowerBound Symbol <= a)
forall o (a :: o). Sing o a -> Proof (LowerBound o <= a)
unsafeLeast

unsafeLeast :: Sing o a -> Proof (LowerBound o <= a)
unsafeLeast :: forall o (a :: o). Sing o a -> Proof (LowerBound o <= a)
unsafeLeast !Sing o a
_ = ('True :~: 'True)
-> OrdCond (Compare (LowerBound o) a) 'True 'True 'False :~: 'True
forall a b. a -> b
unsafeCoerce (forall (a :: Bool). a :~: a
forall {k} (a :: k). a :~: a
Refl @True)


-- | 'TotalOrder's with 'UpperBound's.
class TotalOrder o => BoundedAbove o where

  type UpperBound o = (u :: o) | u -> o

  -- | Existence of an upper bound \( b_u \).
  upperBound :: Sing o (UpperBound o)

  {- |

  \( b_u \) is the @greatest@ element of @o@.

  \[
    \forall a \ldot
      a \leq b_u
  \]

  -}
  greatest :: Sing o a -> Proof (a <= UpperBound o)

-- }}}

-- --< Miscellaneous Type Families >-- {{{

-- | A mapping from kinds to their corresponding singleton type constructors.
type family   Sing k      = (s :: k -> Type) | s -> k
type instance Sing Nat    = SNat
type instance Sing Char   = SChar
type instance Sing Symbol = SSymbol

-- | A mapping from equality constraints to their corresponding evidence carriers.
type family Proof (c :: Constraint) = (r :: Type) | r -> c where
  Proof (a ~ b) = a :~: b

-- }}}