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}，代码类型检查。

1. 我认为使用 {n} 只是意味着将函数的隐式 n 参数带入作用域。为什么会导致错误？

2. 错误消息是什么意思？我能想到的唯一解释是，由于将x::xs 模式匹配为S len，类型中的隐式参数n 被重写，并且Idris 丢失了这些相同的信息。

3. 用{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 是什么，因此是消息。