Is this a valid representation of real numbers?

Question

I am trying to find the simplest representation of real numbers on the lambda calculus. I've thought about this one, and wonder if this is valid. First, we define a real number in the range -1.0 - 0.0 as any member of the following datatype (on Haskell for clarity):

data Part = Left Part | Right Part | Zero

With the following interpretation:

toFloat :: Part -> Float
toFloat x = go x 0.5 where
    go (Left x)  add = add + go x (add / 2)
    go (Right x) add = add + go x (add / 2)
    go Zero      add = 0.0

I believe this provides an unique isomorphism between elements of Part and Real numbers on the range [-1.0, 1.0]. Some examples:

0    = Zero
0.5  = Right Zero
0.25 = Right (Left Zero)
1.0  = Right 1.0
1/3  = a procedure that approaches its value

Then, a real number can be defined as a tuple (Nat, Part) there Nat is a natural number multiplier and Part is a real number on the range -1.0, 1.0. This looks much simpler than cauchy sequences. Is this structure and interpretation truly isomorphic to real numbers?

Answer 1

No, it's not. Even if you fix the typos (right now there is no difference between Left and Right), what would be Left 1.0?

Basically, you are reinventing binary representation of real numbers, and it's well known that some numbers have two representations.