Quels sont les points de rigueur de Haskell?

90

Nous savons tous (ou devrions savoir) que Haskell est paresseux par défaut. Rien n'est évalué tant qu'il n'a pas été évalué. Alors, quand faut-il évaluer quelque chose? Il y a des points où Haskell doit être strict. J'appelle ces «points de rigueur», bien que ce terme particulier ne soit pas aussi répandu que je l'avais pensé. Selon moi:

La réduction (ou évaluation) dans Haskell ne se produit qu'aux points de rigueur.

La question est donc: quels sont précisément les points de rigueur de Haskell? Mon intuition dit que main, seq/ modèles bang, pattern matching, ainsi que toute IOaction effectuée par mainles points de strictness primaires, mais je ne sais pas vraiment pourquoi je sais.

( De plus, si elles ne sont pas ce qui appelle des « points », de strictness sont ils appelés?)

J'imagine qu'une bonne réponse inclura une discussion sur WHNF et ainsi de suite. J'imagine aussi que cela pourrait toucher le calcul lambda.


Edit: réflexions supplémentaires sur cette question.

En réfléchissant à cette question, je pense qu'il serait plus clair d'ajouter quelque chose à la définition d'un point de rigueur. Les points de rigueur peuvent avoir des contextes et des profondeurs variables (ou rigueur). Revenant à ma définition selon laquelle «la réduction en Haskell ne se produit qu'aux points de rigueur», ajoutons à cette définition cette clause: «un point de rigueur n'est déclenché que lorsque son contexte environnant est évalué ou réduit».

Alors, laissez-moi essayer de vous lancer sur le genre de réponse que je veux. mainest un point de rigueur. Il est spécialement désigné comme le premier point de rigueur de son contexte: le programme. Lorsque le programme ( mainle contexte du programme) est évalué, le point de rigueur de main est activé. La profondeur de Main est maximale: elle doit être pleinement évaluée. Main est généralement composé d'actions IO, qui sont également des points de rigueur, dont le contexte est main.

Maintenant, vous essayez: discuter seqet faire correspondre les modèles en ces termes. Expliquez les nuances de l'application des fonctions: en quoi est-elle stricte? Comment n'est-ce pas? Et quoi deepseq? letet casedéclarations? unsafePerformIO? Debug.Trace? Définitions de premier niveau? Types de données stricts? Modèles de bang? Etc. Combien de ces éléments peuvent être décrits en termes de seq seulement ou de correspondance de motifs?

Dan Burton
la source
10
Votre liste intuitive n'est probablement pas très orthogonale. Je soupçonne que seqla correspondance des motifs est suffisante, le reste étant défini en fonction de ces éléments. Je pense que la correspondance de motifs assure la rigueur des IOactions, par exemple.
CA McCann
Les primitives, telles que +les types numériques intégrés, forcent également la rigueur, et je suppose que la même chose s'applique aux appels FFI purs.
hammar
4
Il semble y avoir deux concepts confondus ici. La correspondance de modèle et les modèles seq et bang sont des moyens par lesquels une expression peut devenir stricte dans ses sous-expressions - c'est-à-dire que si l'expression supérieure est évaluée, la sous-expression l'est aussi. D'autre part, la principale exécution des actions d'E / S est la façon dont l'évaluation commence . Ce sont des choses différentes, et c'est une sorte d'erreur de type de les inclure dans la même liste.
Chris Smith
@ChrisSmith Je n'essaye pas de confondre ces deux cas différents; si quoi que ce soit, je demande des éclaircissements supplémentaires sur la manière dont ils interagissent. La rigueur se produit d'une manière ou d'une autre, et les deux cas sont importants, bien que différents, des parties de la rigueur "se produisant". (et @ monadic: ಠ_ಠ)
Dan Burton
Si vous voulez / avez besoin d'espace pour discuter d'aspects de cette question, sans tenter une réponse complète, permettez-moi de suggérer d'utiliser les commentaires sur mon / r / haskell post pour cette question
Dan Burton

Réponses:

46

