dependent-type - 如何在 Idris 中将数字范围指定为类型？

Question

我一直在尝试使用 Idris，似乎应该很简单地指定某种类型来表示两个不同数字之间的所有数字，例如NumRange 5 105 到 10 之间的所有数字的类型。我想包括双精度数/浮点数，但对整数执行相同操作的类型同样有用。我该怎么做呢？

Answer 1

在实践中，您最好根据需要简单地检查边界，但您当然可以编写一个数据类型来强制执行这样的属性。

一种直接的方法是这样的：

data Range : Ord a => a -> a -> Type where
  MkRange : Ord a => (x,y,z : a) -> (x >= y && (x <= z) = True) -> Range y z

我已经在Ordtypeclass 上通用地编写了它，尽管您可能需要对其进行专门化。范围要求表示为一个等式，因此您只需Refl在构造它时提供 a，然后将检查该属性。例如：MkRange 3 0 10 Refl : Range 0 10。这样的事情的一个缺点是必须提取包含的值的不便。当然，如果您想以编程方式构造一个实例，您需要提供边界确实满足的证明，或者在允许失败的某些上下文中执行，例如Maybe.

Nat我们可以毫不费力地为 s 编写一个更优雅的示例，因为对于它们，我们已经有了一个库数据类型来表示比较证明。特别是LTE，表示小于或等于。

data InRange : Nat -> Nat -> Type where
  IsInRange : (x : Nat) -> LTE n x -> LTE x m -> InRange n m

现在这个数据类型很好地封装了 n ≤ x ≤ m 的证明。对于许多临时应用程序来说，这将是矫枉过正，但它肯定显示了您如何为此目的使用依赖类型。