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.