Un bon point de départ est de comprendre cet article: A Natural Semantics for Lazy Evalution (Launchbury). Cela vous dira quand les expressions sont évaluées pour un petit langage similaire au Core de GHC. Ensuite, la question restante est de savoir comment mapper Haskell complet à Core, et la plupart de cette traduction est donnée par le rapport Haskell lui-même. Dans GHC, nous appelons ce processus "désucre", car il supprime le sucre syntaxique.

Eh bien, ce n'est pas toute l'histoire, car GHC comprend toute une série d'optimisations entre le désugarage et la génération de code, et beaucoup de ces transformations réorganiseront le Core afin que les choses soient évaluées à des moments différents (l'analyse de rigueur en particulier entraînera l'évaluation des choses plus tôt). Donc, pour vraiment comprendre comment votre programme sera évalué, vous devez vous pencher sur le Core produit par GHC.

Peut-être que cette réponse vous semble un peu abstraite (je n'ai pas mentionné spécifiquement les motifs de bang ou seq), mais vous avez demandé quelque chose de précis , et c'est à peu près le mieux que nous puissions faire.

Simon Marlow
la source
18
J'ai toujours trouvé amusant que dans ce que GHC appelle "désucre", le sucre syntaxique supprimé inclut la syntaxe réelle du langage Haskell lui-même ... ce qui implique, semble-t-il, que GHC est en réalité un compilateur d'optimisation pour le GHC Langage de base, qui se trouve également inclure un frontal très élaboré pour traduire Haskell en Core. :]
CA McCann
Les systèmes de types ne se machinent pas avec précision cependant ... en particulier mais pas seulement en ce qui concerne la traduction des classes de types en dictionnaires explicites, si je me souviens bien. Et tous les derniers trucs TF / GADT, si je comprends bien, ont encore élargi cet écart.
sclv
GCC n'optimise pas non plus C: gcc.gnu.org/onlinedocs/gccint/Passes.html#Passes
György Andrasek
20

Je reformulerais probablement cette question comme suit : Dans quelles circonstances Haskell évaluera-t-il une expression? (Peut-être clouer sur une "forme normale de tête faible.")

Pour une première approximation, nous pouvons spécifier ceci comme suit:

  • L'exécution des actions d'E / S évaluera toutes les expressions dont elles «ont besoin». (Vous devez donc savoir si l'action IO est exécutée, par exemple son nom est main, ou elle est appelée depuis main ET vous devez savoir ce dont l'action a besoin.)
  • Une expression en cours d'évaluation (hé, c'est une définition récursive!) Évaluera toutes les expressions dont elle a besoin.

À partir de votre liste intuitive, les actions principales et IO entrent dans la première catégorie, et la correspondance séquentielle et la correspondance de modèles entrent dans la deuxième catégorie. Mais je pense que la première catégorie correspond davantage à votre idée de "point de rigueur", car c'est en fait ainsi que nous faisons en sorte que l'évaluation dans Haskell devienne des effets observables pour les utilisateurs.

Donner tous les détails spécifiquement est une tâche importante, car Haskell est un langage de grande taille. C'est aussi assez subtil, car Concurrent Haskell peut évaluer les choses de manière spéculative, même si nous finissons par ne pas utiliser le résultat à la fin: c'est une troisième génération de choses qui provoquent l'évaluation. La deuxième catégorie est assez bien étudiée: vous voulez regarder la rigueur des fonctions impliquées. La première catégorie peut aussi être considérée comme une sorte de «rigueur», bien que ce soit un peu douteux car evaluate xet ce seq x $ return ()sont en fait des choses différentes! Vous pouvez le traiter correctement si vous donnez une sorte de sémantique à la monade IO (passer explicitement un RealWorld#jeton fonctionne pour les cas simples), mais je ne sais pas s'il existe un nom pour ce type d'analyse de rigueur stratifiée en général.

Edward Z. Yang
la source
17

C a le concept de points de séquence , qui sont des garanties pour des opérations particulières qu'un opérande sera évalué avant l'autre. Je pense que c'est le concept existant le plus proche, mais le terme essentiellement équivalent point de rigueur (ou peut-être point de force ) est plus conforme à la pensée de Haskell.

En pratique, Haskell n'est pas un langage purement paresseux: par exemple, la correspondance de motifs est généralement stricte (donc essayer une correspondance de motifs oblige l'évaluation à se produire au moins assez loin pour accepter ou rejeter la correspondance.

