rename Double type, "Float", to a more informative type

[cartazio]

Either "Double", or as some folks suggested on IRC, Float64. (latter is More systematic, so i'd be ok with ). Point being Float is needlessly misleading and does't communicate correctly that nature of the float model

Should I email the idris list for this? I'm happy to write the patch for this once its sorted out.

[cartazio]

I'll cook up a patch for this when things get less hectic for me in the next week or two since folks seem in favor of it

[brendanzab]

For precedants, Go uses float32 and float64 and Rust uses f32 and f64. These reflect the sizes specified in the IEEE floating point spec. C of course uses float and double, but that is a historical thing. If one was truly systematic, the 32-bit float should actually be called single (if going by that naming scheme). One could argue that Float might be better used for the type class.

[Ralith]

Another datapoint: Julia also uses Float32 and Float64.

[cartazio]

Wait, did you add 32 bit floats and rename the float type to double?
On Mar 30, 2015 7:04 PM, "Jan de Muijnck-Hughes" notifications@github.com
wrote:

Closed #379 #379 via
67a9d4d
67a9d4d
.

—
Reply to this email directly or view it on GitHub
#379 (comment).

[jfdm]

@cartazio In Commit 89e325c @edwinb renamed the name of Float to Double so that it is more informative, thus addressing this issue. I have added a line into the FAQ describing the reasoning behind the naming convention used and why a Float64 name wasn't provided. I also recommended that this issue has been closed. Moreno, it is to the best of my knowledge that a Float primitive has not been added, and that the type alias called Float is there for backwards compatibility until the next release of Idris.

Whether we need a size 32 float type is not my call.

[cartazio]

Ok. Sounds reasonable
On Mar 31, 2015 2:55 AM, "Jan de Muijnck-Hughes" notifications@github.com
wrote:

@cartazio https://github.com/cartazio In Commit 89e325c
89e325c
@edwinb https://github.com/edwinb renamed the name of Float to Double
so that it is more informative, thus addressing this issue. I have added a
line into the FAQ describing the reasoning behind the naming convention
used and why a Float64 name wasn't provided. I also recommended that this
issue has been closed. Moreno, it is to the best of my knowledge that a
Float primitive has not been added, and that the type alias called Float
is there for backwards compatibility until the next release of Idris.

Whether we need a size 32 float type is not my call.

—
Reply to this email directly or view it on GitHub
#379 (comment)
.