How to typespec a float range in Elixir?

Question

Background

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.

Question

How can I fix my spec so it works?

Answer 1

Elixir can't do that. When you try to restrict a range of float with some literal values in types, which has the infinite possibility, what you're doing is part of "dependent type". A few programming languages support dependent type systems, namely Idris and Agda. Not even Haskell (a language that is really good at type systems) supports dependent type.

The reason that integer fix works is that it's a syntax sugar of finite possibility. Your type declaration is evaluated to something like

@type percentage :: 0|1

But you can't list all the possibilities of float between 0.0 to 1.0 in that way.

In Elixir, you'll check the float range in run time, in other words, function body.