Les programmeurs peuvent également utiliser la seqprimitive pour forcer une expression à évaluer indépendamment du fait que le résultat sera jamais utilisé.

$!est défini en termes de seq.

- Paresseux ou non strict .

Donc, votre réflexion sur !/ $!et seqest essentiellement juste, mais la correspondance de modèles est soumise à des règles plus subtiles. Vous pouvez toujours utiliser ~pour forcer la correspondance de modèle paresseux, bien sûr. Un point intéressant de ce même article:

L'analyseur de rigueur recherche également les cas où des sous-expressions sont toujours requises par l'expression externe, et les convertit en évaluation impatiente. Il peut le faire parce que la sémantique (en termes de «bas») ne change pas.

Continuons dans le terrier du lapin et regardons la documentation pour les optimisations effectuées par GHC:

L'analyse de rigueur est un processus par lequel GHC tente de déterminer, au moment de la compilation, quelles données seront définitivement «toujours nécessaires». GHC peut ensuite créer du code pour calculer simplement ces données, plutôt que le processus normal (surcharge plus élevée) pour stocker le calcul et l'exécuter plus tard.

- Optimisations GHC: analyse de rigueur .

En d'autres termes, un code strict peut être généré n'importe où en tant qu'optimisation, car la création de thunks est inutilement coûteuse lorsque les données seront toujours nécessaires (et / ou ne peuvent être utilisées qu'une seule fois).

