Copyright	(c) L. S. Leary 2025
Safe Haskell	None
Language	Haskell2010

Data.Type.Ord.Axiomata

Contents

Relations
Axiomata
Miscellaneous Type Families

Description

Axiomata for easier use of Data.Type.Ord.

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

Synopsis

type (<) (a :: k) (b :: k) = Compare a b ~ 'LT
type (==) (a :: k) (b :: k) = Compare a b ~ 'EQ
type (>) (a :: k) (b :: k) = Compare a b ~ 'GT
type (<=) (a :: k) (b :: k) = (a <=? b) ~ 'True
type (/=) (a :: k) (b :: k) = OrdCond (Compare a b) 'True 'False 'True ~ 'True
type (>=) (a :: k) (b :: k) = (a >=? b) ~ 'True
class Equivalence e where
- (=?) :: forall (a :: e) (b :: e). Sing e a -> Sing e b -> Either ((a :~: b) -> Void) (a :~: b)
- refl :: forall (a :: e). Sing e a -> Proof (a == a)
- sub :: forall (a :: e) (b :: e). a == b => Sing e a -> Sing e b -> a :~: b
class Equivalence o => TotalOrder o where
- (<|=|>) :: forall (a :: o) (b :: o). Sing o a -> Sing o b -> OrderingI a b
- antiSym :: forall (a :: o) (b :: o). Sing o a -> Sing o b -> Compare a b :~: Reflect (Compare b a)
- transLeq :: forall (a :: o) (b :: o) (c :: o). (a <= b, b <= c) => Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
type family Reflect (o :: Ordering) = (p :: Ordering) | p -> o where ...
minTO :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Sing o (Min a b)
maxTO :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Sing o (Max a b)
defaultDecideEq :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Either ((a :~: b) -> Void) (a :~: b)
class TotalOrder o => BoundedBelow o where
- type LowerBound o = (l :: o) | l -> o
- lowerBound :: Sing o (LowerBound o)
- least :: forall (a :: o). Sing o a -> Proof (LowerBound o <= a)
class TotalOrder o => BoundedAbove o where
- type UpperBound o = (u :: o) | u -> o
- upperBound :: Sing o (UpperBound o)
- greatest :: forall (a :: o). Sing o a -> Proof (a <= UpperBound o)
type family Sing k = (s :: k -> Type) | s -> k
type family Proof c = (r :: Type) | r -> c where ...

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.

type (<) (a :: k) (b :: k) = Compare a b ~ 'LT Source #

type (==) (a :: k) (b :: k) = Compare a b ~ 'EQ Source #

type (>) (a :: k) (b :: k) = Compare a b ~ 'GT Source #

type (<=) (a :: k) (b :: k) = (a <=? b) ~ 'True Source #

type (/=) (a :: k) (b :: k) = OrdCond (Compare a b) 'True 'False 'True ~ 'True Source #

type (>=) (a :: k) (b :: k) = (a >=? b) ~ 'True Source #

Axiomata

Equivalence

class Equivalence e where Source #

Eq for Sing e with Compare @e. Due to the inclusion of sub, symEq and transEq are demoted to lemmata.

Methods

(=?) Source #

Arguments

:: forall (a :: e) (b :: e). Sing e a
-> Sing e b
-> Either ((a :~: b) -> Void) (a :~: b)

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 \]

refl Source #

Arguments

:: forall (a :: e). Sing e a
-> Proof (a == a)

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.

sub Source #

Arguments

:: forall (a :: e) (b :: e). a == b
=> Sing e a
-> Sing e b
-> a :~: b

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.

Instances

Instances details

Equivalence Nat Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (=?) :: forall (a :: Nat) (b :: Nat). Sing Nat a -> Sing Nat b -> Either ((a :~: b) -> Void) (a :~: b) Source # refl :: forall (a :: Nat). Sing Nat a -> Proof (a == a) Source # sub :: forall (a :: Nat) (b :: Nat). a == b => Sing Nat a -> Sing Nat b -> a :~: b Source #
Equivalence Char Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (=?) :: forall (a :: Char) (b :: Char). Sing Char a -> Sing Char b -> Either ((a :~: b) -> Void) (a :~: b) Source # refl :: forall (a :: Char). Sing Char a -> Proof (a == a) Source # sub :: forall (a :: Char) (b :: Char). a == b => Sing Char a -> Sing Char b -> a :~: b Source #
Equivalence Symbol Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (=?) :: forall (a :: Symbol) (b :: Symbol). Sing Symbol a -> Sing Symbol b -> Either ((a :~: b) -> Void) (a :~: b) Source # refl :: forall (a :: Symbol). Sing Symbol a -> Proof (a == a) Source # sub :: forall (a :: Symbol) (b :: Symbol). a == b => Sing Symbol a -> Sing Symbol b -> a :~: b Source #

Total Order

class Equivalence o => TotalOrder o where Source #

Ord for Sing e with Compare @e.

Methods

(<|=|>) Source #

Arguments

:: forall (a :: o) (b :: o). Sing o a
-> Sing o b
-> OrderingI a b

Decidable connectivity of ordering.

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

antiSym Source #

Arguments

