I want to create a percentage type using floats, something like:
@type percentage :: 0.0..1.0
Now, you will know that this is not a valid typespec, because I am using 0.0.
The (incorrect) fix there would be to change the spec to:
@type percentage :: 0..1
But this now means I have a range of integers from 0 to 1. I do not want integers, I want floats.
I have also checked the Range.t() option, but this is not what I want. My API requires floats, not an object of type Range.
Yes, it is impossible in current typespecs language. Dialyzer will reduce complexity of every integer range typespec into integer() during checking (that’s how dialyzer works). So you can just write float() with a comment next to it (like float() # from 1.0 to 2.0) without any significant impact on type checking.
For a more detailed explanation, there is this SO answer:
Basically, this all comes down to the type I am trying to create - a dependant type (a type that depends both on the value and type of the parameter). Because here the range of possible values is infinity, this is not possible.
Some type systems have infinite ranges of values. The problem is that Dialyzer’s type system doesn’t. And no, this type is not dependant. The author of SO answer is completely wrong
This has nothing to do with dependent types and it would be trivial for dialyzer and other tools to support this. If we were so inclined we could even support things like :foo .. :bar to cover the range of all atoms from :foo to :bar, or why not {any(), 53, float()} .. {12, atom(), map()} and other arbitrary ranges? There’s nothing stopping us from doing so.
The problem is that Dialyzer’s type system doesn’t.
dialyzer does not have a “type system,” it’s untyped and only reasons about sets of possible values (which may be infinite). That you cannot express arbitrary sets of possible values through @type annotations (@value_constraint would have been a better name) is nothing more than a limitation in the current implementation of the “type language.”
Yes, I meant expressiveness of type language. But dialyzer has a type system, Type system - Wikipedia, it is just pluggable and gradual without any impact on runtime or performance
Can you elaborate on why a function that returns @type percentage :: 0.0..1.0 is not a function returning a dependent type?
From the wikia:
(…) In computer science and logic, a dependent type is a type whose definition depends on a value [in addition to its type] (…)
This makes sense to me. The percentage() type, were it to exist, would depend not only on parameter being a float but also on the value of said float to be between 0.0 .. 1.0.
Can you elaborate as to why percentage() cannot be considered a dependent type?
No, dependent type is a type which depends on the value
For example, if Erlang/Elixir was a statically typed language, maps there would be dependent. When their size is less than 33 items, they use flatmap implementation, while for bigger sizes they use hashmap implementation. So, in this example the type depends on the size of the map
While for float ranges, it is just a range, and it is not a dependant type. It is just a subtype of the float, and that’s all. Like uint is a subtype of int (without maximum integer limit of course), which bounds the integer to always be not less than 0
Sure, but only if we stretch the definition into uselessness. If we look at dialyzer through the lens of it having a type system, values are lifted to the type level which more or less turns everything into a tautology:
“The type of 1 is 1, the type of :foo is :foo.”
“The return type of bar(1234) is the result of bar(1234).”
“The argument types for quux/2 are those for which it produces a value.”
The latter has funny implications for server loops and other code that doesn’t return normally by design. Oh, and as the type of a value is its value, doesn’t that imply that nearly all functions have dependent types? After all, 1 + 2 returns 3 and that’s a type all of its own
Understanding that dialyzer only reasons about sets of possible values is crucial to working with it.
For example, if Erlang/Elixir was a statically typed language, maps there would be dependent. When their size is less than 33 items, they use flatmap implementation, while for bigger sizes they use hashmap implementation. So, in this example the type depends on the size of the map
That detail is hidden and could still be under a dependent type system, perhaps a better example would be list_to_tuple/1 where the arity of the tuple depends of the length of the provided list.
How so? How could I make this work?
By teaching dialyzer that all numbers can have ranges, not just integers. It should be about as simple as making the integer range logic in lib/dialyzer/erl_types.erl allow any kind of number as lower and upper bound and change all uses to match that. That’s what we do in the Erlang compiler (which has a separate implementation of dialyzers underlying algorithm) and it works just fine.
Ok, so I understand from this that my example is a subtype of float and not a dependent type.
A clear case of a dependent type would be list_to_tuple/1 as you mentioned.
This part is now clear to me.
This section however raises several questions. I thought Elixir was compiled to Erlang, which is then compiled into something else.
Shouldn’t then dyalizer know what to do with this?
I feel like I have a knowledge gap in how dialyzer works with Elixir, as I always believed it was the same version for both Elixir and Erlang, and the only “difference” was dialyxir (a wrapper around dialyzer for Elixir).
If Elixir and Erlang use different versions of dialyzer, where can I find them?
If this is the case, why hasn’t Elixir updated its version to that of Erlang in order to support this? (what is the hold-back)
dialyzer doesn’t know how to do this for Erlang either. The Erlang compiler has a separate implementation of the same underlying idea as dialyzer that it uses for optimizing code, which is capable of handling float ranges.
Alright, so if the Erlang compiler has this functionality implemented, why doesn’t dialyzer have it? This would then benefit the entire BEAM ecosystem if such a change were to occur correct?
No one has cared enough to do it, I’m guessing it’s because few people need these kinds of ranges. The compiler has it to be better at optimizing arithmetic, and the whole BEAM ecosystem does benefit from that.
(As an aside, the compiler doesn’t look at @type annotations at all. It only reasons about the code.)
To be more precise, a dependent type is when you can express a quantifier over a value. For example, you can have a type that is represented by all vectors with length of 3.
What typespecs have is singleton types. Those are types that contain a single entry, like the atom :foo, and in our case the type perfectly mirrors a value.
Yes, that’s true. I just didn’t want to dig into formal discussion, and I’ve just provided an example to explain the difference between dependent and independent typing
