Pourquoi la fonction `head` de Haskell se plante-t-elle sur une liste vide (ou pourquoi *ne renvoie-t-elle pas* une liste vide) ? (Philosophie des langages)

Question

Note aux autres contributeurs potentiels : N'hésitez pas à utiliser des notations abstraites ou mathématiques pour faire valoir votre point de vue. Si je trouve que votre réponse n'est pas claire, je demanderai des éclaircissements, mais sinon, n'hésitez pas à vous exprimer de manière confortable.

Pour être clair : je suis no à la recherche d'un "coffre-fort" head ni le choix de head en particulier exceptionnellement significatif. L'essentiel de la question suit la discussion sur head y head' qui servent à fournir un contexte.

J'utilise Haskell depuis quelques mois maintenant (au point qu'il est devenu mon langage principal), mais j'admets ne pas être bien informé sur certains des concepts les plus avancés ni sur les détails de la philosophie du langage (bien que je sois plus que désireux d'apprendre). Ma question n'est donc pas tant une question technique (à moins qu'elle ne le soit et que je ne m'en rende pas compte) qu'une question de philosophie.

Pour cet exemple, je parle de head .

Comme vous le savez, j'imagine,

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

Cela découle de head :: [a] -> a . C'est normal. Il est évident que l'on ne peut pas renvoyer un élément qui n'a pas de type. Mais en même temps, il est simple (si ce n'est trivial) de définir

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

J'ai vu quelques petites discussions à ce sujet aquí dans la section des commentaires de certaines déclarations. Notamment, un certain Alex Stangl dit

Il existe de bonnes raisons de ne pas rendre tout "sûr" et de ne pas lever des exceptions lorsque les conditions préalables sont violées.

Je ne remets pas nécessairement en cause cette affirmation, mais je suis curieux de savoir quelles sont ces "bonnes raisons".

En outre, un Paul Johnson dit,

Par exemple, vous pourriez définir "safeHead : : [a] -> Maybe a", mais maintenant, au lieu de gérer une liste vide ou de prouver que cela ne peut pas arriver, vous devez gérer "Rien" ou prouver que cela ne peut pas arriver.

Le ton que je lis dans ce commentaire suggère qu'il s'agit d'une augmentation notable de la difficulté/complexité/quelque chose, mais je ne suis pas sûr de comprendre ce qu'il veut dire.

Un certain Steven Pruzina dit (en 2011, pas moins) ,

"Il y a une raison plus profonde pour laquelle, par exemple, 'head' ne peut pas être à l'épreuve des pannes. Pour être polymorphe tout en gérant une liste vide, 'head' doit toujours retourner une variable du type qui est absent de toute liste vide particulière. Ce serait divin si Haskell pouvait faire cela...".

Le polymorphisme est-il perdu en autorisant la gestion des listes vides ? Si oui, comment, et pourquoi ? Y a-t-il des cas particuliers qui rendraient cela évident ? Cette section a été amplement répondue par @Russell O'Connor. Toute autre réflexion est, bien entendu, la bienvenue.

Je modifierai ce texte en fonction de la clarté et des suggestions. Toute réflexion, tout document, etc., que vous pouvez fournir sera très apprécié.

Answer 1

Est-ce que le polymorphisme est perdu en permettant les vide ? Si oui, comment et pourquoi ? Existe-t-il des cas particuliers qui rendraient qui rendraient cela évident ?

Le théorème libre pour head déclare que

f . head = head . $map f

En appliquant ce théorème à [] implique que

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

Ce théorème doit être valable pour chaque f donc, en particulier, cela doit être vrai pour const True y const False . Cela implique

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

Ainsi, si head est correctement polymorphe et head [] était une valeur totale, alors True serait égal à False .

PS. J'ai d'autres commentaires sur le contexte de votre question, à savoir que si vous avez une condition préalable selon laquelle votre liste n'est pas vide, vous devriez la faire respecter en utilisant un type de liste non vide dans la signature de votre fonction au lieu d'utiliser une liste.

Answer 2

Pourquoi quelqu'un utilise-t-il head :: [a] -> a au lieu de la correspondance des motifs ? L'une des raisons est que vous savez que l'argument ne peut pas être vide et que vous ne voulez pas écrire le code pour gérer le cas où l'argument est vide.

Bien sûr, votre head' de type [a] -> Maybe a est défini dans la bibliothèque standard comme Data.Maybe.listToMaybe . Mais si vous remplacez une utilisation de head con listToMaybe vous devez écrire le code pour gérer le cas vide, ce qui va à l'encontre de l'objectif de l'utilisation de l'option head .

Je ne dis pas qu'utiliser head est un bon style. Il cache le fait qu'il peut entraîner une exception, et en ce sens, il n'est pas bon. Mais il est parfois pratique. Le fait est que head sert certains objectifs qui ne peuvent être atteints par listToMaybe .

La dernière citation de la question (sur le polymorphisme) signifie simplement qu'il est impossible de définir une fonction de type [a] -> a qui renvoie une valeur sur la liste vide (comme l'explique Russell O'Connor dans sa réponse ).

Answer 3

Il est tout à fait naturel de s'attendre à ce que ce qui suit se vérifie : xs === head xs : tail xs - une liste est identique à son premier élément, suivi du reste. Ça semble logique, non ?

Maintenant, comptons le nombre de conses (applications de : ), en faisant abstraction des éléments réels, lorsqu'on applique la prétendue "loi" à [] : [] devrait être identique à foo : bar mais le premier n'a pas de cones, tandis que le second en a (au moins) un. Uh oh, quelque chose ne va pas ici !

Le système de types de Haskell, malgré toutes ses forces, n'est pas en mesure d'exprimer le fait que vous ne devriez appeler head sur une liste non vide (et que la "loi" n'est valable que pour les listes non vides). Utilisation de head déplace la charge de la preuve vers le programmeur, qui devrait s'assurer qu'il n'est pas utilisé sur des listes vides. Je pense que les langages typés de manière dépendante comme Agda peuvent aider ici.

Enfin, une description un peu plus opérationnelle et philosophique : comment devrait-on head ([] :: [a]) :: a être mis en œuvre ? Conjurer une valeur de type a à partir de rien est impossible (pensez aux types inhabités tels que les data Falsum ), et reviendrait à prouver n'importe quoi (via l'isomorphisme de Curry-Howard).

Answer 4

Il y a plusieurs façons de penser à cela. Je vais donc argumenter à la fois pour et contre head' :

Contre head' :

Il n'est pas nécessaire d'avoir head' : Puisque les listes sont un type de données concret, tout ce que l'on peut faire avec les head' que vous pouvez faire par la correspondance de motifs.

En outre, avec head' vous échangez juste un foncteur contre un autre. À un moment donné, vous voulez passer aux choses sérieuses et travailler sur l'élément de liste sous-jacent.

Pour la défense de head' :

Mais la correspondance des modèles masque ce qui se passe. En Haskell, nous sommes intéressés par le calcul de fonctions, ce qui est mieux accompli en les écrivant dans un style sans point, à l'aide de compositions et de combinateurs.

En outre, la réflexion sur le [] y Maybe functeurs, head' vous permet d'aller et venir entre eux (en particulier l'option Applicative exemple de [] con pure = replicate .)

Answer 5

Si, dans votre cas d'utilisation, une liste vide n'a aucun sens, vous pouvez toujours choisir d'utiliser NonEmpty à la place, où neHead est sûr à utiliser. Si vous le voyez sous cet angle, ce n'est pas la head qui n'est pas sûre, c'est la structure de données de la liste entière (encore une fois, pour ce cas d'utilisation).