{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2626","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2626/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2626/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2626/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2626","id":106938440,"number":2626,"title":"Support for IEEE 754-2008 floating point numbers","user":{"login":"bgaster","id":185398,"avatar_url":"https://avatars.githubusercontent.com/u/185398?v=3","gravatar_id":"","url":"https://api.github.com/users/bgaster","html_url":"https://github.com/bgaster","followers_url":"https://api.github.com/users/bgaster/followers","following_url":"https://api.github.com/users/bgaster/following{/other_user}","gists_url":"https://api.github.com/users/bgaster/gists{/gist_id}","starred_url":"https://api.github.com/users/bgaster/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bgaster/subscriptions","organizations_url":"https://api.github.com/users/bgaster/orgs","repos_url":"https://api.github.com/users/bgaster/repos","events_url":"https://api.github.com/users/bgaster/events{/privacy}","received_events_url":"https://api.github.com/users/bgaster/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-09-17T08:49:55Z","updated_at":"2015-09-18T08:15:55Z","closed_at":null,"body":"Currently Idris supports only double precision floating point numbers. The lack of support for single precision floating point numbers is quite limiting, for example graphics API's, such as OpenGL and DirectX, depend mostly on single precision. Moreover backend targets such as Java and C both natively support single precision and it seems strange not to be able to target them directly.\r\n\r\nFurther to this in the age of computations being more and more bandwidth limit, e.g. many graphics applications, there has seen a shift for native support, in many platforms, for half precision floating point, i.e. 16-bit floating point numbers. \r\n\r\nTo this end I would like to propose that support is added to Idris for at least:\r\n\r\n  Single precision \r\n\r\nand either required or optional (backend) support for \r\n\r\n  Half precision\r\n\r\nOne way to handle the half would be to implement a package similar to Haskell's:\r\n\r\n   https://github.com/ekmett/half\r\n\r\nbut this leads to concerns about performance on platforms that natively support Half. Also see note at end about implementing half in terms of single.\r\n\r\nTo this end I would like to propose that the following types are added as primitives to Idris:\r\n\r\nFloat16 (half precision)\r\nFloat32 (single precision)\r\nFloat64 (double precision)\r\n\r\nFloat64 would just be an alternative name for Float, i.e. double, that Idris already supports. Float16 could be optionally supported by a backend and something like the Haskell half package could be used for implementations that do not provide native support. \r\n\r\nSupporting at least Float32 puts Idris in line with other functional languages, e.g. Haskell, as a minimum.\r\n\r\n I do have some concerns that Idris currently uses Float for double precision, as this is confusing when compared to almost all other programming languages. To change it now, of course, would be a code breaking change, but maybe it would make more sense to define:\r\n\r\nHalf      (half precision)\r\nFloat    (single precision)\r\nDouble (double precision)\r\n\r\nThis would seem more standard when compared to other languages.\r\n\r\nNote on half precision: As half is not supported directly in languages like C and Java and not all hardware  currently supports it natively, then a naive implementation might simply promote to single precision, perform the necessary operations, and \"round\" back down to half. This can be a serious issue in the presence of NANs, for example. Clearly this can lead to different implementation capabilities being exposed to the developer and thus we might want to specify what is allowed behaviour."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/141378027","html_url":"https://github.com/idris-lang/Idris-dev/issues/2626#issuecomment-141378027","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2626","id":141378027,"user":{"login":"bgaster","id":185398,"avatar_url":"https://avatars.githubusercontent.com/u/185398?v=3","gravatar_id":"","url":"https://api.github.com/users/bgaster","html_url":"https://github.com/bgaster","followers_url":"https://api.github.com/users/bgaster/followers","following_url":"https://api.github.com/users/bgaster/following{/other_user}","gists_url":"https://api.github.com/users/bgaster/gists{/gist_id}","starred_url":"https://api.github.com/users/bgaster/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/bgaster/subscriptions","organizations_url":"https://api.github.com/users/bgaster/orgs","repos_url":"https://api.github.com/users/bgaster/repos","events_url":"https://api.github.com/users/bgaster/events{/privacy}","received_events_url":"https://api.github.com/users/bgaster/received_events","type":"User","site_admin":false},"created_at":"2015-09-18T08:15:55Z","updated_at":"2015-09-18T08:15:55Z","body":"I take your point and concern about the blowup in primitives and agree that\nin the case of half that a pluggable primitive might be a good way to go,\nbut I really can't see a good argument for not being on par with other\nlanguages when it comes to single precision, e.g. Haskell. I really think\nIdris needs to support single and double precision as a base feature set\nand beyond that I agree it is more questionable.\n\nMy long term goal is to use Idris as a platform for graphics/vision\nresearch with high-level languages and in that regard I feel that single\nprecision support is a necessary evil, as all of the main stream APIs use\nfloat almost everywhere, e.g. any 3D mesh is going to have vertices\nrepresented in single precision, the cost to move them to double would\ndouble the size of the mesh, which are already pretty large, in many cases.\n\nThat being said I don't yet have practical examples of floating point\narithmetic in types, however, I can envision such applications as we go\ndown the path of graphics research.\n\nOn Thu, Sep 17, 2015 at 10:53 AM, Markus Pfeiffer <notifications@github.com>\nwrote:\n\n> I am a bit concerned about the blowup in number of types, and primitives\n> (you'll have to supply primitives for all the float functions that people\n> want for example, and make sure they always work as they should). This\n> should quite probably be a library, or even a set of libraries.\n>\n> I am also not sure about the usefulness of floating point arithmetic in\n> types, even though I can imagine ways to use them.\n>\n> I suggest you have a look at the pluggable primitives as well. I imagine\n> *processing* any amount of floating point in Idris directly will be a bit\n> frustrating.\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/idris-lang/Idris-dev/issues/2626#issuecomment-141027263>\n> .\n>\n"}}