… Aucune autre évaluation ne peut être effectuée sur la valeur; on dit qu'elle est sous forme normale . Si nous sommes à l'une des étapes intermédiaires afin que nous ayons effectué au moins une évaluation sur une valeur, elle est sous forme normale de tête faible (WHNF). (Il existe aussi une «forme normale de tête», mais elle n'est pas utilisée dans Haskell.) Évaluer complètement quelque chose dans WHNF le réduit à quelque chose sous forme normale ...

- Wikibooks Haskell: Paresse

(Un terme est en forme normale de tête s'il n'y a pas de beta-redex en position de tête 1. Un redex est un redex de tête s'il est précédé uniquement par des abstraits lambda de non-redexes 2. ) Donc, quand vous commencez à forcer un thunk, vous travaillez pour WHNF; quand il n'y a plus de thunks à forcer, vous êtes en forme normale. Autre point intéressant:

… Si, à un moment donné, nous devions, par exemple, imprimer z à l'utilisateur, nous aurions besoin de l'évaluer complètement…

Ce qui implique naturellement que, en effet, toute l' IOaction réalisée à partir main fait l' évaluation de la force, ce qui devrait être évident compte tenu que les programmes Haskell faire, en fait, faire des choses. Tout ce qui doit passer par la séquence définie dans maindoit être dans une forme normale et est donc soumis à une évaluation stricte.

Cependant, CA McCann a bien compris dans les commentaires: la seule chose qui a de la particularité mainest qu'elle mainest définie comme spéciale; la correspondance de motifs sur le constructeur est suffisante pour assurer la séquence imposée par la IOmonade. À cet égard uniquement seqet le pattern-matching sont fondamentaux.

Jon Purdy
la source
4
En fait, la citation "si à un moment donné nous devions, par exemple, imprimer z à l'utilisateur, nous aurions besoin de l'évaluer complètement" n'est pas entièrement correcte. C'est aussi strict que l' Showinstance de la valeur imprimée.
nominolo
10

Haskell n'est pas un langage paresseux purement AFAIK, mais plutôt un langage non strict. Cela signifie qu'il n'évalue pas nécessairement les termes au dernier moment possible.

Une bonne source pour le modèle de «paresseux» de haskell peut être trouvée ici: http://en.wikibooks.org/wiki/Haskell/Laziness

Fondamentalement, il est important de comprendre la différence entre un thunk et la forme normale d'en-tête faible WHNF.

Ma compréhension est que haskell tire les calculs à l'envers par rapport aux langages impératifs. Ce que cela signifie, c'est qu'en l'absence de schémas «seq» et bang, ce sera finalement une sorte d'effet secondaire qui force l'évaluation d'un thunk, ce qui peut à son tour provoquer des évaluations préalables (véritable paresse).

Comme cela conduirait à une horrible fuite d'espace, le compilateur détermine alors comment et quand évaluer les thunks à l'avance pour économiser de l'espace. Le programmeur peut ensuite prendre en charge ce processus en donnant des annotations de rigueur (en.wikibooks.org/wiki/Haskell/Strictness, www.haskell.org/haskellwiki/Performance/Strictness) pour réduire davantage l'utilisation de l'espace sous forme de thunks imbriqués.

Je ne suis pas un expert de la sémantique opérationnelle de haskell, je vais donc laisser le lien comme une ressource.

Quelques ressources supplémentaires:

http://www.haskell.org/haskellwiki/Performance/Laziness

http://www.haskell.org/haskellwiki/Haskell/Lazy_Evaluation

fluquid
la source
6

Paresseux ne veut pas dire ne rien faire. Chaque fois que votre modèle de programme correspond à une caseexpression, il évalue quelque chose - juste assez de toute façon. Sinon, il ne peut pas déterminer quel RHS utiliser. Vous ne voyez aucune expression case dans votre code? Ne vous inquiétez pas, le compilateur traduit votre code en une forme simplifiée de Haskell où ils sont difficiles à éviter.

Pour un débutant, une règle de base est qu'il letest paresseux, casemoins paresseux.

T_S_
la source
2
Notez que bien qu'il caseforce toujours l'évaluation dans GHC Core, il ne le fait pas dans Haskell normal. Par exemple, essayez case undefined of _ -> 42.
hammar
2
casedans GHC Core évalue son argument à WHNF, tandis que casedans Haskell évalue son argument autant que nécessaire pour sélectionner la branche appropriée. Dans l'exemple de hammar, ce n'est pas du tout, mais dans case 1:undefined of x:y:z -> 42, il évalue plus profondément que WHNF.
Max
Et aussi case something of (y,x) -> (x,y)ne doit pas évaluer somethingdu tout. Cela est vrai pour tous les types de produits.
Ingo
@Ingo - c'est incorrect. somethingdevrait être évalué à WHNF pour atteindre le constructeur de tuple.
John L
John - Pourquoi? Nous savons qu'il doit s'agir d'un tuple, alors où est le point de l'évaluer? Il suffit que x et y soient liés au code qui évaluent le tuple et extraient le slot approprié, si jamais ils sont nécessaires.
Ingo du
4

Ce n'est pas une réponse complète visant le karma, mais juste une pièce du puzzle - dans la mesure où il s'agit de sémantique, gardez à l'esprit qu'il existe plusieurs stratégies d'évaluation qui fournissent la même sémantique. Un bon exemple ici - et le projet parle également de la façon dont nous pensons généralement à la sémantique Haskell - était le projet Eager Haskell, qui a radicalement modifié les stratégies d'évaluation tout en conservant la même sémantique: http://csg.csail.mit.edu/ pubs / haskell.html

sclv
la source
2

Le compilateur Glasgow Haskell traduit votre code en un langage de type Lambda-calcul appelé core . Dans ce langage, quelque chose va être évalué, chaque fois que vous le casemodélisez par une déclaration-. Ainsi, si une fonction est appelée, le constructeur le plus extérieur et seulement lui (s'il n'y a pas de champs forcés) va être évalué. Tout le reste est mis en conserve dans un bruit sourd. (Les thunks sont introduits parlet liaisons).

Bien sûr, ce n'est pas exactement ce qui se passe dans la vraie langue. Le compilateur convertit Haskell en Core d'une manière très sophistiquée, rendant paresseux autant de choses que possible et tout ce qui est toujours nécessaire. En outre, il existe des valeurs non encadrées et des tuples toujours stricts.

Si vous essayez d'évaluer une fonction à la main, vous pouvez essentiellement penser:

  • Essayez d'évaluer le constructeur le plus externe du retour.
  • Si quelque chose d'autre est nécessaire pour obtenir le résultat (mais seulement si c'est vraiment nécessaire) sera également évalué. L'ordre n'a pas d'importance.
  • Dans le cas d'E / S, vous devez évaluer les résultats de toutes les déclarations du premier au dernier. C'est un peu plus compliqué, car la monade IO fait quelques astuces pour forcer l'évaluation dans un ordre spécifique.
fuz
la source