Discussion:Type récursif

J’ai plusieurs reproches à faire à cet article :

1. la notation μα.T n’est pas introduite, on ne comprend pas en première lecture ce que ça signifie. Il a fallu que je lise plus bas pour comprendre que c’était un terme façon λ-calcul mais sur les types (avec λ remplacé par μ). Je pense qu’introduire un peu les notations aurait été une bonne chose.
2. les histoires d’iso et d’équi récursivité sont des détails techniques qui pourraient être discutés dans une page à part, mais dans cet article ça fait bizarre. Là encore, j’ai eu du mal à comprendre, faute d’illustrations. Et les notations T[x/y] pour les notations sont à expliciter, quelqu’un qui n’a jamais fait de λ-calcul aura du mal à suivre. D’autant plus que les types récursifs se retrouvent aussi en programmation impérative et que les gens de ce domaine n’ont pas le même background.
3. Comme beaucoup de choses il y a des dualités. Un type de données en soi correspond à une construction et une utilisation. Ici la partie représentation interne est discutée (sa construction), mais pas son emploi, et il y a justement pas mal de choses à dire dessus (comme la récursion bien fondée qui garantit la terminaison, ou son dual, la corécursion qui garantit d’autres propriétés, savoir si une donnée récursive peut se contenir elle même [et donc ne pas être bien fondée], par exemple pour faire des listes circulaires, …).
4. Il y a aussi pas mal de fautes de frappes, je repasserai peut être les corriger quand l’article sera plus avancé

je suis en train de récurer cet article à fond.

1. j’ai essayé d’expliciter la syntaxe (μα.T et T[U/α]) et d’ajouter des exemples. j’espère que c’est plus accessible maintenant.
   à noter qu’il faudrait éviter le double emploi avec l’article « type algébrique » (qui a bien besoin de travail lui aussi). hélas, c’est un peu compliqué de donner des exemples autres (et simples, et pratiques…), sachant que la plupart des langues de programmation restreignent les types récursifs à ceux‐ci (voir la discussion sur l’iso/équi‐récursivité). pour montrer l’équirécursivité dans toute sa généralité, j’envisage un exemple dans la veine de [1], où la problématique est d’écrire (en langage C) une fonction qui se renvoie elle‐même. il me semblerait que ce soit un besoin parfois rencontré dans la nature.
2. je pense que l’iso‐ et l’équi‐récursivité ont leur place dans cet article, qui par nature traite de théorie des types. en plus, ça permet d’expliquer ce qui est permis et interdit dans la plupart des langues. de toute façon, leurs sections respectives sont trop courtes pour en faire des articles séparés. au moins, on peut les laisser sous une section « Théorie » (comme c’est déjà le cas) et rendre l’article plus pratique avec davantage d’exemples concrets.
   on a exactement les mêmes phénomènes en C qu’en Haskell (à savoir que mon exemple ci‐dessus est impossible car un typedef ne peut pas être récursif, mais qu’on peut le contourner en encapsulant la donnée dans une struct), ça pourrait donc être intéressant de montrer aussi de tels exemples en C pour les gens davantage familiers de la programmation impérative ?
3. il me semble que beaucoup de choses que tu dis auraient plutôt leur place dans un article sur les fonctions récursives, non ? ceci dit, il est vrai qu’il faudrait au moins mentionner que ça se traite par des fonctions récursives, et aussi que certaines langues autorisent des définitions récursives de valeurs, menant à des valeurs circulaires. mais je crois que ça concernerait davantage les types algébriques que les types récursifs dans toute leur généralité.
4. fait, normalement.

— Maëlan (discuter) 19 juillet 2016 à 14:28 (CEST)

voilà, j’ai ajouté mon exemple de C. c’est moche,mais que demande le peuple. je m’attaque aux références… — Maëlan (discuter) 19 juillet 2016 à 16:46 (CEST)