Numeric.Natural.Lens

Useful tools for Gödel numbering.

Documentation

_Pair :: Iso' Natural (Natural, Natural)

The natural numbers are isomorphic to the product of the natural numbers with itself.

N = N*N

_Sum :: Iso' Natural (Either Natural Natural)

The natural numbers are isomorphic to disjoint sums of natural numbers embedded as evens or odds.

N = 2*N

_Naturals :: Iso' Natural [Natural]

The natural numbers are isomorphic to lists of natural numbers

pattern Pair :: Natural -> Natural -> Natural

interleaves the bits of two natural numbers

pattern Sum :: Either Natural Natural -> Natural

Sum (Left q) = 2*q
Sum (Right q) = 2*q+1

pattern Naturals :: [Natural] -> Natural

Naturals [] = 0
Naturals (h:t) = 1 + Pair h (Naturals t)