idris - 将 Nat 保持在固定范围内

Question

我想要一个 Nat保持在一个固定的范围内。我想要函数 incr和 decr如果他们要将数字推到范围之外，则失败。这似乎是 Fin 的一个很好的用例。 ，但我不确定如何使它工作。类型签名可能如下所示:

- Returns the next value in the ordered finite set.
- Returns Nothing if the input element is the last element in the set. 
incr : Fin n -> Maybe (Fin n)

- Returns the previous value in the ordered finite set.
- Returns Nothing if the input element is the first element in the set.
decr : Fin n -> Maybe (Fin n)

Nat将用于索引 Vect n .我该如何实现 incr和 decr ?是 Fin甚至是正确的选择？

Answer 1

我想最简单的方法是使用来自 Data.Fin 的一些标准 Fin↔Nat 转换函数。 :

incr, decr : {n : Nat} -> Fin n -> Maybe (Fin n)
incr {n=n} f = natToFin (succ $ finToNat f) n

decr {n=n} f = case finToNat f of
    Z => Nothing
    S k => natToFin k n