Композиция функции Haskell с функцией карты - PullRequest
Новая
       36

Композиция функции Haskell с функцией карты

0 голосов
/ 11 октября 2018

Я просматриваю книгу Ричарда Берда «Мышление функционально с Хаскеллом», и есть раздел, в котором я не могу понять, где он доказывает свойство метода фильтра.Он доказывает: 

filter p . map f = map f . filter (p . f)

Ранее в книге он определяет фильтр следующим образом: 

filter p = concat . map (test p)
test p x = if p x then [x] else []

Вот как он доказывает первое уравнение: 

    filter p . map f
= {second definition of filter} -- He's referring to the definition I gave above
    concat . map (test p) . map f
= {functor property of map}
    concat . map (test p . f)
= {since test p . f = map f . test (p . f)}
    concat . map (map f . test (p . f))
= {functor property of map}
    concat . map (map f) . map (test (p . f))
= {naturality of concat}
    map f . concat . map (test (p . f))
= {second definition of filter}
    map f . filter (p . f)

Я не могу понять, как test p . f равно map f . test (p . f).

Вот как я пытался это проверить: 

test :: (a -> Bool) -> a -> [a]
test p x = if p x then [x] else []

test ((<15) . (3*)) 4 -- test p .f, returns [4]
(map (3*) . test((<15) . (3*))) 4 -- map f . test (p . f), returns [12]

Может кто-нибудь объяснить, что яя здесь скучаю?

Ответы [ 2 ]

0 голосов
/ 11 октября 2018

Ответ HTNW охватывает ваш тестовый пример и способ доказательства уравнения с использованием определения test.Я бы сказал, что все еще существует основной вопрос: откуда мы должны были вывести это уравнение - почему мы должны даже рассматривать возможность того, чтобы оно было правдой?Чтобы ответить на этот вопрос, давайте начнем со второго взгляда на уравнение: 

test p . f = map f . test (p . f)

На словах это говорит о том, что изменение значения осуществляется с помощью некоторой функции f, а затем, с учетом некоторого подходящего предиката p,применение test p к нему аналогично изменению значения после использования test (с предикатом, соответствующим образом модифицированным путем компоновки его с f, чтобы он соответствовал типу неизмененного значения).

Далее, давайте рассмотрим тип test: 

-- I'm adding the implicit forall for the sake of emphasis.
forall a. (a -> Bool) -> a -> [a]

Здесь важно то, что функция с этим типом должна работать при любом выборе a.Если это может быть что-то, мы ничего не знаем об этом заранее при реализации функции с этим типом, например test.Это серьезно ограничивает возможности такой функции: в частности, все элементы списка результатов, если таковые имеются, должны совпадать с предоставленным значением типа a (как мы можем изменить его на что-то другое, не зная его типазаранее?), и предикат должен быть либо проигнорирован, либо применен к тому же значению (к чему бы мы еще применили его?).Принимая это во внимание, то, что говорит уравнение, теперь кажется естественным: не имеет значения, изменим ли мы значения с f до или после test, потому что test не изменит значения самостоятельно.

Один из способов сделать подобные рассуждения строгими - использовать свободные теоремы.Свободная теорема для типа, благодаря параметрическому полиморфизму, гарантированно всегда выполняется для любого возможного значения этого типа, и вам не нужно ничего, кроме типа, чтобы выяснить это.Бывает, что свободная теорема для forall a. (a -> Bool) -> a -> [a] точно равна test p . f = map f . test (p . f).Поскольку я не могу отдать должное предмету в этих коротких строках, вот несколько ссылок о свободных теоремах:

0 голосов
/ 11 октября 2018

Вы проверяли 

test (p . f) = map f . test (p . f)

Что на самом деле неверно.На самом деле это свойство 

test p . f = map f . test (p . f)

Когда LHS ассоциируется как 

test p . f = (test p) . f

Помните, что приложение функции более тесно связано, чем любой определяемый пользователем оператор, действуя так, как будто оно infixl 10.Два идентификатора рядом друг с другом всегда являются частью приложения префиксной функции.(За исключением случая с as-pattern: f xs@ys zs означает f (xs@ys) zs.)

Для доказательства свойства: 

    test p . f
={definition of (.)}
    \x -> test p (f x)
={definition of test}
    \x -> if p (f x) then [f x] else []
={definition of map, multiple times}
    \x -> if p (f x) then map f [x] else map f []
={float map f out of cases}
    \x -> map f (if p (f x) then [x] else [])
={definition of (.)}
    \x -> map f (if (p . f) x then [x] else [])
={definition of test}
    \x -> map f (test (p . f) x)
={definition of (.)}
    map f . test (p . f)

Адаптируя ваш пример, test (<15) . (*3) означает «умножить на3, гарантируя, что результат будет меньше 15. "map (*3) . test ((<15) . (*3)) означает «убедитесь, что трижды введенное значение меньше 15, и, если так, верните трижды введенное значение».

...