Counting Infinity

import Data.List
import Data.Ratio

-- A few utilities and toys for later:

data Void                    {- This needs -XEmptyDataDecls -}
instance Show Void

data Tree = N | Tree :@: Tree deriving Show

-- interleaving append
a      +~~+ []     = a
[]     +~~+ b      = b
(a:as) +~~+ (b:bs) = a : b : as +~~+ bs

diagonalZipWith f as bs = [ f a b
                          | (x,y) <- pairs
                          , a <- as !! x
                          , b <- bs !! y ]
  where []     !! _ = []
        (x:_)  !! 0 = [x]
        (_:xs) !! n = xs !! (n-1)

(*) `on` f = \x y -> f x * f y




-- We shall get started with some basic infinite sets of numbers

nats = [0..]
-- [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,..]

ints = 0 : [1..] +~~+ map negate [1..]
-- [0,1,-1,2,-2,3,-3,4,-4,5,-5,6,-6,7,-7,8,-8,9,-9,10,-10,11,-11,..]

primes = nubBy(((>1).).gcd)[2..]
-- [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,..]
-- (My thanks to the author of this whoever you are (: )

fibs = map fst $ iterate (\(x,y)->(y,x+y)) $ (0,1)
-- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377,610,987,1597,2584,4181,..]




-- Looking at the diagonals of every pair of nats:
--
--   (0,0) (1,0) (2,0) (3,0)
--   (0,1) (1,1) (2,1) (3,1)
--   (0,2) (1,2) (2,2) (3,2)
--   (0,3) (1,3) (2,3) (3,3)
--
-- Each element of the first diagonal, having one element, sums to zero,
-- Each element of the second, two of them, sums to one, ...

pairs = concatMap pairsSummingTo [0..]
  where pairsSummingTo n = map (\i -> (i, n-i)) [0..n]
-- [(0,0),(0,1),(1,0),(0,2),(1,1),(2,0),(0,3),(1,2),(2,1),(3,0),(0,4),
--  (1,3),(2,2),(3,1),(4,0),(0,5),(1,4),(2,3),(3,2),(4,1),(5,0),(0,6),
--  (1,5),(2,4),(3,3),(4,2),(5,1),(6,0),(0,7),(1,6),...]




-- Let us consider every unique rational, They all (a%b) have GCD(a,b) = 1
-- Let's then, start with the GCD 1 and execute Euclid's algorithm backwards.

{-
 - i: 1%1 in Q
 - f: a%b in Q -> (a+b)%b in Q
 - g: a%b in Q -> a%(a+b) in Q
 -}

{- [{I}, {FI}, {GI}, {FFI}, {FGI}, {GFI}, {GGI}, {FFFI}, ...] -}
{- concat [[{I}], [{FI}, {GI}], [{FFI}, {FGI}, {GFI}, {GGI}],
           [{FFFI}, ...], ...] -}

rationals = let rats   0   = [i]
                rats (n+1) = map f (rats n) ++ map g (rats n)
             in concatMap rats nats
  where i   = 1%1
        f r = (numerator r + denominator r) % denominator r
        g r = numerator r % (numerator r + denominator r)
-- [1%1,2%1,1%2,3%1,3%2,2%3,1%3,4%1,5%2,5%3,4%3,3%4,3%5,2%5,1%4,5%1,7%2,
--  8%3,7%3,7%4,8%5,7%5,5%4,4%5,5%7,5%8,4%7,3%7,3%8,2%7,...]





-- Every string that can be made from a list of symbols
strings symbols = concat [ enumerate n symbols | n <- [1..] ]
  where enumerate 0 _ = [""]
        enumerate n d = concatMap (\y->map (:y) d) (enumerate (n-1) d)


-- Every binary sequence
binary = strings ['1', '0']
-- ["1","0","11","01","10","00","111","011","101","001","110",
--  "010","100","000","1111","0111","1011","0011","1101","0101",
--  "1001","0001","1110","0110","1010","0010","1100","0100","1000",...]


-- This is a very slow method to generate all well parenthesized expressions
-- It is a perfectly valid method for proving that a set is enumerable though
-- In general, showing that a set is the subset of all strings composed from
-- some symbols
parenthesized = filter balanced $ strings ['(', ')']
  where split s = map (flip splitAt s) [1..length s-1]
        balanced []     = True
        balanced (_:[]) = False
        balanced s      =     head s == '(' && last s == ')'
                           && balanced (tail $ init $ s)
                        || any (uncurry ((&&) `on` balanced)) (split s)
-- ["()","()()","(())","()()()","(())()","()(())","(()())","((()))",
--  "()()()()","(())()()","()(())()","(()())()","((()))()","()()(())",
--  "(())(())","()(()())","(()()())","((())())","()((()))","(()(()))",
--  "((()()))","(((())))",...]



-- This is fabulous, So I stole it from:
-- http://web.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/spigot.pdf
pi = g(1,180,60,2) where 
  g(q,r,t,i) = let (u,y)=(3*(3*i+1)*(3*i+2),div(q*(27*i-12)+5*r)(5*t)) 
               in y : g(10*q*i*(2*i-1),10*u*(q*(5*i-2)+r-y*t),t*u,i+1)
-- [3,1,4,1,5,9,2,6,5,3,5,8,9,7,9,3,2,3,8,4,6,2,6,4,3,3,8,3,2,7,9,5,0,...]




-- We can use typeclasses to recurse over the structure of a type
-- If a function listing all inhabitants of a type is written,
-- One can be sure that infinity will crop up.

class Inhabitants a where
  inhabitants :: [a]

instance Inhabitants Void where
  inhabitants = []

instance Inhabitants () where
  inhabitants = [()]

instance Inhabitants Bool where
  inhabitants = [True, False]

instance Inhabitants Integer where
  inhabitants = ints

instance Inhabitants a => Inhabitants (Maybe a) where
  inhabitants = [Nothing] ++ map Just inhabitants

instance (Inhabitants a, Inhabitants b) => Inhabitants (Either a b) where
  inhabitants = map Left inhabitants +~~+ map Right inhabitants

instance Inhabitants a => Inhabitants [a] where
  inhabitants = [[]] ++ diagonalZipWith (:) inhabitants inhabitants

instance Inhabitants Tree where
  inhabitants = [N] ++ diagonalZipWith (:@:) inhabitants inhabitants

-- take 600 $ inhabitants :: [ Either [Maybe Integer] Tree ]
--                             ^^ You can try various types here
--                                as long as they are in the
--                                Inhabitants class.