natural-arithmetic: Arithmetic of natural numbers

[ bsd3, library, math ] [ Propose Tags ]

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:

Versions [faq] 0.1.0.0, 0.1.1.0, 0.1.2.0
Change log CHANGELOG.md
Dependencies base (>=4.11 && <5) [details]
License BSD-3-Clause
Copyright 2019 Andrew Martin
Author Andrew Martin
Maintainer andrew.thaddeus@gmail.com
Category Math
Home page https://github.com/andrewthad/natural-arithmetic
Bug tracker https://github.com/andrewthad/natural-arithmetic/issues
Uploaded by andrewthad at Mon Jan 20 18:43:31 UTC 2020
Distributions NixOS:0.1.2.0
Downloads 590 total (135 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2020-01-20 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees