Single precision (32 bit) floating point

[joelberkeley]

• I have read CONTRIBUTING.md.
• I have checked that there is no existing PR/issue about my proposal.

Summary

I would like Idris to have a single precision 32-bit floating point primitive.

Motivation

My use case is numerical computing. Deep learning, in particular, uses this heavily.

The proposal

The main breaking change I foresee is that backends won't support it out of the box. @dunhamsteve even points out that JS might not be able to support it (I haven't looked). I know little about backends generally.

I also imagine this might introduce a bunch of resolution errors re floating point literals, unless we default to Double for backwards compatibility.

It would presumably be called Float, to match Double (and Idris1 Float?).

Do we want a floating-point interface for functions on floats (sin etc.), or do we overload. Overload seems practical, assuming we won't add any other precisions (what about complex?).

Examples

Trivially obvious, but anyway ...

pi : Float
pi = 3.141592625358979

Technical implementation

I assume the C implementation will just be float.

Idris code may just be a copy-paste for interfaces on Double.

Alternatives considered

Not introducing it.

Other alternatives require more insight into implementation.

Conclusion

I'm not aware of any language with fixed-width floating point that doesn't have this.

[buzden]

A feasible alternative can be to have a library with [external] datatype and FFI calls for primitive operations, literals support and standard interface implementations. Particular library is free to not to support all backends, so there will be no problem with js inability.