Определение функции flip в Haskell - PullRequest
Новая
       77

Определение функции flip в Haskell

1 голос
/ 10 июня 2019

В настоящее время я пытаюсь изучить Haskell с помощью книги «Learn You a Haskell» и пытаюсь понять реализацию функции flip в главе 5 .Проблема в том, что автор заявляет, что если g x y = f y x является действительным, то f y x = g x y также должно быть истинным.Но как и почему это изменение влияет на два определения функций?

Я знаю, как работает карри, и я также знаю, что оператор -> по умолчанию является ассоциативным справа, поэтому объявления типов фактически одинаковы.Я также понимаю функции отдельно друг от друга, но не знаю, как с этим связано обращение g x y = f y x.

первая функция переворота 

flip' :: (a -> b -> c) -> (b -> a -> c)
flip' f = g
    where g x y = f y x

вторая функция переворота 

flip' :: (a -> b -> c) -> b -> a -> c
flip' f y x = f x y

Ответы [ 2 ]

7 голосов
/ 10 июня 2019

Я думаю, что аргумент, который автор имеет в своей голове, был дико сокращен до такой степени, что он даже не имеет смысла. Но вот мое предположение о рассуждениях. Начнем с первого определения: 

flip f = g where g x y = f y x

Теперь мы видим, что это карри, и мы используем все обсуждение ассоциативности (->) и мусора, чтобы написать то же самое, но с двумя дополнительными аргументами для f. Как это: 

flip f <b>x y</b> = g <b>x y</b> where g x y = f y x

Теперь у нас есть уравнение, которое он назвал следующим образом: g x y = f y x и наоборот. Мы можем переписать тело flip, используя это уравнение, например: 

flip f x y = <b>f y x</b> where g x y = f y x

Поскольку в теле определения больше не упоминается g, мы можем удалить его. 

flip f x y = f y x

И теперь мы в значительной степени там. В окончательном определении автор поменял местами имена x и y. Я не знаю, почему они решили сделать это, но это законный шаг, который вы можете предпринять в эквалайзере, так что никаких проблем нет. Это дает нам их окончательное уравнение: 

flip f y x = f x y
3 голосов
/ 10 июня 2019

flip принимает функцию и возвращает перевернутую версию функции.Одним из способов определения flip' является включение приложения в само определение, поскольку 

flip' f y x = f x y  ===> flip' f y = \x -> f x y
                     ===> flip' f = \y -> \x -> f x y

То есть flip' f - это функция, которая применяет f к своим собственным аргументам в обратном порядке.

Второе определение просто дает сначала анонимной функции \y -> \x -> f x y имя, а затем использует это имя в качестве определения flip' f x y. 

                     ===> flip' f = g where g = \y -> \x -> f x y
                     ===> flip' f = g where g y = \x -> f x y
                     ===> flip' f = g where g y x = f x y

То есть flip' f является некоторой функциейg, где g определено для применения f к аргументам g в обратном порядке.

Определения g x y = f y x и g y x = f x y эквивалентны до альфа-преобразования.В обоих случаях f является свободной переменной в определении g;g является закрытием аргумента f для flip'.

...