Объяснение выделки для zipWith ($)

Question

Я пытался понять этот кусок кода, но я не в состоянии обернуть его ясно:

ghci > :t zipWith 
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] 
ghci > :t ($) 
($) :: (a -> b) -> a -> b 
ghci > let c = zipWith ($) 
ghci > :t c 
c :: [b -> c] -> [b] -> [c] 

Как [b -> c] происходят в указанной выше типа подписи ?

Answer 1

для того, чтобы zipWith ($) к typecheck мы должны объединить тип zipWith первый аргумент с типом ($). Я напишу их вместе и с уникальными именами, чтобы сделать его более понятным.

zipWith :: (a  -> b -> c) -> [a]  -> [b] -> [c] 
($)  :: ((x -> y) -> x -> y) 

Таким образом, zipWith typechecks тогда и только тогда, когда мы можем предположить, что a ~ (x -> y), b ~ x и c ~ y. Ничто не останавливает это объединение от успеха, поэтому мы можем заменить эти имена на тип для zipWith.

zipWith :: ((x -> y) -> x -> y) -> [x -> y] -> [x] -> [y] 
($)  :: ((x -> y) -> x -> y) 

А затем приступить к применению, так как все совпадает красиво Сейчас

zipWith ($) :: [x -> y] -> [x] -> [y] 

что эквивалентно до конкретного выбора имен переменных типа с типом вы видели.

Answer 2

Это просто замена контекста и никакой магии. Посмотрите:

ghci > :t zipWith 
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] 
ghci > :t ($) 
($) :: (a' -> b') -> a' -> b' 

Теперь рассмотрим zipWith ($). Он имеет тип (a -> b -> c) -> [a] -> [b] -> [c], где зафиксирован первый аргумент, поэтому мы должны сопоставлять соответствие (a -> b -> c) (тип первого arg) с (a' -> b') -> a' -> b' (тип $). Таким образом, мы имеем a = (a' -> b'), b = a', c = b'. Substitute возвращается к zipWith: [a' -> b'] -> [a'] -> [b'] (первый аргумент фиксирован, поэтому он исчезает из типа), и это именно то, что вы получили с переменными типа, названными по-разному.

Также можно рассмотреть семантику zipWith: возьмите молнию (первый аргумент), а затем запишите два списка вместе. Если ваша застежка-молния является функциональным приложением ($ - это приложение-функция, да!), То при застегивании двух списков вы просто вызываете элементы первого списка с соответствующим элементом второго списка. И тип функции отражает это.

Answer 3

Фактические буквы, присвоенные типу, являются произвольными и могут быть любыми. Вы можете так же легко написать тип ($), как

(x -> y) -> x -> y 

Он принимает два аргумента функция принимает один аргумент, и значение, чтобы передать в функцию.

Первый аргумент zipWith - это функция, принимающая два аргумента (a -> b -> c). Учитывая определение ($), вы выбираете a, как (x -> y) и b, как x то c является y, так что вы получите тип zipWith ($) в

[x -> y] -> [x] -> [y] 

Answer 4

Давайте перепишем немного нашу подпись:

($) :: (a -> b) -> a -> b 
($) :: a' -> b' -> c' 
    where -- pseudo-Haskell 
    a' = a -> b 
    b' = a 
    c' = b 


zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] 

И найти, что

zipWith ($) :: [a'] -> [b'] -> [c'] 

zipWith ($) :: [a -> b] -> [a] -> [b]