有限制类型的语言吗？
有没有一种类型化的编程语言，我可以像下面的两个例子那样约束类型？
概率是一个浮点数，最小值为0.0，最大值为1.0。
type Probability subtype of float
where
max_value = 0.0
min_value = 1.0
离散概率分布是一个映射，其中：键应该都是相同的类型，值都是概率，并且值的总和= 1.0。
type DPD<K> subtype of map<K, Probability>
where
sum(values) = 1.0
据我所知，Haskell或Agda不可能这样做。
你想要的就是所谓的细化类型。
可以在Agda中定义Probability ：Prob.agda
具有总和条件的概率质量函数类型在行264处定义。
有些语言比Agda有更直接的细化类型，例如ATS
你可以在Haskell中用Liquid Haskell做这件事，它用扩展类型扩展了Haskell。 谓词在编译时由SMT解算器管理，这意味着证明是完全自动的，但是您可以使用的逻辑受到SMT解算器处理的限制。 （令人高兴的是，现代SMT解决方案非常灵活！）
一个问题是我不认为Liquid Haskell目前支持浮动。 如果没有，则应该可以纠正，因为SMT解算器有浮点数的理论。 你也可以假装浮点数实际上是有理性的（甚至可以在Haskell中使用Rational ！）。 考虑到这一点，你的第一个类型可能是这样的：
{p : Float | p >= 0 && p <= 1}
你的第二种类型编码会有点困难，特别是因为地图是一种很难解释的抽象类型。 如果您使用的是成对的列表而不是地图，则可以编写如下的“度量”：
measure total :: [(a, Float)] -> Float
total [] = 0
total ((_, p):ps) = p + probDist ps
（您可能想包装[]在newtype了。）
现在你可以使用total在细化约束列表：
{dist: [(a, Float)] | total dist == 1}
Liquid Haskell的巧妙之处在于，所有的推理都是在编译时为你自动完成的，作为使用有限制逻辑的回报。 （喜欢措施total也非常受限于他们如何写，这是哈斯克尔的一小部分包含“每个构造函数只有一个案件”规则）。这意味着，在这种风格的细化类型是那么强大，但更容易使用比全面依赖类型，使它们更实用。
Perl6有一个“类型子集”的概念，它可以添加任意条件来创建一个“子类型”。
具体为你的问题：
subset Probability of Real where 0 .. 1;
和
role DPD[::T] {
has Map[T, Probability] $.map
where [+](.values) == 1; # calls `.values` on Map
}
（注：在当前实现，“何处”部分在运行时检查，但因为“真正的类型”是在编译时检查（包括你的类），由于有纯注释（ is pure ）里面的std（主要是perl6）（这些也在*等操作符上），这只是一个努力的问题（它不应该更多）。
更普遍：
# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")
然后你可以检查一个数字是否与智能匹配算符~~匹配：
say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True
而且，多亏了multi sub （或多个，真的 - 多种方法或其他），我们可以根据这个来调度：
multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don't name the argument, we just put its type
#Also, the last semicolon in a block is optional