Le principe même de mon langage était de pousser le principe du typage le plus loin possible, car si il est impossible de "prouver" un code dans le cas général, tu peux prouver beaucoup de choses structurellement. Donc, l'idée était de voir jusqu'où on pouvait aller dans le typage statique.
On peut aller très loin dans le typage statique : Coq !. Mais là, c'est du lourd et c'est violent. :-) En Coq, l'égalité n'est même pas une primitive du langage mais est définie... par le principe des indiscernables de Leibniz.
Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :
letrecl=1::l;;letrecl=1::l;;vall:intlist=[1;<cycle>](* là on attend la fin des temps :-P *)l=l;;
Le principe du typage et de l'inférence de types dans les langages fonctionnels viennent de la théorie de la démonstration, et l'inférence de types c'est de la preuve automatique. Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable (c'est déjà le cas avec les GADT où il faut parfois rajouter des annotations pour que le système d'inférence fonctionne). En Coq, le système est si expressif qu'il faut faire les preuves à la main, le cas général étant indécidable.
Comme on est quand même trolldi et que cette question du principe d'idendité résonne chez moi, je ne peux m'empêcher de citer mon maître :
Unité et diversité. Quand un objet se présente à nous plusieurs fois, mais à chaque fois avec les mêmes déterminations intérieures (qualitas et quantitas), il est, si on le considère comme un objet de l'entendement pur, le même, toujours le même, non pas plusieurs, mais une seul chose (numerica identitas); si au contraire il est phénomène, il ne s'agit plus de comparer des concepts, mais quelque identique que tout puise être à ce point de vue, la diversité des lieux qu'occupe ce phénomène dans un même temps est un principe suffisant de la diversité numérique de l'objet même (des sens). Ainsi, dans deux gouttes d'eau, peut-on faire complétement abstraction de toute diversité intérieure (de qualité et de quantité), et il suffit de les intuitionner en même temps dans des lieux différents pour les regarder comme numériquement diverses. Leibniz prenait les phénomènes pour des choses en soi, par conséquent pour des intelligiblia, c'est-à-dire pour des objets de l'entendement pur (bien qu'il leur donnât le nom de phénomènes, à cause du caractère confus de leur représentation), et alors son principe des indiscernables (principium identitatis indescernabilium) était certainement inattaquable; mais comme ce sont des objets de la sensibilité, et comme l'entendement par rapport à eux n'a pas d'usage pur, mais un usage simplement empirique, la pluralité et la diversité numériques sont déjà indiqué par l'espace même comme condition des phénomènes extérieurs. En effet, un partie de l'espace, quoique parfaitement semblable et égale à une autre, est cependant en dehors d'elle, et elle est précisément par là, par rapport à la première partie, une partie diverse, qui s'ajoute à la précédente pour constituer un espace plus grand, et il doit en être de même, par suite, pour tout ce qui est en même temps en différents de l'espace, quelque semblable et quelque égale que cela puisse être par ailleurs.
Kant, Critique de la raison pure.
D'où la distinction entre les deux prédicats d'égalité en OCaml : égalité structurelle = et égalité physique ==, où la première peut être longue voire ne pas répondre tandis que la seconde répond toujours en temps constant. Cette même distinction, qui a grandement son importance, pourrait même être utile pour fournir une sémantique plus « propre » à la physique quantique de telle sorte que l'on ne dise plus qu'un objet peut être en deux lieux au même instant (soit disant en vertu du principe de superposition).
j'y ai pensé après avoir lu logicomix
J'avais dans l'idée de faire un journal un jour sur cette BD, faudrait peut être que je m'y colle. Si tu l'as lu, il y a un passage dans un restaurant à Paris où Poincaré se moque de Hilbert qui veut fabriquer une machine à faire des théorèmes parce qu'il « aime trop les saucisses » :-P (ce passage vaut bien les gros troll de DLFP ;-). Leibniz en avait eu l'idée et Frege, Russel, Hilbert voulaient mener le programme à bout. Mais Kant, à son époque, avait déjà saisi l'impossibilité de la chose, et Poincaré qui l'avait bien lu était fort sceptique sur la réussite du projet... jusqu'à ce que Gödel mette tout le monde d'accord et donne raison à Kant sur Leibniz ! \o/
Cela étant toutes ces recherches ne furent pas vaines, et c'est pour cela que l'on a l'ordinateur, les langages de programmations, et les théories des types.
Pour revenir à ton problème particulier et ton code, je jetterais peut être un œil dessus si j'ai le temps pour comprendre un peu mieux ce que tu cherches à faire.
c'est plus un "Sont du même type" genre un "~", c'est un blanc dans ma mini syntaxe
Cet article sur le blog de Jane Street te donnera peut être des idées.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par kantien . En réponse au journal EDSL et F-algèbres. Évalué à 1.
On peut aller très loin dans le typage statique : Coq !. Mais là, c'est du lourd et c'est violent. :-) En Coq, l'égalité n'est même pas une primitive du langage mais est définie... par le principe des indiscernables de Leibniz.
Le problème de l'égalité structurelle en OCaml c'est qu'elle peut être indécidable, et partir dans un calcul sans fin :
Le principe du typage et de l'inférence de types dans les langages fonctionnels viennent de la théorie de la démonstration, et l'inférence de types c'est de la preuve automatique. Selon le système de types (sa « puissance » expressive) l'existence d'une preuve d'une assertion peut devenir indécidable (c'est déjà le cas avec les GADT où il faut parfois rajouter des annotations pour que le système d'inférence fonctionne). En Coq, le système est si expressif qu'il faut faire les preuves à la main, le cas général étant indécidable.
Comme on est quand même trolldi et que cette question du principe d'idendité résonne chez moi, je ne peux m'empêcher de citer mon maître :
D'où la distinction entre les deux prédicats d'égalité en OCaml : égalité structurelle
=et égalité physique==, où la première peut être longue voire ne pas répondre tandis que la seconde répond toujours en temps constant. Cette même distinction, qui a grandement son importance, pourrait même être utile pour fournir une sémantique plus « propre » à la physique quantique de telle sorte que l'on ne dise plus qu'un objet peut être en deux lieux au même instant (soit disant en vertu du principe de superposition).J'avais dans l'idée de faire un journal un jour sur cette BD, faudrait peut être que je m'y colle. Si tu l'as lu, il y a un passage dans un restaurant à Paris où Poincaré se moque de Hilbert qui veut fabriquer une machine à faire des théorèmes parce qu'il « aime trop les saucisses » :-P (ce passage vaut bien les gros troll de DLFP ;-). Leibniz en avait eu l'idée et Frege, Russel, Hilbert voulaient mener le programme à bout. Mais Kant, à son époque, avait déjà saisi l'impossibilité de la chose, et Poincaré qui l'avait bien lu était fort sceptique sur la réussite du projet... jusqu'à ce que Gödel mette tout le monde d'accord et donne raison à Kant sur Leibniz ! \o/
Cela étant toutes ces recherches ne furent pas vaines, et c'est pour cela que l'on a l'ordinateur, les langages de programmations, et les théories des types.
Pour revenir à ton problème particulier et ton code, je jetterais peut être un œil dessus si j'ai le temps pour comprendre un peu mieux ce que tu cherches à faire.
Cet article sur le blog de Jane Street te donnera peut être des idées.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.