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]] 

Однако, я запутался, почему конкатенация с лямбда-выражения не может ..?

Answer 1

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

Это где компилятор не может определить значение a. Если вы только что набрали [1,2,3] в REPL, он даст ему тип List Integer. Но [1,2,3] также может быть типа List Int, List Nat или любого другого списка некоторых номеров. Если вы попробуете ваш пример с ['a','b','c'], эта неопределенность исчезает и РЕПЛ примет его с радостью:

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]]) 

В большинстве, но в простейших случаях для унификации требуются некоторые декларации типов. Вот почему (++) работает, но не лямбда-выражение. Первое проще, и последнее имеет абстракцию больше для него (т. Е. Дополнительную функцию).

Но при написании реального кода в файл, компилятор не будет столь же дружественным, как РЕПЛ и будет требовать объявлений типа в любом случае:

-- 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