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

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

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