如何在Idris中使用形参（值绑定）进行基础模式匹配？

嘿，这个问题我之前也踩过坑！Idris报的这些推断错误，核心原因是第一个模式匹配里的[]是完全多态的——它的类型是List a，但在这个匹配分支里，没有任何线索能让编译器确定a到底是什么类型（比如是Int、String还是别的）。

让我们拆解一下你的代码：函数contrived的参数是一个五元组，第一个元素是List a，但在第一个匹配分支([] , 'b', (1, 2.0), "hi" , True)里，[]本身没有携带任何关于a的类型信息，而且其他参数的类型（Char、Int、Double等）和a完全无关，编译器自然没法凭空推断出a的类型。

两种可行的解决方案 #

方案1：显式标注空列表的类型

给第一个模式里的[]加上类型注释，直接告诉编译器它属于哪个具体的List类型。如果你只是想匹配空列表，不在乎元素类型，用Void（表示没有值的类型）是个很合适的选择，因为空列表本来就不会有元素：

contrived : (List a, Char, (Int, Double), String, Bool) -> Bool
contrived ([] : List Void , 'b', (1, 2.0), "hi" , True) = False
contrived (a, b, c, d, e) = True

当然你也可以换成其他具体类型，比如List Int，只要符合你的实际需求就行。

方案2：显式绑定类型参数

如果你想让这个分支匹配任意类型的空列表，可以显式绑定函数的类型参数a，告诉编译器不管a是什么，只要元组的其他元素匹配就触发这个分支：

contrived : {a : Type} -> (List a, Char, (Int, Double), String, Bool) -> Bool
contrived ([] , 'b', (1, 2.0), "hi" , True) {a} = False
contrived (a, b, c, d, e) = True

这里的{a}是显式引用函数的类型参数，告诉编译器我们接受任何a类型的空列表来匹配这个分支。

为什么书里的例子没这个问题？ #

你对照Manning的书籍没发现问题，大概率是书里的示例要么：

• 在模式匹配的其他部分用到了和a相关的具体值（比如另一个参数是a类型），让编译器能推断出a；
• 函数的类型参数有明确的约束，或者上下文已经固定了a的类型。

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