为什么 Idris 给我以下代码的类型不匹配错误？答案

【问题标题】：Why does Idris give me Type mismatch error for the following code?为什么 Idris 给我以下代码的类型不匹配错误？
【发布时间】：2019-08-22 06:43:35
【问题描述】：

我是一个试图学习 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

为什么会出现这个错误？

【问题讨论】：

标签： idris dependent-type

【解决方案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，所以这就是你想在那里使用的。

【讨论】：