In Idris, wie man 1 zu einem Fin hinzufügen, bis ein "max" erreicht wird

Question

Ich habe einen Datentyp, der eine Zahl im Konstruktor nimmt, und diese Zahl MUSS zwischen 1 und 5 sein (dargestellt als 0..4):

import Data.Fin 
data Stars = MkStars (Fin 5) 

ich möchte eine Funktion erstellen, die man zu einem bestehenden star hinzuzufügen, und wenn es bereits ein 5 stars, tut nichts

ich versuchte

addOneStar: Stars -> Stars 
addOneStar (MkStars FZ) = MkStars (FS FZ) 
addOneStar (MkStars (FS x)) = if x < 3 
           then MkStars (FS (FS x)) 
           else MkStars (FS x) 

Aber es tun Es kompiliert nicht mit dem Fehler:

Type mismatch between 
      Fin 4 (Type of x) 
    and 
      Fin 3 (Expected type) 

    Specifically: 
      Type mismatch between 
        1 
      and 
        0 

Kann mir jemand erklären, warum gibt es diesen Fehler? Und wie man es repariert?

Answer 1

Fin implementiert die Enum Schnittstelle, die Nachfolgerfunktion succ mit genau der gewünschten Semantik bereitstellt, die die Implementierung von addOneStar trivial macht:

addOneStar: Stars -> Stars 
addOneStar (MkStars s) = MkStars $ succ s 

Answer 2

Der Typ des Konstruktor FS ist FS : Fin n -> Fin (S n), wenn Sie also x : Fin 5 haben, auch wenn Sie wissen, dass es weniger als 3 : Fin 5, seine Art noch Fin 5 ist, so dass Sie es nicht zu FS passieren können und ein Ein Fin 5; Sie erhalten stattdessen eine Fin 6.

Sie können eine Funktion nextFin : Fin n -> Maybe (Fin n) schreiben, die Nothing für die größte Fin zurückgibt; aber diese Funktion muss das neue Fin neu erstellen, es kann nicht einfach FS auf der obersten Ebene anwenden. Die Idee ist, die Tatsache zu nutzen, dass FZ : Fin n entweder einen Nachfolger hat oder nicht, abhängig davon, ob n 1 oder größer ist; und der Nachfolger von FS k ist der Nachfolger von k eingewickelt in FS:

import Data.Fin 

total nextFin : Fin n -> Maybe (Fin n) 
nextFin {n = Z}   k  = absurd k 
nextFin {n = (S Z)}  _  = Nothing 
nextFin {n = (S (S n))} FZ  = Just (FS FZ) 
nextFin {n = (S (S n))} (FS k) = map FS $ nextFin k 

Answer 3

Cactus' answer erklärt das Problem und gibt eine mögliche Lösung. Da wir abhängige Arten in Idris haben, obwohl, würde ich zumindest die Möglichkeit einer Lösung werben, die Verwendung von dem macht und damit als mehr idiomatischen zu sehen:

nextFin : (m : Fin (S n)) -> {auto p : (toNat m) `LT` n} -> Fin (S n) 
nextFin {n = Z} FZ {p} = absurd $ succNotLTEzero p 
nextFin {n = Z} (FS FZ) impossible 
nextFin {n = S k} FZ = FS FZ 
nextFin {n = S k} (FS l) {p} = let p = fromLteSucc p in 
    FS $ nextFin l 

Diese Funktion als Argument, die einen Beweis braucht gegeben Fin ist nicht der letzte. Auf diese Weise können Sie auf der Ebene der Typüberprüfung sicher sein, dass das Programm niemals versucht, Ihnen dafür eine nextFin zu geben.

Wenn Sie nicht wollen, dass, sondern so etwas wie der zitierten Antwort, können Sie auch strengthen zusammen verwenden mit with rules den meisten Fällen zu vermeiden:

nextFin : Fin (S n) -> Maybe $ Fin (S n) 
nextFin m with (strengthen m) 
    | Left k = Nothing 
    | Right k = Just $ FS k 

Answer 4

Die anderen Antworten haben Ihre Frage gerichtet direkt. Ich bin hier, um ein alternatives Design anzubieten.

Sie erwähnen, dass Ihre Nummer zwischen 1 und 5 liegen muss. (Es sieht so aus, als würden Sie ein Filmbewertungssystem erstellen?) Anstatt dies indirekt als natürliche Zahl zwischen 0 und 4 darzustellen, warum nicht einfach die kleine Anzahl der erlaubten Fälle direkt aufzählen? Sie benötigen dafür keine abhängigen Typen. Folgendes ist gültig Haskell 98.

data Stars = OneStar 
      | TwoStars 
      | ThreeStars 
      | FourStars 
      | FiveStars 
      deriving (Eq, Ord, Show, Read, Bounded, Enum) 

addOneStar FiveStars = FiveStars 
addOneStar s = succ s