Wartung eines Nat innerhalb eines festen Bereichs

Question

Ich hätte gerne eine Nat, die innerhalb eines festen Bereichs bleibt. Ich möchte Funktionen incr und decr, die fehlschlagen, wenn sie die Zahl außerhalb des Bereichs schieben werden. Dies scheint, als ob es ein guter Anwendungsfall für Fin wäre, aber ich bin nicht wirklich sicher, wie es funktioniert. Die Art Signaturen könnte wie folgt aussehen:

- 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) 

Die Nat wird Index in ein Vect n verwendet werden. Wie kann ich incr und decr implementieren? Ist Fin dafür die richtige Wahl?

Answer 1

Ich denke, der einfachste Weg, um einige Standards Fin↔Nat Konvertierungsfunktionen von Data.Fin zu verwenden ist:

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