I am familiar with the Peano Natural Number definition which is what you see in intro to functional programming courses and examples. But I have also much later encountered a practical implementation of natural numbers, the "Binary Natural Number implementation" like this in Coq. I am not too familiar with them yet, but I imagine it helps with encoding the Natural numbers so you don't have to computer n+1 times to get to 10000 or whatever.
But what about fractions, integers, rational numbers, irrational numbers, or other forms of the natural numbers or these numbers for binary encoding, hexadecimal encoding, or other encodings for performance reasons. Are there any examples out there of functional definitions of numbers that fit this description? I am looking for source code or thorough functional descriptions. I am interested in both breadth and depth (learning of all of the various kinds, with specific implementations).
You can have a look at the standard library of Coq. It contains a variety of numbers, and theorems about different encodings of them. It even contains IEEE standard floats (as well as mathematical real numbers).