enums - 在 Idris 中，如何将 1 添加到 Fin 直到达到 "max"

Question

我有一个数据类型，它在构造函数中接受一个数字，并且该数字必须介于 1 和 5 之间(表示为 0..4):

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

我想创建一个函数，为现有的星加一，如果它已经是5星，则不执行任何操作

我试过了

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)

但是它没有编译并出现错误:

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

    Specifically:
            Type mismatch between
                    1
            and
                    0

有人可以向我解释为什么会出现此错误吗？以及如何修复它？

Answer 1

Cactus' answer解释问题并给出一种可能的解决方案。不过，由于我们在 Idris 中有依赖类型，我至少会宣传利用它的解决方案的可能性，因此可以被视为更惯用的:

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