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