Idris中从Vect获取切片列表出现类型不匹配问题求解

问题原因 #

你遇到的报错不是window函数的逻辑错误，是类型签名的约束和列表推导中i的类型不匹配导致的。
你定义的window函数要求输入Vect的长度必须严格等于i + (m + n)，当你直接写window 0 3 xs时，i是编译期可知的字面量Nat，编译器可以直接推导出n=2，满足0 + 3 + 2 = 5的长度约束，所以可以正常运行。但列表推导中的i来自[0,2]这个List Nat，它的类型是通用的Nat，不会携带具体取值的编译期信息，类型检查阶段没法证明任意的i都满足i + 3 + n = 5，所以会抛出类型不匹配错误。

解决方案 #

方案1：修改window的类型签名，用LTE约束适配任意长度的输入向量

把输入长度约束改为「输入向量长度≥i+m」，借助Idris标准库的LTE（小于等于）类型和auto隐式参数，让编译器自动搜索合法的长度证明：

window : (i : Nat) -> (m : Nat) -> {auto ok : LTE (i + m) len} -> Vect len t -> Vect m t
window i m xs = take m (drop i xs)

修改后你原来的列表推导代码可以直接编译运行，编译器会自动验证i取0、2时都满足i+3 ≤ 5的约束，自动生成对应的证明。

方案2：为遍历的下标打包长度证明

如果你不想修改window的原有类型签名，可以把每个下标和对应的长度证明打包成依赖对再遍历：

-- 定义下标列表，每个元素携带「i+3 ≤5」的证明
indices : List (n : Nat ** LTE (n + (3 + k)) 5)
indices = [0 ** %search, 2 ** %search]

ys : List (Vect 3 Int)
ys = [window i 3 xs | (i ** _) <- indices]

其中%search会让编译器自动生成对应下标符合长度约束的证明，也能通过类型检查。

内容的提问来源于stack exchange，提问作者Alexandru Dinu