Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
169 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Haskell, théorie des catégories/types

Envoyé par Blincer 
Haskell, théorie des catégories/types
il y a trois années
Bonjour !
Je m'intéresse aux fondements des mathématiques et en particulier à la logique intuitionniste, je programme aussi en Haskell (programmation fonctionnelle) et je cherche à approfondir les bases mathématiques des monoïdes et monades.
J'ai lu que ces concepts venaient de la théorie des catégories mais également de la théorie des types.

Serait-il possible d'avoir des ressources sur le sujet (niveau Maths. Spé), des éclaircissements sur ces théories voir leur rapport avec les fondements des maths et l'informatique ? Et qu'en est-il de la théorie homotopique des types ?

Merci d'avance,



Edité 1 fois. La dernière correction date de il y a trois années et a été effectuée par Blincer.
Re: Haskell, théorie des catégories/types
il y a trois années
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".
Re: Haskell, théorie des catégories/types
il y a trois années
Merci pour ta réponse, je vais regarder ces exercices et essayer de trouver un livre sur ladite correspondance de Curry-Howard. :)
Re: Haskell, théorie des catégories/types
il y a trois années
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).
Re: Haskell, théorie des catégories/types
il y a trois années
@Blincer:

la correspondance de Curry Howard est juste le fait qu'une preuve de maths EST un programme. Je dis "EST" exprès, de manière un peu outrancière. Ce n'est qu'un titre de spécialité, assez large, avec des ramifications et des gens très en désaccord les uns avec les autres parfois.

Les langages comme haskell ou cmal sont dits fonctionnels parce qu'exploitant ça, ils expriment directement la possibilité d'envoyer une fonction de $A\to B$ dans un $C$, etc, autrement dit, tu peux donner sans façon à manger comme paramètre une fonction à une autre fonction. Ca ne va pas plus loin.

Exemple en caml: let f a b c = a ( b c ) ;;

va faire de $f$ l'opération $\circ$ que les matheux définissent plutôt comme suit:

$$ \circ := [ x\mapsto [y\mapsto [z\mapsto x(y(z)) ] ] ]$$

Le typage est un mot "mal choisi" mais qui s'est retrouvé à la mode à la suite de montée en puissance de plusieurs mouvements idéologiques (je ne dis pas s'ils sont "bien ou mal" lol, ce serait trop long.

Pour préciser ce que dit Georges, je confirme ++ ce qu'il dit. Par contre, attention: ma critique sévère est UNIQUEMENT CONTRE le mot "fondatrice". Ces spécialités DEVRAIENT (et se trompent en se trompant de mot) utiliser le mot "unificatrice", car elles sont légitimes et ont fait leurs preuves pour cette qualité: elles tentent d'unifier (et y arrivent avec un taux de réussite honorable au moins).

Mais elles ne fondent évidemment rien du tout, elles sont imbitables pour les béotiens, verbeuses, pas du tout naturelles et réalisent en fait typiquement un programme humain de "réussite à la force du poignet à coups de techniques inspirées ou de coups de génie de certains de leurs membres". En gros, elles roulent avec le frein, et épatent les gens justement parce que malgré le frein, elles atteignent une bonne vitesse.

Cela dit, maitriser haskell ou caml ne nécessite aucunement d'avoir la moindre connaissance en catégories (qui n'ont rien à voir avec justement parce que ces langages ont le bon gout de ne pas infliger l'obligation de typer**).

** ils demandent juste de passer par une petite politesse "typante" de surface probablement (enfin je parle pour caml, je ne sais même pas si haskel s'abaisse à ça) parce qu'ils avaient des visées autres en plus de la programmation (la transmission aux étudiants, la sécurité informatique dans la construction des airbus..), mais tu peux récupérer (par exemple dans caml) la liberté de ne pas typer avec l'ordre suivant:

type toutenUn = blabla options | options | F of (toutenUn->toutenUn)

Et c'est même absolument nécessaire si tu veux profiter des vraies capacités de caml (et j'imagine des autres langages de même nature), le typage ne te donnant accès qu'à des trucs ternes et bien souvent même "consistant".

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Haskell, théorie des catégories/types
il y a trois années
Bonjour,
Peut-être ce livre :
Homotopy type theory
Cordialement,
Diane
Re: Haskell, théorie des catégories/types
il y a trois années
De mon téléphone : j'ai bien vérifié l'absence de malentendu car dans le titre il y a le mot "fondation". Mais non c'est clair que l'auteur des premières pages revendique bien de "fonder les maths" avec son système. C'est incroyable ce qu'on peut devenir bête quand on milite. Il ne s'aperçoit d'ailleurs même pas des bêtises factuelles qu'il dit EN MATHS (entre les pages 6 et 10) mais aussi sociologiques quand il prétend que 99% des matheux n'ont besoin que de peu de consistency strength. Et puis alors la méconnaissance de la TDE manifestée au début du premier chapitre est assez spectaculaire (suivi d'un paragraphe où il prétend que son système "ne type pas"... Pas mal).

C'est vraiment dommage qu'un truc qui a pourtant l'air si bien risque de subir un jour un retour de manivelle pour des exagérations qui ne sont pourtant pas si compromettantes. Bref... on ne peut pas protéger les gens contre eux mêmes. (Dans la liste des auteurs les seuls noms que je connais sont aussi de grands militants de cette idéologie (T.Coquand quand par exemple) du coup je ne peux pas avancer en découvrant par exemple des auteurs reconnus par ailleurs neutres)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Haskell, théorie des catégories/types
il y a trois années
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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Haskell, théorie des catégories/types
il y a trois années
Comme mes deux précédents posts peuvent sembler un peu "politiques", je vais écrire une "critique technique"** du traité mis en lien dans le fil suivant: [www.les-mathematiques.net]. En fait, je vais le résumer (en prétendant que c'est sans perte jusqu'à être contredit, et si je ne le suis pas c'est le sommum de l'humiliation pour ce traité grinning smiley (c'est un jeu, hein! je parle comme dom)).

** ainsi je vais mettre des mots "très formels" sur ce que ma lecture en diagonale lui reproche.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 147 743, Messages: 1 485 038, Utilisateurs: 28 075.
Notre dernier utilisateur inscrit kscaro62.


Ce forum
Discussions: 2 475, Messages: 49 764.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page