有没有一种类型化的编程语言，我可以像下面两个例子那样限制类型？
Is there a typed programming language where I can constrain types like the following two examples?
概率是一个浮动
A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.
type Probability subtype of float
where
max_value = 0.0
min_value = 1.0
离散概率分布是一张图， ：键应该都是相同的类型，值都是概率，值的总和= 1.0。 A Discrete Probability Distribution is a map, where: the keys should all be the same type, the values are all Probabilities, and the sum of the values = 1.0.
据我所知，Haskell或Agda是不可能的。
As far as I understand, this is not possible with Haskell or Agda.
推荐答案称为优化类型。
这是可以在Agda中定义概率： Prob.agda
It's possible to define Probability in Agda: Prob.agda
具有和条件的概率质量函数类型在第264行定义。
The probability mass function type, with sum condition is defined at line 264.
有些语言比Agda有更直接的优化类型，例如 ATS
There are languages with more direct refinement types than in Agda, for example ATS
更多推荐
有限制类型的语言吗？
发布评论