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?

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

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)

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

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.

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.

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.)

It looks like @DullBananas posted in that issue already

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.

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

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.