What something is is what you can do with it

I.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module I where

-- reals in the interval [0,1]

-- If you have some I, and you give me any average algebra a
-- then I will give you a view of I as a sequence of a-valued approximations
data I where
  MkI :: (forall a . AvgAlgebra a => [a]) -> I

-- observe an I as a sequence of approximations
observe :: AvgAlgebra a => I -> [a]
observe (MkI xs) = xs

-- arbitrarily choose an approximation level to stop at
est :: AvgAlgebra a => I -> a
est (MkI xs) = case drop 100 xs of
  [] -> last xs
  (x:xs) -> x

-- An average algebra is some type a with two distinguished points
-- and an average operation. 
class AvgAlgebra a where
  avg :: a -> a -> a
  p0 :: a
  p1 :: a


-- Examples

-- floats as an example average algebra
instance AvgAlgebra Double where
  avg x y = (x + y) / 2
  p0 = 0
  p1 = 1

-- for fun, I itself is an average algebra
instance AvgAlgebra I where
  p0 = MkI (repeat p0)
  p1 = MkI (repeat p1)
  avg (MkI xs) (MkI ys) = MkI (zipWith avg xs ys)



data Bit = Zero | One deriving Show

-- [Bit] can serve as an I implementation
wrapBits :: [Bit] -> I
wrapBits bs = MkI f where
  f :: AvgAlgebra a => [a]
  f = go p0 p1 bs where
    go x y []     = []
    go x y (Zero:bs) = let y' = avg x y in y' : go x y' bs
    go x y (One:bs)  = let x' = avg x y in x' : go x' y bs

-- floats in the range [0,1] can serve as an I implementation
wrapFloat :: Double -> I
wrapFloat z = MkI f where
  f :: AvgAlgebra a => [a]
  trunc z = z - fromInteger (floor z)
  f = go p0 p1 z where
    go x y z | z < 0.5  = let y' = avg x y in y' : go x y' (trunc (2 * z))
             | z >= 0.5 = let x' = avg x y in x' : go x' y (trunc (2 * z))


-- example of an irrational number "0.10100100010000..."
irr :: I
irr = wrapBits (go 0) where
  go i = replicate i Zero ++ [One] ++ go (i+1)



-- construction of a number in total isolation
cool :: I
cool = MkI (go p0 p1 100) where
  go x y 0 = []
  go x y i | i `mod` 3 == 0 = x : go x (avg x y) (i-1)
           | otherwise      = x : go (avg x y) y (i-1)