Поддержание 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