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

Question

我有一个数据类型在构造函数中接受一个数字，这个数字必须在 1 到 5 之间（表示为 0..4）：

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

我想创建一个将 1 添加到现有 star 的函数，如果它已经是 5 stars，则不执行任何操作

我试过了

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

构造函数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)让returnsNothing最大Fin；但是该函数必须重建新的 Fin，它不能只在最顶层应用 FS。这个想法是利用 FZ : Fin n 有或没有后继者这一事实，这取决于 n 是否为 1 或更大； FS k 的后继者是包裹在 FS 中的 k 的后继者：

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 2

解释了问题并给出了一种可能的解决方案。不过，由于我们在 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

Answer 3

其他答案已经直接解决了你的问题。我是来提供替代设计的。

你提到你的数字必须在 1 到 5 之间。（看起来你正在构建某种电影评级系统？）而不是间接地将其表示为 0 到 4 之间的有界自然数，为什么不直接列举少数允许的情况？您不需要依赖类型；以下有效 Haskell 98.

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

addOneStar FiveStars = FiveStars
addOneStar s = succ s

Answer 4

Fin 实现 Enum 接口，为后继函数 succ 提供完全所需的语义，这使得 addOneStar 的实现变得简单：

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

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

In Idris, how to add 1 to a Fin until a "max" is Reached

enums

dependent-type

idris