Почему `head` Хаскелла падает на пустой список (или почему * не * не возвращает пустой список)? (Философия языка)

Question

Примечание для других потенциальных участников: пожалуйста, не стесняйтесь использовать абстрактные или математические обозначения, чтобы высказать свою точку зрения. Если я нахожу ваш ответ неясным, я попрошу разъяснения, но в остальном не стесняйтесь выразить себя удобным способом.

Чтобы быть ясным: я не ищу "сейф" head, и выбор head, в частности, не имеет особого смысла. Суть вопроса следует за обсуждением head и head', которые служат для обеспечения контекста.

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

Для этого примера я говорю о head.

Как я понимаю, вы узнаете,

Prelude> head []    
*** Exception: Prelude.head: empty list

Это следует из head :: [a] -> a. Справедливо. Очевидно, что никто не может вернуть элемент (махнув рукой) никакого типа. Но в то же время просто (если не тривиально) определить

head' :: [a] -> Maybe a
head' []     = Nothing
head' (x:xs) = Just x

Я видел небольшое обсуждение этого здесь в разделе комментариев некоторых утверждений. Примечательно, что один Алекс Штангл говорит

'Есть веские причины не делать все "безопасным" и не создавать исключений при нарушении предварительных условий.'

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

Кроме того, Пол Джонсон говорит,

'Например, вы можете определить «safeHead :: [a] -> Возможно a», но теперь вместо того, чтобы обрабатывать пустой список или доказывать, что это не может произойти, вы должны обработать «Nothing» или доказать, что оно может не бывает.

Тон, который я прочитал из этого комментария, говорит о том, что это заметное увеличение сложности / сложности / чего-то, но я не уверен, что понимаю, что он там излагает.

Один Стивен Прузина говорит (в 2011 году, не меньше),

"Существует более глубокая причина, почему, например, 'head' не может быть защищенным от сбоев. Чтобы быть полиморфным, но обрабатывать пустой список, 'head' всегда должен возвращать переменную типа, который отсутствует в каком-либо конкретном пустом списке. Было бы Delphic, если бы Haskell мог сделать это ... ".

Полиморфизм потерян, если разрешить обработку пустого списка? Если так, то как и почему? Есть ли конкретные случаи, которые сделали бы это очевидным? В этом разделе подробно ответил @Russell O'Connor. Любые дальнейшие мысли, конечно, приветствуются.

Я отредактирую это в соответствии с требованиями ясности и предложения. Любые мысли, документы и т. Д., Которые вы можете предоставить, будут наиболее ценными.

Answer 1

Полиморфизм потерян, если пуст обработка списка? Если так, то как и почему? Существуют ли конкретные случаи, которые сделать это очевидным?

Свободная теорема для head утверждает, что

f . head = head . $map f

Применение этой теоремы к [] подразумевает, что

f (head []) = head (map f []) = head []

Эта теорема должна выполняться для каждого f, в частности, она должна выполняться для const True и const False. Это подразумевает

True = const True (head []) = head [] = const False (head []) = False

Таким образом, если head является должным образом полиморфным, а head [] было общим значением, тогда True будет равно False.

PS. У меня есть некоторые другие комментарии по поводу фона вашего вопроса о том, что если у вас есть предварительное условие, что ваш список не пуст, то вам следует применять его, используя непустой тип списка в сигнатуре функции вместо использования списка.

Answer 2

Почему кто-то использует head :: [a] -> a вместо сопоставления с образцом? Одна из причин в том, что вы знаете, что аргумент не может быть пустым, и не хотите писать код для обработки случая, когда аргумент пуст.

Конечно, ваш head' типа [a] -> Maybe a определен в стандартной библиотеке как Data.Maybe.listToMaybe. Но если вы замените использование head на listToMaybe, вам придется написать код для обработки пустого регистра, что не соответствует этой цели использования head.

Я не говорю, что использование head - это хороший стиль. Он скрывает тот факт, что это может привести к исключению, и в этом смысле это не хорошо. Но это иногда удобно. Дело в том, что head служит некоторым целям, которые не могут быть достигнуты listToMaybe.

Последняя цитата в вопросе (о полиморфизме) просто означает, что невозможно определить функцию типа [a] -> a, которая возвращает значение в пустом списке (как Рассел О'Коннор объяснил в его ответ ).

Answer 3

Естественно ожидать, что будет выполнено следующее: xs === head xs : tail xs - список идентичен первому элементу, за которым следуют остальные.Кажется логичным, верно?

Теперь давайте посчитаем количество conses (приложений :), не учитывая фактические элементы, при применении предполагаемого «закона» к []: [] должно быть идентично foo : bar,но у первого есть 0 conses, в то время как у последнего есть (по крайней мере) один.О-о, что-то здесь не так!

Система типов Хаскелла, несмотря на все ее сильные стороны, не может выразить тот факт, что вы должны вызывать head только в непустом списке (и что 'закон''действительно только для непустых списков).Использование head переносит бремя доказывания на программиста, который должен убедиться, что он не используется в пустых списках.Я полагаю, что здесь могут помочь языки с зависимой типизацией, такие как Agda.

Наконец, чуть более функционально-философское описание: как следует реализовать head ([] :: [a]) :: a?Выдавать значение типа a из воздуха невозможно (представьте себе необитаемые типы, такие как data Falsum), и это будет равносильно доказательству чего-либо (через изоморфизм Карри-Ховарда).

Answer 4

Есть несколько разных способов думать об этом. Поэтому я буду спорить как за, так и против head':

Против head':

Нет необходимости иметь head': поскольку списки представляют собой конкретный тип данных, все, что вы можете сделать с head', вы можете сделать путем сопоставления с образцом.

Кроме того, с head' вы просто меняете один функтор на другой. В какой-то момент вы захотите приступить к медленным трюкам и поработать над базовым элементом списка.

В защиту head':

Но сопоставление с образцом затемняет то, что происходит. В Haskell мы заинтересованы в вычислении функций, что лучше всего сделать, написав их в бессмысленном стиле с использованием композиций и комбинаторов.

Кроме того, думая о функторах [] и Maybe, head' позволяет перемещаться между ними (в частности, Applicative экземпляр [] с pure = replicate.)

Answer 5

Если в вашем случае использование пустого списка вообще не имеет смысла, вы всегда можете выбрать вместо него NonEmpty, где neHead безопасно использовать. Если вы видите это с этой точки зрения, это не небезопасная функция head, а целая структура данных списка (опять же, для этого варианта использования).

Answer 6

Я думаю, что это вопрос простоты и красоты. Что, конечно, в глазах смотрящего.

Если исходить из фона Lisp, вы можете знать, что списки состоят из cons-ячеек, каждая ячейка имеет элемент данных и указатель на следующую ячейку. Пустой список - это не список как таковой, а специальный символ. И Хаскелл соглашается с этим.

На мой взгляд, это и чище, и проще, и более традиционно, если пустой список и список - это две разные вещи.

... Я могу добавить - если вы беспокоитесь о том, что голова небезопасна - не используйте ее, вместо этого используйте сопоставление с шаблоном:

sum     [] = 0
sum (x:xs) = x + sum xs