我一直在尝试使用 Idris，似乎应该很简单地指定某种类型来表示两个不同数字之间的所有数字，例如NumRange 5 10 是 5 到 10 之间所有数字的类型。我想包括双精度数/浮点数，但是对整数执行相同操作的类型同样有用。我该怎么做呢？
【问题讨论】：
Ordinal 5 包含从 0 到 4 的所有自然数。
NumRange 5 10 表示为Fin 6，fZ 表示 5，fS fZ 表示 6，以此类推。
标签： dependent-type idris
在实践中，根据需要简单地检查边界可能会更好，但您当然可以编写数据类型来强制执行这样的属性。
一个简单的方法是这样的：
data Range : Ord a => a -> a -> Type where
MkRange : Ord a => (x,y,z : a) -> (x >= y && (x <= z) = True) -> Range y z
我已经在Ord 类型类上通用地编写了它，尽管您可能需要对其进行专门化。范围要求表示为一个等式，因此您只需在构造它时提供Refl，然后将检查该属性。例如：MkRange 3 0 10 Refl : Range 0 10。这样的事情的一个缺点是必须提取包含的值的不便。当然，如果您想以编程方式构建实例，则需要提供确实满足边界的证明，或者在某些允许失败的情况下执行此操作，例如 Maybe。
我们可以毫不费力地为Nats 编写一个更优雅的示例，因为对于它们，我们已经有了一个库数据类型来表示比较证明。特别是LTE，代表小于或等于。
data InRange : Nat -> Nat -> Type where
IsInRange : (x : Nat) -> LTE n x -> LTE x m -> InRange n m
现在这个数据类型很好地封装了 n ≤ x ≤ m 的证明。对于许多临时应用程序来说，这将是多余的，但它肯定显示了您如何为此目的使用依赖类型。
【讨论】：