Idris 中的隐式参数

Question

我需要一些帮助来解释有关 Idris 中隐式参数的错误消息以及为什么一个小的更改可以修复它。这是代码：

import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n} (x :: xs)
  = let result = myReverse xs ++ [x] in
                 ?rhs

导致此错误：

When checking left hand side of myReverse:
When checking an application of Main.myReverse:
        Type mismatch between
                Vect (S len) elem (Type of x :: xs)
        and
                Vect n elem (Expected type)

        Specifically:
                Type mismatch between
                        S len
                and
                        n

但是，将 {n} 替换为 {n = S len}，代码会进行类型检查。

我认为使用 {n} 只是为了将函数的隐式 n 参数带入作用域。为什么这会导致错误？
错误信息是什么意思？我能想到的唯一解释是类型中的隐式参数 n 由于模式匹配 x::xs 被重写为 S len，并且 Idris 丢失了这些相同的信息。
如何用 {n = S len} 替换它？

Answer 1

在这些情况下，您最好的选择是使用 idris 为您进行编程。如果您从

开始

myReverse : Vect n elem -> Vect n elem
myReverse {n} xs = ?myReverse_rhs

现在在 xs 上进行大小写拆分

myReverse : Vect n elem -> Vect n elem
myReverse {n = Z} [] = ?myReverse_rhs_1
myReverse {n = (S len)} (x :: xs) = ?myReverse_rhs_2

所以 idris 不仅对 xs 进行了 case split，而且对 n 进行了 case split，因为对于空向量，长度必须为 Z，对于非空向量，长度必须至少为 S len。这也意味着 xs 现在的长度为 len。

因为 n 也在你的函数的右边，很明显你需要为 myReverse_rhs_2 提供一些长度为 S len 的东西，当你正确地进行模式匹配时，它等于 n 。

在错误消息中，idris 不知道 n 是什么，因此出现了消息。

Idris 中的隐式参数

Implicit arguments in Idris

idris