如何在向量长度上说服 Idris

Question

刚开始使用 Idris（如果重要的话，那就是 Idris 2），偶然发现了这个问题。我正在尝试实现一个函数，该函数返回一个由所有斐波那契数组成的向量，直到给定 n。这是到目前为止的定义（它不编译）：

fibs : (n : Nat) -> Vect (n + 1) Int
fibs Z = [0]
fibs (S Z) = [0, 1]
fibs (S k) =
    case (fibs k) of
        (x :: y :: xs) => (x + y) :: x :: y :: xs

我得到的错误如下：

Can't solve constraint between:
    S (S ?len)
and
    plus ?_ (fromInteger 1)

错误指向表达式(x :: y :: xs)。

我知道我需要向 Idris 证明 fibs k 的长度至少为 2，但我不明白如何做到这一点，以及为什么从现有定义中不明显。对我来说，fibs (S k) 中的 k 肯定必须 >= 1，否则 fibs Z 或 fibs (S Z) 将匹配。 fibs k 的长度，其中k >= 1 因此必须>= 2，根据fibs : (n : Nat) -> Vect (n + 1) Int 的定义。我缺少什么以及如何在 Idris 中表达这一点？

Answer 1

第一个1 + n 比n + 1 更容易推断类型检查器，因为左侧的plus 模式匹配：

> :printdef plus
plus : Nat -> Nat -> Nat
plus 0 right = right
plus (S left) right = S (plus left right)

所以在不知道n的情况下，类型定义中的n + 1不能归约，而1 + n可以归约为S n。

仅此fibs 编译。但是如果你想检查函数是否是总的，你会得到：

> :total fibs
Main.fibs is possibly not total due to:
Main.case block in fibs at test.idr:7:10-17, which is not total as there are missing cases

因为类型检查器不查看其他子句，所以它不知道fibs (S Z) 已经在其他地方处理。因此在fibs (S k) = case (fibs k) of … k 可以是Z，然后结果是Vect (S Z)，在case switch 中没有处理。

但修复和第一个一样简单，只需在 S (S k) 上进行模式匹配：

fibs (S (S k)) = case (fibs (S k)) of
    (x :: y :: xs) => (x + y) :: x :: y :: xs