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

Question

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

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

我已经把它写在了 Ord 上。 typeclass，尽管您可能需要专门化它。范围要求以等式表示，因此您只需提供 Refl在构建它时，然后将检查该属性。例如: 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 的证明。对于许多临时应用程序来说，这有点过头了，但它确实展示了如何为此目的使用依赖类型。