Hackage :: [Package]

ord-axiomata: Axiomata & lemmata for easier use of Data.Type.Ord

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

When using Data.Type.Ord, there are many facts one intuitively expects to hold that GHC is not clever enough to infer.

We rectify this situation with a TotalOrder typeclass providing axiomata with which such facts may be proven to GHC.

[Skip to Readme]

Properties

Versions 0.1.0.0
Change log CHANGELOG.md
Dependencies base (>=4.19 && <5) [details]
License BSD-3-Clause
Copyright (c) L. S. Leary 2025
Author L. S. Leary
Maintainer L.S.Leary.II@gmail.com
Category Data, Math
Home page https://github.com/LSLeary/ord-axiomata
Bug tracker https://github.com/LSLeary/ord-axiomata/issues
Source repo head: git clone https://github.com/LSLeary/ord-axiomata.git
this: git clone https://github.com/LSLeary/ord-axiomata.git(tag v0.1.0.0)
Uploaded by Leary at 2025-06-21T07:45:09Z

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for ord-axiomata-0.1.0.0

[back to package description]

ord-axiomata

When using Data.Type.Ord, there are many facts one intuitively expects to hold that GHC is not clever enough to infer.

We rectify this situation with a TotalOrder typeclass that not only enables comparison of singletons, but also provides axiomata allowing one to safely prove such facts to GHC.

Axiomata

Alongside TotalOrder, there are a few other accompanying classes.

Equivalence

\[ \begin{alignat*}{3} &\text{reflexivity} \quad\quad\quad && \forall a \kern-2pt : \kern6pt && a = a \\ &\text{symmetry} \quad\quad\quad && \forall a, b \kern-2pt : \kern6pt && a = b \implies b = a \\ &\text{transitivity} \quad\quad\quad && \forall a, b, c \kern-2pt : \kern6pt && a = b \land b = c \implies a = c \\ \end{alignat*} \]

Total Ordering

\[ \begin{alignat*}{3} &\text{strong connectivity} \quad\quad\quad && \forall a, b \kern-2pt : \kern6pt && a \lt b \lor a = b \lor a \gt b \\ &\text{anti-symmetry} \quad\quad\quad && \forall a, b \kern-2pt : \kern6pt && a \le b \implies b \ge a \\ &\text{transitivity} \quad\quad\quad && \forall a, b, c \kern-2pt : \kern6pt && a \leq b \land b \leq c \implies a \leq c \\ \end{alignat*} \]

Bounding

\[ \begin{alignat*}{3} &\text{bounded below} \quad\quad\quad && \exists l \forall a \kern-2pt : \kern6pt && l \leq a \\ &\text{bounded above} \quad\quad\quad && \exists u \forall a \kern-2pt : \kern6pt && a \leq u \\ \end{alignat*} \]

Lemmata

With the above at our disposal, we can prove general, reusable facts. Both for practical use and as demonstration, we provide several lemmata for the Min and Max type families.

Minimum

\[ \begin{alignat*}{3} &\text{deflationary} \quad\quad\quad && \forall a, b \kern-2pt : \kern6pt && \mathrm{min} \kern3pt a \kern3pt b \leq a, b \\ &\text{monotonicity} \quad\quad\quad && \forall a, b, c, d \kern-2pt : \kern6pt && a \leq c \land b \leq d \implies \mathrm{min} \kern3pt a \kern3pt b \leq \mathrm{min} \kern3pt c \kern3pt d \\ \end{alignat*} \]

Maximum

\[ \begin{alignat*}{3} &\text{inflationary} \quad\quad\quad && \forall a, b \kern-2pt : \kern6pt && a, b \leq \mathrm{max} \kern3pt a \kern3pt b \\ &\text{monotonicity} \quad\quad\quad && \forall a, b, c, d \kern-2pt : \kern6pt && a \leq c \land b \leq d \implies \mathrm{max} \kern3pt a \kern3pt b \leq \mathrm{max} \kern3pt c \kern3pt d \\ \end{alignat*} \]