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

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

Для ясности: я не ищу «безопасное» head , и выбор head , в частности, не является исключительно значимым. Суть вопроса следует за обсуждением head и head ', которые служат для предоставления контекста.

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

В этом примере я говорю о голове .

Как я полагаю, вы знаете,

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

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

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

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

: «Есть веские причины не делать все« безопасным »и создавать исключения при нарушении предусловий»

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

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

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

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

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

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

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

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