Modulelens-5.3.5Haskell2010

Numeric.Natural.Lens

Useful tools for Gödel numbering.

value_Pair :: Iso' Natural (Natural, Natural)

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

N = N*N

value_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

value_Naturals :: Iso' Natural [Natural]

The natural numbers are isomorphic to lists of natural numbers

patternpattern Pair :: Natural -> Natural -> Natural

interleaves the bits of two natural numbers

patternpattern Sum :: Either Natural Natural -> Natural

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

patternpattern Naturals :: [Natural] -> Natural

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