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

Data.Type.Ord.Axiomata

Contents

Sing
Axiomata
Lemmata

Description

Axiomata & lemmata for easier use of Data.Type.Ord.

\[ \newcommand{\colon}{ \! : } \]

Synopsis

type family Sing k = (s :: k -> Type) | s -> k
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 -> Compare a a :~: 'EQ
- sub :: forall (a :: e) (b :: e). Compare a b ~ 'EQ => 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)
- transTO :: forall (a :: o) (b :: o) (c :: o). (a <= b, b <= c) => Sing o a -> Sing o b -> Sing o c -> (a <=? c) :~: 'True
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 -> (LowerBound o <=? a) :~: 'True
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 -> (a <=? UpperBound o) :~: 'True
sym :: forall e (a :: e) (b :: e). (Equivalence e, Compare a b ~ 'EQ) => Sing e a -> Sing e b -> Compare b a :~: 'EQ
transEq :: forall e (a :: e) (b :: e) (c :: e). (Equivalence e, Compare a b ~ 'EQ, Compare b c ~ 'EQ) => Sing e a -> Sing e b -> Sing e c -> Compare a c :~: 'EQ
minDefl1 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> (Min a b <=? a) :~: 'True
minDefl2 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> (Min a b <=? b) :~: 'True
minMono :: forall o (a :: o) (c :: o) (b :: o) (d :: o). (TotalOrder o, a <= c, b <= d) => Sing o a -> Sing o b -> Sing o c -> Sing o d -> (Min a b <=? Min c d) :~: 'True
maxInfl1 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> (a <=? Max a b) :~: 'True
maxInfl2 :: forall o (a :: o) (b :: o). TotalOrder o => Sing o a -> Sing o b -> (b <=? Max a b) :~: 'True
maxMono :: forall o (a :: o) (c :: o) (b :: o) (d :: o). (TotalOrder o, a <= c, b <= d) => Sing o a -> Sing o b -> Sing o c -> Sing o d -> (Max a b <=? Max c d) :~: 'True

Sing

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

Maps 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

Axiomata

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

\[ \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 \geq b &\iff a > b \lor a = b \end{align} \]

These aren't consistent by construction, however—we need more axiomata.

Equivalence

class Equivalence e where Source #

Eq for Sing e with Compare @e. Due to the inclusion of sub, sym 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 \colon 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 \colon a \sim b \lor a \not\sim b \]

refl Source #

Arguments

:: forall (a :: e). Sing e a
-> Compare a a :~: 'EQ

Reflexivity of equivalence.

\[ \forall a \colon a = a \]

Can also be read as:

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

The other direction of sub.

sub Source #

Arguments

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

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

\[ \forall a, b \colon 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 -> Compare a a :~: 'EQ Source # sub :: forall (a :: Nat) (b :: Nat). Compare a b ~ 'EQ => 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 -> Compare a a :~: 'EQ Source # sub :: forall (a :: Char) (b :: Char). Compare a b ~ 'EQ => 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 -> Compare a a :~: 'EQ Source # sub :: forall (a :: Symbol) (b :: Symbol). Compare a b ~ 'EQ => 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 \colon a \lt b \lor a = b \lor a \gt 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 \colon a \leq b \iff b \geq a \]

transTO Source #

Arguments

:: forall (a :: o) (b :: o) (c :: o). (a <= b, b <= c)
=> Sing o a
-> Sing o b
-> Sing o c
-> (a <=? c) :~: 'True

Transitivity of ordering.

\[ \forall a, b, c \colon 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 # transTO :: forall (a :: Nat) (b :: Nat) (c :: Nat). (a <= b, b <= c) => Sing Nat a -> Sing Nat b -> Sing Nat c -> (a <=? c) :~: 'True 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 # transTO :: forall (a :: Char) (b :: Char) (c :: Char). (a <= b, b <= c) => Sing Char a -> Sing Char b -> Sing Char c -> (a <=? c) :~: 'True 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 # transTO :: forall (a :: Symbol) (b :: Symbol) (c :: Symbol). (a <= b, b <= c) => Sing Symbol a -> Sing Symbol b -> Sing Symbol c -> (a <=? c) :~: 'True 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 -> (LowerBound o <=? a) :~: 'True Source #

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

\[ \forall a \colon 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 -> (LowerBound Nat <=? a) :~: 'True 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 -> (LowerBound Char <=? a) :~: 'True 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 -> (LowerBound Symbol <=? a) :~: 'True 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 -> (a <=? UpperBound o) :~: 'True Source #

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

\[ \forall a \colon a \leq b_u \]

Lemmata

Equivalence

sym Source #

Arguments

:: forall e (a :: e) (b :: e). (Equivalence e, Compare a b ~ 'EQ)
=> Sing e a
-> Sing e b
-> Compare b a :~: 'EQ

Symmetry of equivalence.

\[ \forall a, b \colon a = b \iff b = a \]

transEq Source #

Arguments

:: forall e (a :: e) (b :: e) (c :: e). (Equivalence e, Compare a b ~ 'EQ, Compare b c ~ 'EQ)
=> Sing e a
-> Sing e b
-> Sing e c
-> Compare a c :~: 'EQ

Transitivity of equivalence.

\[ \forall a, b, c \colon a = b \land b = c \implies a = c \]

Min

minDefl1 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> (Min a b <=? a) :~: 'True

Min is deflationary in its first argument.

\[ \mathrm{min} \, a \, b \leq a \]

minDefl2 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> (Min a b <=? b) :~: 'True

Min is deflationary in its second argument.

\[ \mathrm{min} \, a \, b \leq b \]

minMono Source #

Arguments

:: forall o (a :: o) (c :: o) (b :: o) (d :: o). (TotalOrder o, a <= c, b <= d)
=> Sing o a
-> Sing o b
-> Sing o c
-> Sing o d
-> (Min a b <=? Min c d) :~: 'True

Min is monotonic in both arguments.

\[ a \leq c \land b \leq d \implies \mathrm{min} \, a \, b \leq \mathrm{min} \, c \, d \]

Max

maxInfl1 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> (a <=? Max a b) :~: 'True

Max is inflationary in its first argument.

\[ a \leq \mathrm{max} \, a \, b \]

maxInfl2 Source #

Arguments

:: forall o (a :: o) (b :: o). TotalOrder o
=> Sing o a
-> Sing o b
-> (b <=? Max a b) :~: 'True

Max is inflationary in its second argument.

\[ b \leq \mathrm{max} \, a \, b \]

maxMono Source #

Arguments

:: forall o (a :: o) (c :: o) (b :: o) (d :: o). (TotalOrder o, a <= c, b <= d)
=> Sing o a
-> Sing o b
-> Sing o c
-> Sing o d
-> (Max a b <=? Max c d) :~: 'True

Max is monotonic in both arguments.

\[ a \leq c \land b \leq d \implies \mathrm{max} \, a \, b \leq \mathrm{max} \, c \, d \]