idris - 为什么 Idris 会给我以下代码的类型不匹配错误？

Question

我是一个尝试学习 Idris 的新手，我想创建一个函数 test，它返回一个 Vector，其类型由函数参数参数化。

vecreplicate : (len : Nat) -> (x : elem) -> Vect len elem
vecreplicate Z     x = []
vecreplicate (S k) x = x :: vecreplicate k x

test : (k:Nat) -> Nat -> Vect k Int
test Z = vecreplicate Z (toIntegerNat Z)
test k = vecreplicate k (toIntegerNat k)

当我尝试使用 Idris 编译代码时，出现以下类型错误

Type mismatch between
    Vect len elem (Type of vecreplicate len x)
and
    Nat -> Vect 0 Int (Expected type)

Specifically:
    Type mismatch between
            Vect len
    and
            \uv => Nat -> uv

为什么会出现此错误？

Answer 1

test : (k:Nat) -> Nat -> Vect k Int 有两个参数，但你只匹配 k。这就是为什么预期类型是 lambda (Nat -> Vect 0 Int)。只需放下一个 Nat:test : (k : Nat) -> Vect k Int。

此外，toIntegerNat 返回 Integer 而不是 Int。 :search Nat -> Int 返回 toIntNat，所以这就是你想在那里使用的内容。