The problems with numbers in Elm

Request Feedback
1

Elm has two types which hold numbers: Int and Float. I think the system of number types in Elm needs improvement (I made 2 posts that are somewhat related to this).

One problem is that there needs to be a more explicit distinction between Int and Float. This includes the syntax for number literals, where there is sometimes no difference between Int an Float. Maybe there should be a syntax in number literals where 3.i is an integer and 3.f is a float. There should also be more explicit separation of the arithmetic operators. One time I saw someone’s idea where they proposed that things like +. would be for floats (I can’t find the post).

Another problem is the ability to remove impossible states in number values. You are forced to have numbers be able to hold a very wide range of numbers. This does not allow you to remove impossible values from numbers. There are packages that try to solve this problem, but they don’t provide enough control. For example, if you have a predefined number value that needs to be within a certain range, but the number you set is out of range, it does not produce a compile error.

This is a great description of how to think about removing impossible states. It says this:

Int is the set { ... -2, -1, 0, 1, 2 ... }

But what if we want it to just be { 0, 1, 2, 3, ... }? There is no way to do that currently.

It also needs to be possible to define 8 bit ints, 16 bit int, etc. because that will be useful in the future if Elm ever is able to compile to WebAssembly.

This is a very difficult language design problem to solve. Do you have any ideas for solving this prob?

2

Maybe we need to have a concept of number sets. We could have a predefined int type:

type Int

And then we could define this type that includes integers from 1 to 10:

type OneToTen
    = Int
    & (n | n <= 10)
    & (n | n >= 1)

And this would give us a compiler error (currently it’s not possible to make this cause a compile error):

badNumber : OneToTen
badNumber =
    68
3

If you want a restricted type, just create your own module with an opaque type and only that module can update it.

Unfortunately Elm has no concept of preconditions so that is not entire safe, but might get you 80% there.

4

I’m currently working on my Master thesis that will introduce a more general concept called refinement types. You can check out my first introduction here:

The Master thesis will be finished next year. I’m expecting to give an update on the current state either in june or in july.

Here’s a head start:

What you are proposing would come with more downsides than benefits. So I highly recommend the elm team to NOT implement anything going in this direction.

Example

Lets say we introduce your proposed definition:

type MinusTwoToTwo =
  Int
  & (n | n <= 2)
  & (n | n >= -2)

type ZeroToFour =
  Int
  & (n | n <= 4)
  & (n | n == 0)

Then the following example can not be compiled:

fun : MinusTwoToTwo -> ZeroToFour
fun x =
  if (x * x) <= (x + x) then
    x * x
  else
    x

(Taken from my thesis proposal)

Just looking at it, it should be easy to check that the types are valid. But for a Computer (a Compiler) comparing multiplication with addition is a hard task.

In fact Z3, the theorem prover that will be used for my implementation and that is also used in Liquid Haskell will fail trying to prove this.

Mathematically speaking we CAN NOT have a program that can solve a general formula using multiplication (and addition).

This has been proven.

So why do a Master thesis about it?

Because while in generally this is not solvable, for a very big range of problems we can actually find a solution. It might be that in some far future we can ensure that the compiler finds a proof for 90% of all typical problems found in the “real world”. The current provers(like Z3) are quite good at proving “normal” statements about indexes. For example something like off by one errors can easily be detected. But it will always be possible that your code - even if its correct - can not be compiled.

Going back to our example, if we just rewrite the code a bit, then the code will compile again.

fun : MinusTwoToTwo -> ZeroToFour
fun x =
  if (x >= -2) && (x <= 2) then
    x * x
  else
    x

(I’ve tested this exact example in Liquid Haskell)

6 Likes
5

It’s probably not even likely that we need the ability to convert from one number type to another

6

The argument stays the same for

type OneToTen
    = Int
    & (n | n <= 10)
    & (n | n >= 1)

fun : OneToTen -> OneToTen
fun x =
  if (x * x) <= (x + x) then
    x * x
  else
    x

By NOT changing the type, the problem actually gets harder (as it’s now more general then before).

What the compiler(the type checker im working on) is tying to solve is to get

( x | x * x <= x + x ) --i hope im using your syntax correctly

into something like

( x | x <= a && x >= b ) --for constants a and b

This is where it fails

3 Likes
7

Maybe there could be a built in general clamp function that is defined like this, which could be very useful for converting between different number types

clamp1 : number1 -> number2

usage

myNum : OneToTen
myNum =
    clamp1 13

myNum == 10
8 
clamp1 : number1 -> number2

Won’t this cause issues as soon as someone writes the following?

floatToInt : Int 
floatToInt =
    clamp1 5.5
9

I guess the best solution is to use opaque types for it.

I would not want to have a native solution. it’s not something that can be done in compile-time and opaque types are already a perfect solution for everything to do with runtime insurance.

10

I agree with @Lucas_Payr. I think that having a native solution would be imperfect in a lot of situations, like if you wanted to model numbers that fulfill other conditions (even or odd, inside a (in)finite set of numbers like {1, 2, 3, 5, 8, 11, …}).

I think that this check is best done in custom code, therefore in a custom opaque type.

You’ll have to deal with a lot of safeguards (functions that return Maybes in case your value doesn’t match the conditions), but I think that that can be simplified when something is easily detectable through static analysis, as I described in safe unsafe operations in Elm.

11

@DullBananas Here is the post about separate operators for Int and Float you were looking for: https://github.com/elm/compiler/issues/2078

I’ve even toyed with the idea of replacing most of Basics with Int and Float modules. Yeah, they’ll have some “duplicate” functions, but that’s not a problem for map? (Not saying this is necessarily a good idea, I just like trying to think outside the box.)

12

It looks like @DullBananas posted in that issue already :slightly_smiling_face:

I’ll second what they asked there though. What does having operators that are explicit for either Float or Int solve? To me it seems like it would result in having to duplicate a lot of math functions? elm-units would especially suffer from this.

13

The main problem with removing impossible states from numbers is the fact that there is no way to define a restricted number in your code without being able to get a compile time error if it is out of bounds. Maybe there could be a syntax that takes a maybe or result and unwraps it, and gives a compile error if it is nothing or err.

So with something like this:

clampMaybe : number -> number -> number -> Maybe number
clampMaybe min max value =
    if value <= max && value >= min then
        Just value
    else
        Nothing

We could have this code:

oneToTen : number -> Maybe number
oneToTen =
    clampMaybe 1 10

{ oneToTen 12 } -- compile error
{ oneToTen 5 } -- 5
14

I’m currently testing a (private) type SafeInt which is restricted to integers in JavaScript safe integer range and defined as

type SafeInt
    = Defined Float
    | Undefined

Undefined works a bit like NaN, but any operation which would result in unrepresentable value causes Undefined, including overflows:

-- `2 ^ 55` is undefined
SafeInt.pow (SafeInt.fromInt 2) (SafeInt.fromInt 55)
    |> SafeInt.toInt
    --> Nothing

While this works and is easy to implement, it’s quite slow - operations can be 100 times slower than with Int. But for my use cases this is good enough.

ps. I’m not using actual NaN internally since that would result in inconsistent behavior because of bug Inconsistant equality for objects containing NaN.

1 Like
15

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.