Где и почему я должен использовать лишние пустые шаблоны?

Например:

intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy _  [] _     =  []
intersectBy _  _  []    =  []
intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]

Есть дополнительные шаблоны для [] и похоже, что они используются в Haskell Data.List, но что это за оптимизация? И где тут разница с Идрисом?

Я спрашиваю, потому что я слышал, что «это затруднит рассуждения об этом», и у человека, который сказал мне, что не было времени, чтобы полностью объяснить это.

Сомневаюсь, что смогу понять, как это сделать, выполняя "уменьшение доказательства" функции.

Может кто-нибудь объяснить мне политику дополнительных шаблонов здесь с позиций Haskell и Idris, чтобы я мог понять и увидеть разницу.


haskell pattern-matching idris
person cnd    schedule 22.04.2015    source источник

Ответы (4)


arrow_upward
13
arrow_downward

С семантической точки зрения шаблон

intersectBy _  [] _     =  []

выглядит избыточным даже с точки зрения производительности. Вместо этого в Хаскеле

intersectBy _  _  []    =  []

не является избыточным, поскольку в противном случае

intersectBy (==) [0..] []

будет расходиться, так как понимание попытается попробовать все элементы x <- [0..].

Однако я не уверен, что мне нравится этот особый случай. Почему бы нам не добавить специальный случай, охватывающий intersectBy (==) [0..] [2], чтобы он возвращал [2]? Кроме того, если производительность является проблемой, во многих случаях я хотел бы использовать подход O (n log n) посредством предварительной сортировки, даже если это не работает с бесконечными списками и требует Ord a.

person chi    schedule 22.04.2015
comment
Отлично, теперь это имеет смысл! Но как бы вы на самом деле добавили специальный случай, охватывающий intersect (==) [0..] [2] ? - person Sibi; 22.04.2015
comment
почему _ [] _ выглядит лишним? - person cnd; 22.04.2015
comment
@Heather, потому что [x | x <- xs , ...] немедленно оценивается как [], когда xs пусто. - person chi; 22.04.2015
comment
@chi, но пустые регистры используются везде в прелюдии GHC, даже в этой функции (по крайней мере, используются) hs#L436-L440" rel="nofollow noreferrer">github.com/ghc/ghc/blob/ - person cnd; 22.04.2015
comment
@Sibi Например, intersectBy xs [y] = [ y | elem y xs]. Я бы не стал добавлять это в реальный код - это просто для аргумента. - person chi; 22.04.2015
comment
@chi Это недопустимая реализация для intersectBy. Кроме того, что, если на входе будет что-то вроде этого: intersect (==) [2] [0..]. ? Я думаю, именно поэтому этот частный случай не рассматривается. - person Sibi; 22.04.2015
comment
@Heather В других случаях это часто необходимо. Здесь, кажется, это не так. Возможно, авторы той версии Prelude посчитали, что таким образом код следует лучшему стилю — понятия не имею. - person chi; 22.04.2015
comment
@ Сиби, я забыл. Вместо этого используйте intersectBy eq xs [y] = [ y | any (eq y) xs]. Симметричный случай уже обрабатывается последним общим пониманием. Тем не менее, я чувствую, что эти особые случаи делают семантику более сложной и трудной для понимания. Если один список бесконечен, а другой содержит какой-то элемент, не входящий в первый список, пересечение все равно должно расходиться. Создание особых случаев для null, singleton или даже конечных списков кажется мне сложным. - person chi; 22.04.2015
comment
@chi Спасибо за объяснение. Я думаю, что авторы прелюдии могли добавить специальные случаи только для пустого списка при наличии бесконечных списков. Но это только предположение.... :) - person Sibi; 22.04.2015
comment
Я думаю, вы могли бы возразить, что правильное пересечение обязательно завершится, если список любой конечен. Однако это будет не очень красиво, особенно учитывая By и отсутствие порядка. - person dfeuer; 22.04.2015

arrow_upward
11
arrow_downward

Не нужно гадать, когда вы сможете просмотреть историю через git blame, GHC Trac и список рассылки библиотек.

Первоначально определение было только третьим уравнением,

intersectBy eq xs ys    =  [x | x <- xs, any (eq x) ys]

В https://github.com/ghc/ghc/commit/8e8128252ee5d91a73526479f01ace8ba2537667 второе уравнение было добавлено как улучшение строгости/производительности, и в то же время было добавлено первое уравнение, чтобы новое определение всегда было по крайней мере таким же, как исходное. В противном случае intersectBy f [] _|_ будет _|_, когда раньше было [].

