无法索引到由递归函数构造的列表

Question

我有一个函数getN'，它应该递归地构造一个包含 n 个元素的列表，但是我认为我做错了什么，因为我无法对其进行索引并且输出看起来出乎意料：

getN' : (Double -> Double -> Double) -> Double -> Double -> Double -> Int -> List Double
getN' f dt t0 y0 0 = []
getN' f dt t0 y0 n = rk4' :: getN' f dt (t0+dt) rk4' (n-1) where
    rk4' = rk4 f dt t0 y0

getN' f 0.1 0 1 100 的输出为：

1.0050062486962987 :: getN' f 0.1 0.1 1.0050062486962987 99 : List Double

这对我来说似乎很陌生。特别是语法 head::tail 很熟悉，但 Idris 通常会在 REPL 中打印出整个结果，这表明在这种情况下有些地方不正确。

index 0 $ getN' f 0.1 0 1 100 的输出为：

(input):1:9:When checking argument ok to function Prelude.List.index:
        Can't find a value of type
                InBounds 0 (getN' f 0.1 0.0 1.0 100)

我在做什么/做错了什么？

Answer 1

getN' 不是全部，因此 REPL 不会评估递归调用（因为它可能永远循环）。设置%default total 或total getN' : … 以从编译器获取警告，或使用:total getN' 签入REPL。 Idris 无法推理 Int，在这种特殊情况下，getN' f 0.1 0 1 -1 不会停止。

如果将Int 替换为Nat，它可以工作（0 到Z，n 到(S n) 和n - 1 到n）。来自another answer：编译器只知道从Integer 中减去1 会得到Integer，但不知道确切的数字（与使用Nat 时不同）。这是因为 Integer、Int、Double 和各种 Bits 的算术是使用 prim__subBigInt 等主要函数定义的。

为什么index 失败：它需要证明InBounds k xs，列表至少有k 元素。在 Haskell 中，!! 较弱，因此会在运行时崩溃：(getN' f 0.1 0 1 100) !! 101 会编译，但会抛出异常。这不可能在伊德里斯发生：

>:t index
Prelude.List.index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} ->  a

>:printdef InBounds
data InBounds : Nat -> List a -> Type where
  InFirst : InBounds 0 (x :: xs)
  InLater : InBounds k xs -> InBounds (S k) (x :: xs)

auto 表示编译器尝试搜索证明ok : InBounds n xs。但是，同样，它不会评估 getN' …，因此它不会找到（甚至搜索）证明。这就是你得到的错误：Can't find a value of type InBounds …