CONCAT在zipWith“没有这样的变量”

Question

使用zipWith与另外像下面的代码，做工精细：

zipWith (\x,y => x + y) [1,2,3] [4,5,6] 

但是，使用连接而不是用列表的两个列表失败：

zipWith (\xs,ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]] 

与错误：

When checking argument x to constructor Prelude.List.::: 
     No such variable a 

我观察到，这是可以做到的以下没有错误：

zipWith (++) [[1],[2],[3]] [[4],[5],[6]] 

不过，我很困惑，为什么用lambda表达式串联失败..？

Answer 1

Idris> :t (++) 
Prelude.List.(++) : List a -> List a -> List a 

这是编译器不能确定的a值。如果您只需在REPL中键入[1,2,3]，则会给它List Integer的类型。但[1,2,3]也可能是List Int,List Nat或某些数字的任何其他列表类型。如果你尝试用['a','b','c']你的榜样，这种不确定性消失和REPL会很乐意接受它：

Idris> zipWith (\xs, ys => xs ++ ys) [['a'],['b'],['c']] [['a'],['b'],['c']] 
[['a', 'a'], ['b', 'b'], ['c', 'c']] : List (List Char) 

您可以通过给类型检查提供信息解决最初的问题：

zipWith (\xs, ys => (++) xs ys {a=Integer}) [[1],[2],[3]] [[4],[5],[6]] 
zipWith (\xs, ys => the (List Integer) (xs ++ ys)) [[1],[2],[3]] [[4],[5],[6]] 
the (List (List Integer)) (zipWith (\xs, ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]]) 

在大多数但最简单的情况是统一需要一些类型的声明。这就是为什么(++)有效，但不是lambda表达式。前者更容易，后者更具抽象性（即额外的功能）。

但在文件中写入实际代码时，编译器会不会像REPL友好反正会要求一个类型声明：

-- test : List (List Integer) 
test = zipWith (\xs, ys => xs ++ ys) [[1],[2],[3]] [[4],[5],[6]] 

Type checking ./test.idr 
test.idr:1:1:No type declaration for Main.test