英文:
How to typespec a float range in Elixir?
问题
背景
我想使用浮点数创建一个百分比类型，类似于：
@type percentage :: 0.0..1.0
现在，你会知道这不是一个有效的类型规范，因为我在使用 0.0。修复这个问题的方法是更改规范为：
@type percentage :: 0..1
但现在这意味着我有一个从0到1的整数范围。我不想要整数，我想要浮点数。
我也已经检查了 Range.t() 选项，但这不是我想要的。我的API需要浮点数，而不是 Range 类型的对象。
问题
如何修复我的规范以使其正常工作？
英文:
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?
答案1
得分: 2
Elixir不能做到这一点。当你尝试在类型中限制一定范围的浮点数与一些字面值在类型中，这涉及到无限可能性，你所做的是"依赖类型"的一部分。有几种编程语言支持依赖类型系统，即Idris和Agda。甚至Haskell（一个非常擅长类型系统的语言）也不支持依赖类型。
整数修复可行的原因是它是有限可能性的语法糖。你的类型声明会被评估为类似于
@type percentage :: 0|1
但你无法以这种方式列出从0.0到1.0之间所有的浮点数可能性。
在Elixir中，你将在运行时检查浮点数范围，换句话说，是在函数体内部。
英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论