如何在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

Ord虽然你可能需要专门化它,但我已经在类型类上编写了它.范围要求表示为等式,因此您只需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的证明.对于许多临时应用程序来说,这将是一种过度杀伤,但它肯定会显示出如何为此目的使用依赖类型.