Pourquoi seq est-il mauvais ?

Question

Haskell a une fonction magique nommée seq, qui prend un argument de n'importe quel type et le réduit en Forme Normale à Tête Faible (WHNF).

J'ai lu quelques sources [je ne me souviens pas vraiment qui ils étaient maintenant...] qui affirment que "le seq polymorphe est mauvais". En quoi sont-ils "mauvais"?

De même, il y a la fonction rnf, qui réduit un argument en Forme Normale (NF). Mais ceci est une méthode de classe; cela ne fonctionne pas pour tous les types. Il me semble "évident" que l'on pourrait modifier la spécification du langage pour fournir cela comme une primitive intégrée, similaire à seq. Cela, vraisemblablement, serait "encore pire" que d'avoir simplement seq. En quoi est-ce ainsi?

Enfin, quelqu'un a suggéré qu'en donnant aux fonctions seq, rnf, par et similaires le même type que la fonction id, plutôt que la fonction const comme c'est le cas actuellement, ce serait une amélioration. Pourquoi?

Answer 1

Autant que je sache, une fonction polymorphe seq est mauvaise car elle affaiblit les théorèmes libres, ou, en d'autres termes, certaines égalités qui sont valides sans seq ne le sont plus avec seq. Par exemple, l'égalité

map g (f xs) = f (map g xs)

est vraie pour toutes les fonctions g :: tau -> tau', toutes les listes xs :: [tau] et toutes les fonctions polymorphes f :: [a] -> [a]. En gros, cette égalité stipule que f ne peut que réorganiser les éléments de sa liste d'arguments ou supprimer ou dupliquer des éléments mais ne peut pas inventer de nouveaux éléments.

Pour être honnête, il peut inventer des éléments car il pourrait "insérer" une computation non-terminale/une erreur d'exécution dans les listes, étant donné que le type d'une erreur est polymorphe. Autrement dit, cette égalité est déjà fausse dans un langage de programmation comme Haskell sans seq. Les définitions de fonction suivantes fournissent un contre-exemple à l'équation. Essentiellement, du côté gauche, g "cache" l'erreur.

g _ = True
f _ = [undefined]

Pour corriger l'équation, g doit être strict, c'est-à-dire, il doit mapper une erreur sur une erreur. Dans ce cas, l'égalité est à nouveau vérifiée.

Si vous ajoutez un opérateur seq polymorphe, l'équation est de nouveau fausse, par exemple, l'instanciation suivante est un contre-exemple.

g True = True
f (x:y:_) = [seq x y]

Si nous considérons la liste xs = [False, True], nous avons

map g (f [False, True]) = map g [True] = [True]

mais, d'un autre côté

f (map g [False, True]) = f [undefined, True] = [undefined]

Autrement dit, vous pouvez utiliser seq pour faire en sorte que l'élément d'une certaine position de la liste dépende de la définition d'un autre élément dans la liste. L'égalité est à nouveau vérifiée si g est total. Si vous êtes intéressé par les théorèmes libres, consultez le générateur de théorèmes libres, qui vous permet de spécifier si vous considérez un langage avec des erreurs ou même un langage avec seq. Bien que cela puisse sembler avoir moins de pertinence pratique, seq brise certaines transformations qui sont utilisées pour améliorer les performances des programmes fonctionnels, par exemple, la fusion foldr/build échoue en présence de seq. Si vous êtes intéressé par plus de détails sur les théorèmes libres en présence de seq, consultez Théorèmes libres en présence de seq.

Autant que je sache, il avait été connu qu'un seq polymorphe brise certaines transformations lorsqu'il a été ajouté au langage. Cependant, les alternatives ont également des inconvénients. Si vous ajoutez un seq basé sur des classes de types, vous pourriez devoir ajouter de nombreuses contraintes de classe de types à votre programme, si vous ajoutez un seq quelque part en profondeur. De plus, il n'était pas possible de ne pas inclure seq car on savait déjà qu'il y avait des fuites d'espace qui pouvaient être corrigées en utilisant seq.

Enfin, je pourrais ne pas être au courant de quelque chose, mais je ne vois pas comment un opérateur seq de type a -> a fonctionnerait. L'intérêt de seq est qu'il évalue une expression sous forme normale de tête, si une autre expression est évaluée sous forme normale de tête. Si seq a le type a -> a, il n'y a aucun moyen de faire dépendre l'évaluation d'une expression de l'évaluation d'une autre expression.

Answer 2

Un autre contre-exemple est donné dans cette réponse - les monades ne respectent pas les lois des monades avec seq et undefined. Et puisque undefined ne peut être évité dans un langage Turing-complet, celui à blâmer est seq.

Answer 3

L'angoisse autour de Prelude.seq (fréquemment en association avec ⊥) est principalement attribuée à quelques raisons :

1. cela affaiblit l'extensionnalité

    -- (\ x -> f x) == f
   
   seq (\ x -> ⊥ x) y = y
   
   seq ⊥ y = ⊥

2. cela affaiblit la paramétricité

    --  foldr k z (build g) == g k z
   
   foldr ⊥ 0 (build seq) = foldr ⊥ 0 (seq (:) [])
                         = foldr ⊥ 0 []
                         = 0
   
   seq ⊥ 0 = ⊥

3. cela invalide diverses lois, par exemple celles pour l'interface monadique

    --  m >>= return == m
   
   seq (⊥ >>= return :: State s a) True = True
   
   seq (⊥ :: State s a) True = ⊥

Cependant :

1. L'extensionnalité est également affaiblie par la combinaison de la sémantique d'appel par besoin et de l'utilisation de la forme normale de tête faible, comme indiqué par Philip Johnson-Freyd, Paul Downen et Zena Ariola.

2. La paramétricité est également affaiblie par la combinaison de GADTs et des fonctions de map correspondantes satisfaisant aux lois du foncteur, comme démontré par Patricia Johann, Enrico Ghiorzi et Daniel Jeffries.

3. La présence de l'opérateur de point fixe polymorphique :

   yet :: (a -> a) -> a
   yet f = f (yet f)

   impose également des restrictions à la paramétricité, tel que spécifié par Philip Wadler.

4. Établir des lois pour des algorithmes récursifs arbitraires nécessite également de considérer la rigidité, comme expliqué par Maarten Fokkinga (voir chapitre 6).

5. Le fait que certaines combinaisons d'opérateurs et de valeurs puissent invalider des règles logiques ou mathématiques de base n'est pas nouveau, par exemple la division et zéro. Comme pour la division, la rigidité sélective est nécessaire - les algorithmes pour déterminer la rigidité (une propriété non triviale) sont sujets au théorème de Rice : ils peuvent ne pas réussir toujours, entraînant une utilisation inattendue excessive de la mémoire (c'est-à-dire des fuites d'espace) dans les programmes. En ce qui concerne le choix d'utiliser des opérateurs primitifs ou des annotations (pour des patterns ou des types), cela ne change généralement pas l'impact négatif sur les théorèmes et les lois importants.

   Une autre option pourrait être d'utiliser une forme augmentée de la sémantique d'appel par valeur, mais cela suppose que la méthode d'augmentation utilisée soit suffisamment "bien comportée".

---

À un certain moment dans le futur, il y aura peut-être une ou plusieurs avancées dans les sciences informatiques qui résoudront la question. En attendant, l'option la plus pratique est de gérer l'interaction maladroite entre les lois et théorèmes utiles et ceci avec d'autres fonctionnalités de programmation du monde réel.