typechecked/numerology

Numerology

A library demonstrating various approaches to developing a faster Nat.

See here for a blog post introduction to the main concept of the repo.

Installation

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.

The Problem

Traditional church-encoded Nat is slow. What alternatives are there?

BNat

Binary-encoded Nat. Significantly faster, and relatively easy for programmers to reason about.

TNat

Ternary-encoded Nat. Significantly faster again. Can reach 10³⁰⁰ whilst performing addition and approx 10⁴⁰ for multiplication.

It is harder to implement typeclasses for TNat than the alternatives.

MNat

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 10²⁰ * 10²⁰ (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.

numerology's Issues

GCD Algorithm for the three implementations

SBT-microsite

Benchmark different GCD algorithms for BNat

BNat GCD is implemented using Stein's algorithm, which is on paper faster than Euclid's. Would be interesting to see if this holds for BNat in practice

Implement divides for the 3 implementations

a la shapeless