Geek Answers Handbook

In Idris, how to add 1 to the fin until the max is reached

I have a data type that accepts a number in the constructor, and this number MUST be between 1 and 5 (represented as 0..4):

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

I want to create a function that adds it to an existing one star, and if it already exists 5 stars, does nothing

I tried

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)

But it does not compile with an error:

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

    Specifically:
            Type mismatch between
                    1
            and
                    0

Can someone explain to me why this error exists? And how to fix it?

+4
source share
4 answers

Finimplements the interface Enumby providing a successor function succwith the desired semantics, which makes the implementation addOneStartrivial:

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

Cactus . , , , , :

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

, Fin . , , nextFin .

, , strengthen with rules, :

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

FS FS : Fin n -> Fin (S n), , x : Fin 5, , 3 : Fin 5, Fin 5, FS Fin 5; Fin 6.

nextFin : Fin n -> Maybe (Fin n), Nothing Fin; Fin, FS . , , FZ : Fin n , n 1 ; FS k k, 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
+3

Other answers directly answered your question. I am here to offer an alternative design.

You say that your number should be from 1 to 5. (It looks like you are building some kind of movie rating system?) Instead of indirectly representing it as a limited natural number from 0 to 4, why not just list a small number of allowed cases directly? You do not need dependent types for this; valid Haskell 98.

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

addOneStar FiveStars = FiveStars
addOneStar s = succ s
0
source

More articles:


All Articles