A library demonstrating various approaches to developing a faster Nat
.
See here for a blog post introduction to the main concept of the repo.
Releases are available on Maven. Add the following to your build.sbt:
"io.typechecked" %% "numerology" % "<version>"
for the version of your choice. The project is fully tagged and release versions are available to view online.
Traditional church-encoded Nat
is slow. What alternatives are there?
Binary-encoded Nat
. Significantly faster, and relatively easy for programmers to reason about.
Ternary-encoded Nat
. Significantly faster again. Can reach 10300 whilst performing addition and approx 1040 for multiplication.
It is harder to implement typeclasses for TNat
than the alternatives.
An experiment to see if I could get a Nat
specialised for multiplication.
An MNat
is formed as an HList
of pairs of prime numbers and exponents - the prime factorisation
of the number MNat
represents.
The theory was that multiplication is then reduced to simple list operations (concat, sort, etc), and it would
prove faster than TNat
which relies on recursing on Sum
.
Unfortunately this was not the case. MNat
reaches approx 1020 * 1020 (worst-case integers) before failing. About the square root of TNat
's limit.
When paired with the approach in symbology, this encoding would compile primality testing typeclasses in trivial time.