Floating point in the type system

[via Digitalmars-d]

On Saturday, 12 September 2015 at 19:02:16 UTC, Robert wrote:
> handle unusual cases like this. In the process we've managed to 
> break the Idris type system: 
> https://github.com/idris-lang/Idris-dev/issues/2609.

I don't know Idris, but you can't easily unify over floats, 
because they are samples on an interval, and don't behave like 
real numbers, but more like underspecified intervals from 
interval arithmetics.

If you want to unify over reals, you probably should do it 
symbolically.

Or just treat float values as literal symbols in the type system. 
It is useful for configuration: Frequency!342.234

Sometimes it is worthwhile to have an unsound type system. Both D 
and Dart have somewhat unsound type systems. It puts a burden on 
the programmer, but can be useful.