natural-arithmetic: Arithmetic of natural numbers
A search for terms like arithmetic
and natural
on hackage reveals
no shortage of libraries for handling the arithmetic of natural
numbers. How is this library any different some of the others? It has
a particular purpose: providing a foundation on top on which other
libraries may define types indexed by sizes. This uses GHC's
non-inductively-defined GHC.TypeNats.Nat
. As a rule, this does not
use unsafeCoerce
internally anywhere.
Perhaps the most direct competitor to `natural-arithmetic` is a typechecker plugin like type-nat-solver. The big difference is that `type-nat-solver` can really only be used in application code, not in library code. This is because libraries should not require the presence of typechecker plugins. Technically, they can (you could document it), but many developers will not use libraries that have unusual install procedures like this.
This library, in places, requires users to use the TypeApplications
language extension. This is done when a number is only need at
the type level (without a runtime witness).
This library uses a non-minimal core, providing redundant primitives
in Arithmetic.Lt
and Arithmetic.Lte
. This is done in the interest
of making it easy for user to assemble proofs. Recall that proof
assembly is done by hand rather than by an SMT solver, so removing
some tediousness from this is helpful to users.
This library provides left and variants variants of several functions.
For example, Arithmetic.Lte
provides both substituteL
and
substituteR
. This is only done when there are two variants of
a function. For substitution, this is the case because we have
`b = c, a ≤ b ==> a ≤ c` and `a = c, a ≤ b ==> c ≤ b`. So, we
provide both substituteL
and substituteR
. However,
for addition of inequalities, we have four possible variants:
`a ≤ b, c ≤ d ==> a + c ≤ b + d`, `a ≤ b, c ≤ d ==> c + a ≤ b + d`,
`a ≤ b, c ≤ d ==> a + c ≤ d + b`, `a ≤ b, c ≤ d ==> c + a ≤ d + b`.
Consequently, we only provide a single plus
function, and users
must use Arithmetic.Plus.commutative
to further manipulate the
inequality.
Here are the proof-manipulation vocabulary used by this library. Many of these terms are not standard, but we try to be consistent in this library:
Weaken: Increase an upper bound without changing the bounded value
Increment: Increase an upper bound along with the bounded value
Decrement: Decrease an upper bound along with the bounded value
Substitute: Replace a number with an equal number
Modules
[Index] [Quick Jump]
Downloads
- natural-arithmetic-0.2.1.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.1.0.0, 0.1.1.0, 0.1.2.0, 0.1.3.0, 0.1.4.0, 0.2.0.0, 0.2.1.0 |
---|---|
Change log | CHANGELOG.md |
Dependencies | base (>=4.14 && <5), unlifted (>=0.2.1) [details] |
License | BSD-3-Clause |
Copyright | 2019 Andrew Martin |
Author | Andrew Martin |
Maintainer | amartin@layer3com.com |
Category | Math |
Home page | https://github.com/byteverse/natural-arithmetic |
Bug tracker | https://github.com/byteverse/natural-arithmetic/issues |
Source repo | head: git clone git://github.com/byteverse/natural-arithmetic.git |
Uploaded | by l3c_amartin at 2024-02-03T02:02:04Z |
Distributions | LTSHaskell:0.2.1.0, NixOS:0.1.4.0, Stackage:0.2.1.0 |
Reverse Dependencies | 16 direct, 110 indirect [details] |
Downloads | 5914 total (83 in the last 30 days) |
Rating | (no votes yet) [estimated by Bayesian average] |
Your Rating | |
Status | Docs available [build log] Last success reported on 2024-02-03 [all 1 reports] |