Haskell, théorie des catégories/types

Je ne m'y connais pas trop, mais je pense que c'est difficile de trouver des références qui partent de presque rien (s'il y en a, je serais ravi qu'on me détrompe).

Sur la logique intuitionniste et l'informatique, tu peux essayer de faire les exercices de ce fil : clique ici.

Le mot-clef est "correspondance de Curry-Howard".

Ah et puis j'ai oublié le polycopié d'Alain Prouté qui parle de catégories et de logique (si j'ai bien compris). Il contient sûrement beaucoup d'informations sur les catégories dans la direction que tu semblais vouloir explorer (par contre, bonne chance pour les trouver...). Par contre, a priori, pas de CCH dedans.

Par contre, au sujet de la question des fondements, je ne sais pas si tu vas trouver ton bonheur. Il est vrai que dans ce genre de domaines, certaines personnes et certains textes ont des prétentions fondatrices, mais l'intervenant Christophe C juge très sévèrement ces volontés (cf. une discussion récente dans ce sous-forum, mais je ne sais plus laquelle).

Bonjour,
Peut-être ce livre :
Homotopy type theory
Cordialement,
Diane

Etant sur un PC, je commente plus agréablement que du téléphone. Je viens de le lire en diagonale mais assez longtemps (30mn au moins je pense).

En fait, ça agrège des trivialités bien connues de probablement plusieurs spécialités (pour ce qui sont de mes deux spécialités, il n'y a rien de très pertinent dans cet agrégat, il est même très poussif, puisqu'il est complètement étouffé par la verbosité et ne tient pas compte de découvertes un peu moins introductive qui aurait pu de beaucoup alléger cette terrible montée en notations). J'ai essayé de trouver où l'homotopie jouait un rôle et ... je n'ai pas trouvé.

J'ai l'impression (je bien parcouru la partie homotopique (dans la partie "type" il n'y a rien d'autre que le banal lambda calcul typé)), mais je peux me tromper, que finalement le mot "homotopique" vient de l'inspiration générale donnée par les topologues algébristes (qui font gros usage de constructions de ce genre), mais que les "gros théorèmes" de la topologie algébrique / géométrie différentielle ne jouent pas de rôle. Du coup, je trouve ça un peu "publicité mensongère" pour les béotiens (et même pour les "pas béotiens" puisque moi-même espérais trouver de quoi "rendre évident" la topologie algébrique).

Au final, ça donne juste l'impression d'être un traité qui .... vient "décorer" socialement COQ, pour qu'il n'ait pas l'air de juste implémenter un vérifieur de preuves. Encore une fois je peux me tromper et suis demandeur des pages du livre où il y aurait un scoop (j'ai vraiment cherché).

Pour dire les choses autrement, on a l'impression que les auteurs ne sont pas au courant que la "set theory" et "le lambda calcul", c'est la même chose (les passerelles sont triviales), qu'ils ne sont pas au courant non plus que la TDE, ce n'est pas "spécialement ZF, mais l'originnelle (compréhension générale non bridée) qu'ils le "redécouvrent" comme si c'était révolutionnaire dans un cas très particulier qui le cadre typé (donc faible), commettant du coup la grosse erreur classique habituelle "d'avoir peur de la contradiction" (un peu comme les gens qui s'attardent sur les catégories "pas petites" ou "petites" en croyant la différence importante), erreur qui conduit inéluctablement toute personne qui la commet à se noyer dans des systèmes compliqués puisqu'elle est en même temps à la recherche d'efficacité et de non contradiction, et cette complication "aveugle" et "rend content" de l'escalade accomplie.

Encore une fois, 30mn ne suffisent pas, je me trompe peut-être, mais je connais le sujet et surtout chaque fois que j'ai lu un passage, je tombais sur des "choses bien connues" ou "des erreurs bien connues d'interprétation". Or j'ai pourtant bien l'impression d'avoir feuilleté au hasard, mais ce n'est peut-être pas le cas!!

La partie "homotopie" ne m'a pas semblé contenir de "joyau", ou alors les auteurs ne les ont pas "annoncés" de sorte que je les ai ratés, par contre, j'y ai vu le mot "homotopie" prononcé un très grand nombre de fois.

Lors de prochaines lectures, j'essairai de lire la partie "exemples" (où les auteurs prennent la "vraie topologie algébrique classique" et illustrnent leur propos, peut-être est-ce cette partie que je n'ai pas lue que j'aurais dû lire pour prendre conscience de la valeur de ce travail (ou de cette compilation de travaux).

Quoiqu'il en soit, je maintiens évidemment sans risque de perdre mon pari que l'aspect "fondateur" n'existe évidemment pas (c'est une évidence, il n'y a qu'à proposer la lecture de ce traité à un enfant de 12ans, un enfant honnête et motivé bien sûr et de regarder sa réaction): par définition, "fonder" ça veut dire 5 à 20 lignes de mécanique linguistique (pas 400 pages de traité incompréhensible par d'autres gens que des professionnels aguerris d'abord en topologie et logique).

Par ailleurs, il y a des passages vraiment gravement fautifs sur la TDE, je trouve ça dommage. D'autant que même sans bien la connaitre, les auteurs sont quand-même dans une proximité respectable avec ceux qui s'occupent de topos (qui sont des cas particuliers d'implémentations ensemblistes) à qui ils auraient pu demander ou se faire confirmer qu'il n'y a pas "besoin" d'un $\{vrai; faux\}$ extérieur et que tout se fait à l'intérieur (il n'y a pas de métamathématique extérieure à la TDE (seuls les amateurs le pensent), c'est d'ailleurs pour ça et non pour la consistance de ZF que ZF régit la science.

Les auteurs devraient se ressourcer aux oeuvres de Godel pour re-réaliser qu'il n'est pas possible d'avoir à la fois la fécondité et la consistance garantie, car in fine, c'est bien ça leur principale cause de déviation: ils sont pris en flagrant délit de délaisser le lambda-calcul pur pour le lambda-calcul typé, et ils ont eu de nombreux prédécesseurs à prendre la même fausse route. Je rappelle qu'un OS ne "termine pas" (sauf quand on éteint l'ordi). La course à la "terminaison" semble décidément une "maladie intellectuelle" qui a de beaux jours devant elle.