:: forall (a :: o) (b :: o). Sing o a
-> Sing o b
-> Compare a b :~: Reflect (Compare b a)

Anti-symmetry of ordering.

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

transLeq Source #

Arguments

:: forall (a :: o) (b :: o) (c :: o). (a <= b, b <= c)
=> Sing o a
-> Sing o b
-> Sing o c
-> Proof (a <= c)

Transitivity of \( \leq \).

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

Instances

Instances details

TotalOrder Nat Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (<\|=\|>) :: forall (a :: Nat) (b :: Nat). Sing Nat a -> Sing Nat b -> OrderingI a b Source # antiSym :: forall (a :: Nat) (b :: Nat). Sing Nat a -> Sing Nat b -> Compare a b :~: Reflect (Compare b a) Source # transLeq :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b, b <= c) => Sing Nat a -> Sing Nat b -> Sing Nat c -> Proof (a <= c) Source #
TotalOrder Char Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (<\|=\|>) :: forall (a :: Char) (b :: Char). Sing Char a -> Sing Char b -> OrderingI a b Source # antiSym :: forall (a :: Char) (b :: Char). Sing Char a -> Sing Char b -> Compare a b :~: Reflect (Compare b a) Source # transLeq :: forall (a :: Char) (b :: Char) (c :: Char). (a <= b, b <= c) => Sing Char a -> Sing Char b -> Sing Char c -> Proof (a <= c) Source #
TotalOrder Symbol Source #
Instance details Defined in Data.Type.Ord.Axiomata Methods (<\|=\|>) :: forall (a :: Symbol) (b :: Symbol). Sing Symbol a -> Sing Symbol b -> OrderingI a b Source # antiSym :: forall (a :: Symbol) (b :: Symbol). Sing Symbol a -> Sing Symbol b -> Compare a b :~: Reflect (Compare b a) Source # transLeq :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol). (a <= b, b <= c) => Sing Symbol a -> Sing Symbol b -> Sing Symbol c -> Proof (a <= c) Source #

type family Reflect (o :: Ordering) = (p :: Ordering) | p -> o where ... Source #

Reflect an Ordering (to express anti-symmetry).

Equations

Reflect 'LT = 'GT
Reflect 'EQ = 'EQ
Reflect 'GT = 'LT

minTO :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Sing o (Min a b) Source #

The minimum of two totally-ordered singletons.

maxTO :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> Sing o (Max a b) Source #

The maximum of two totally-ordered singletons.

defaultDecideEq Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> Either ((a :~: b) -> Void) (a :~: b)

A default implementation of =? in terms of <|=|>.

Bounding

class TotalOrder o => BoundedBelow o where Source #

TotalOrders with LowerBounds.

Associated Types

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

Methods

lowerBound :: Sing o (LowerBound o) Source #

Existence of a lower bound \( b_l \).

least :: forall (a :: o). Sing o a -> Proof (LowerBound o <= a) Source #

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

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

Instances

Instances details

BoundedBelow Nat Source #

Instance details

Defined in Data.Type.Ord.Axiomata

Associated Types

type LowerBound Nat
Instance details Defined in Data.Type.Ord.Axiomata type LowerBound Nat = 0

Methods

lowerBound :: Sing Nat (LowerBound Nat) Source #

least :: forall (a :: Nat). Sing Nat a -> Proof (LowerBound Nat <= a) Source #

BoundedBelow Char Source #

Instance details

Defined in Data.Type.Ord.Axiomata

Associated Types

type LowerBound Char
Instance details Defined in Data.Type.Ord.Axiomata type LowerBound Char = '\NUL'

Methods

lowerBound :: Sing Char (LowerBound Char) Source #

least :: forall (a :: Char). Sing Char a -> Proof (LowerBound Char <= a) Source #

BoundedBelow Symbol Source #

Instance details

Defined in Data.Type.Ord.Axiomata

Associated Types

type LowerBound Symbol
Instance details Defined in Data.Type.Ord.Axiomata type LowerBound Symbol = ""

Methods

lowerBound :: Sing Symbol (LowerBound Symbol) Source #

least :: forall (a :: Symbol). Sing Symbol a -> Proof (LowerBound Symbol <= a) Source #

class TotalOrder o => BoundedAbove o where Source #

TotalOrders with UpperBounds.

Associated Types

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

Methods

upperBound :: Sing o (UpperBound o) Source #

Existence of an upper bound \( b_u \).

greatest :: forall (a :: o). Sing o a -> Proof (a <= UpperBound o) Source #

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

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

Miscellaneous Type Families

type family Sing k = (s :: k -> Type) | s -> k Source #

A mapping from kinds to their corresponding singleton type constructors.

Instances

Instances details

type Sing Nat Source #
Instance details Defined in Data.Type.Ord.Axiomata type Sing Nat = SNat
type Sing Char Source #
Instance details Defined in Data.Type.Ord.Axiomata type Sing Char = SChar
type Sing Symbol Source #
Instance details Defined in Data.Type.Ord.Axiomata type Sing Symbol = SSymbol

type family Proof c = (r :: Type) | r -> c where ... Source #

A mapping from equality constraints to their corresponding evidence carriers.

Equations

Proof (a ~ b) = a :~: b