Мне кажется, что это текущее определение сейчас максимально ленивое: оно максимально определено для любых входов, за исключением того, что нужно выбирать, левый или правый список сначала проверять на пустоту. (И, как я упоминал выше, этот выбор сделан, чтобы соответствовать историческому определению.)

person Reid Barton    schedule 22.04.2015
comment
Разве добавление intersectBy eq xs [y] = [y | any (eq y) xs] не сделает его еще более определенным, например. intersectBy (==) [0..] [2] ? - person chi; 23.04.2015
comment
@chi, да, я так думаю, и я считаю, что можно использовать этот трюк до конца, гарантируя конечный результат, если любой из аргументов конечен. Но текущая реализация не удаляет дубликаты и не меняет порядок, тогда как ваша удаляет дубликаты, а моя гипотетическая реализация удаляет дубликаты и меняет порядок. - person dfeuer; 23.04.2015
comment
@dfeuer Хорошее замечание по поводу дубликатов - можно утверждать, что мое дополнение меняет семантику оригинала. О том, чтобы использовать трюк полностью: это может быть возможно, но потребует некоторого нетривиального справедливого планирования, поскольку вы не знаете заранее, какой из этих списков является конечным. Кроме того, вам нужно предположить, что конечное является подмножеством другого, поскольку вы не можете проверить, не является ли что-то элементом бесконечного списка. - person chi; 23.04.2015
comment
@chi, хорошее замечание о полуразрешимости. Я забыл об этом! - person dfeuer; 23.04.2015
comment
так что это оптимизация, если я правильно понимаю, но никто еще не объяснил мне возможные проблемы с рассуждениями, к сожалению, пока это добавлено в idris без пустых шаблонов. - person cnd; 23.04.2015

arrow_upward
5
arrow_downward

@chi объясняет случай _ _ [], но _ [] _ также служит цели: он диктует, как intersectBy обрабатывает bottom. С определением, как написано:

λ. intersectBy undefined    []     undefined
[]
λ. intersectBy   (==)    undefined    []
*** Exception: Prelude.undefined

Удалите первый шаблон, и он станет:

λ. intersectBy undefined undefined    []
[]
λ. intersectBy   (==)       []     undefined
*** Exception: Prelude.undefined

Я не уверен в этом на 100%, но я считаю, что отсутствие привязки чего-либо в первом шаблоне повышает производительность. Окончательный шаблон даст тот же результат для xs == [] без оценки eq или ys, но, насколько мне известно, он по-прежнему выделяет пространство стека за их переходы.

person Theodore Lief Gannon    schedule 22.04.2015
comment
Вряд ли, нет. Компилятор удалит неиспользуемые привязки. Это правда, что в некоторых (относительно необычных) обстоятельствах неиспользуемый аргумент будет создан как преобразователь, но это произойдет независимо от того, связан ли он. - person dfeuer; 23.04.2015
comment
Интересно. Таким образом, общий совет не привязывать, если вы его не используете, предназначен только для хорошего стиля, а не для каких-либо технических соображений? - person Theodore Lief Gannon; 23.04.2015
comment
да. Это дает понять читателям, что он не используется. Для неиспользуемых привязок доступно предупреждение компилятора (включено -Wall или -fwarn-unused-binds или чем-то подобным). Это предотвратит случайную забывчивость того, что вы намеревались использовать, если это намерение сигнализируется связыванием имени, которое не начинается с подчеркивания. - person dfeuer; 23.04.2015
comment
Хороший стиль также рекомендует, чтобы аргументы, которые иногда используются, были связаны, если они не используются, с именами, начинающимися с символов подчеркивания. f 0 _x = 3; f _ x = x. Это также, вероятно, эффективный способ запутать программистов Agda, что всегда является хорошей целью. - person dfeuer; 23.04.2015

arrow_upward
4
arrow_downward

В Idris есть большая разница: списки Idris всегда конечны! Кроме того, Idris является в основном строгим (вызовом по значению) языком и необязательно использует средство проверки целостности, поэтому вполне разумно предположить, что в списках аргументов не будет никаких оснований. Значение этой разницы в том, что два определения семантически более близки к Idris, чем к Haskell. Выбор того, что использовать, может быть сделан на основе простоты доказательства свойств функции или может быть основан на простоте.

person dfeuer    schedule 24.04.2015