Lorsque tu expliques que pour toi le système de types de Go est un « jouet playskool que l'on donne aux enfants », tu ne dis pas que c'est en comparaison du super jouet bien plus fun qu'est le système de types OCaml. Du coup, quelqu'un qui n'a pas une bonne connaissance de l'historique de tes messages va prendre cela dans le sens que le système de types de Go est un jouet à côté de celui de OCaml
Il y a une chose que je ne suis pas dans ce passage de ton commentaire : l'interprétation qu'une personne sans connaissance de l'historique de mes messages est tout à fait correct. Ce système de types est un jouet pour enfant à côté de celui d'OCaml. Je comprends que cela puisse être désagréable à lire, mais c'est bien ce que je pense. Là, c'est le logicien en moi qui s'exprime.
Là logique est une science dont l'objet d'étude est, comme son nom l'indique, le langage. Mais elle ne l'étudie pas à la manière de la linguistique, c'est-à-dire qu'elle ne s'intéresse pas à telle ou telle langues données pour les analyser comparativement dans leurs structures. Si je peut m'exprimer ainsi, ce qu'elle cherche à travers la diversité des langues c'est les invariants par variations. Elle cherche les lois nécessaires de toute pensée, dont le langage n'est que le moyen d'expression. En conséquence, elle n'a pas une approche descriptive comme la linguistique, mais une approche prescriptive et, comme le disait Kant dans le traité qu'il lui a consacré :
La logique est une science rationnelle non seulement selon la forme, mais selon la matière; une science a priori des lois nécessaires de la pensée, non pas relativement à des objets particuliers, mais bien relativement à tous les objets en général; c'est donc une science du droit usage de l'entendement et de la raison en général, non pas de façon subjective, c'est-à-dire selon des principes empiriques (psychologique) : comment l'entendement pense — mais de façon objective, c'est-à-dire selon des principes a priori : comment il doit penser.
Kant, logique.
L'aspect prescriptif se trouve à la fin de la définition qu'il donne de cette science : « comment il doit penser ».
Ensuite, ce que la logique a à apporter à la programmation et à ses langages, ce n'est pas ce calcul assez simple sur les booléens, mais la théorie des types. Les notions centrales de la logique sont celles de concepts, jugement et raisonnement. Par miroir, ces notions en informatique sont celle de types, jugements de typage et dérivation de typage.
Résultat, quand je regarde le système de type de Go, j'ai une logique tellement amputée de certains de ses concepts et principes, que l'ensemble m'apparaît réellement comme un jouet : la logique sous-jacente est simpliste en comparaison de ce que contient la logique. Ce qui n'est absolument pas le cas avec le système de types d'OCaml (ou Haskell). Ce qui est amusant, au passage, c'est qu'il y a une implémentation de ce systèmes en Go : le cœur du langage c'est le système F et celui-ci constitue le langage de configuration Dhall.
Par exemple, ce qui me manque, en premier, c'est l'absence de jugement disjonctif : la totalité de ce dont nous débattons depuis le début (et même avant que j'intervienne sur ce fil de discussion). La disjonction n'est pas une opération qui prend deux booléens puis en retourne un troisième, mais une opération qui prend deux jugements puis en produit un troisième. La première opération apparait lorsque l'on interprète ces jugements selon leur valeur de vérité, et cette notion n'est pas primitive mais dérivée.
Les jugements disjonctifs donne naissance aux types somme (A ou B), là où les jugements conjonctifs donnent naissance aux types produit comme les struct (A et B). Les premiers sont fait pour être utiliser ainsi :
Le caractère propre de tous les jugements disjonctifs, qui détermine, au point de vue de la relation, leur différence spécifique relativement aux autres et particulièrement aux jugements catégoriques, consiste en ce que les membres de la disjonction sont en totalité des jugements problématiques, dont ne peut rien penser d'autre que ceci : étant les parties de la sphère d'une connaissance, chacun complétant l'autre pour former le tout (complementum ad totum), pris ensemble, ils équivalent à la sphère du tout. Il s'ensuit que la vérité doit être contenue dans l'un des jugements problématiques, ou, ce qui revient au même, que l'un d'eux doit avoir valeur assertotique, puisqu'en dehors d'eux, la sphère de la connaissance n'englobe rien sous les conditions données et qu'ils sont opposés les uns aux autres; par suite il n'est possible ni qu'il y ait en dehors un autre jugement qui soit vrai, ni qu'il y en ait plus d'un parmi eux.
Kant, logique.
Afin d'avoir ce qu'exige l'usage logique des jugements disjonctifs (« il n'est possible ni qu'il y ait en dehors un autre jugement qui soit vrai, ni qu'il y en ait plus d'un parmi eux »), il est nécessaire que le langage, via son système de types, fournisse de manière primitive les sommes fermées, puis qu'il vérifie l'exhaustivité de leur usage.
Dans le reste, on peut aussi lui reprocher de ne pas pouvoir faire abstraction des jugements, c'est-à-dire pas de variables de types ou généricité. Il n'y a pas de sous-typage, le cœur de la syllogistique aristotélicienne : tous les animaux sont mortels, tous les hommes sont des animaux, donc tous les hommes sont mortels.1 L'usage des raisonnements hypothétique (si A alors B) est bien présent au niveau des booléens (if then else) mais ne semble pas être mis si en avant que cela, et moins évident à utiliser qu'OCaml, au niveau des types (ici c'est le type des fonction, comme f : int -> float).
Je devrais sans doute pouvoir trouver d'autres choses qui me manquent en creusant un peu le langage, mais cela fait déjà beaucoup trop à mon goût. Autant d'absences qui peuvent difficilement me le faire considérer autrement que comme un jouet, relativement à ce que je chercherais à faire avec, quand bien même cette expression pourrait paraître déplaisante à ces utilisateurs.
c'est la combinaison des type sommes avec sous-typage qui nous permettent d'encoder, ce qui relèvent des types dépendants, les droits de lecture et écriture sur un fichier. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Raisons d'essayer Rust
Posté par kantien . En réponse au journal Retour d'expérience sur les langages de programmation. Évalué à 1.
Il y a une chose que je ne suis pas dans ce passage de ton commentaire : l'interprétation qu'une personne sans connaissance de l'historique de mes messages est tout à fait correct. Ce système de types est un jouet pour enfant à côté de celui d'OCaml. Je comprends que cela puisse être désagréable à lire, mais c'est bien ce que je pense. Là, c'est le logicien en moi qui s'exprime.
Là logique est une science dont l'objet d'étude est, comme son nom l'indique, le langage. Mais elle ne l'étudie pas à la manière de la linguistique, c'est-à-dire qu'elle ne s'intéresse pas à telle ou telle langues données pour les analyser comparativement dans leurs structures. Si je peut m'exprimer ainsi, ce qu'elle cherche à travers la diversité des langues c'est les invariants par variations. Elle cherche les lois nécessaires de toute pensée, dont le langage n'est que le moyen d'expression. En conséquence, elle n'a pas une approche descriptive comme la linguistique, mais une approche prescriptive et, comme le disait Kant dans le traité qu'il lui a consacré :
L'aspect prescriptif se trouve à la fin de la définition qu'il donne de cette science : « comment il doit penser ».
Ensuite, ce que la logique a à apporter à la programmation et à ses langages, ce n'est pas ce calcul assez simple sur les booléens, mais la théorie des types. Les notions centrales de la logique sont celles de concepts, jugement et raisonnement. Par miroir, ces notions en informatique sont celle de types, jugements de typage et dérivation de typage.
Résultat, quand je regarde le système de type de Go, j'ai une logique tellement amputée de certains de ses concepts et principes, que l'ensemble m'apparaît réellement comme un jouet : la logique sous-jacente est simpliste en comparaison de ce que contient la logique. Ce qui n'est absolument pas le cas avec le système de types d'OCaml (ou Haskell). Ce qui est amusant, au passage, c'est qu'il y a une implémentation de ce systèmes en Go : le cœur du langage c'est le système F et celui-ci constitue le langage de configuration Dhall.
Par exemple, ce qui me manque, en premier, c'est l'absence de jugement disjonctif : la totalité de ce dont nous débattons depuis le début (et même avant que j'intervienne sur ce fil de discussion). La disjonction n'est pas une opération qui prend deux booléens puis en retourne un troisième, mais une opération qui prend deux jugements puis en produit un troisième. La première opération apparait lorsque l'on interprète ces jugements selon leur valeur de vérité, et cette notion n'est pas primitive mais dérivée.
Les jugements disjonctifs donne naissance aux types somme (A ou B), là où les jugements conjonctifs donnent naissance aux types produit comme les
struct(A et B). Les premiers sont fait pour être utiliser ainsi :Afin d'avoir ce qu'exige l'usage logique des jugements disjonctifs (« il n'est possible ni qu'il y ait en dehors un autre jugement qui soit vrai, ni qu'il y en ait plus d'un parmi eux »), il est nécessaire que le langage, via son système de types, fournisse de manière primitive les sommes fermées, puis qu'il vérifie l'exhaustivité de leur usage.
Dans le reste, on peut aussi lui reprocher de ne pas pouvoir faire abstraction des jugements, c'est-à-dire pas de variables de types ou généricité. Il n'y a pas de sous-typage, le cœur de la syllogistique aristotélicienne : tous les animaux sont mortels, tous les hommes sont des animaux, donc tous les hommes sont mortels.1 L'usage des raisonnements hypothétique (si A alors B) est bien présent au niveau des booléens (if then else) mais ne semble pas être mis si en avant que cela, et moins évident à utiliser qu'OCaml, au niveau des types (ici c'est le type des fonction, comme
f : int -> float).Je devrais sans doute pouvoir trouver d'autres choses qui me manquent en creusant un peu le langage, mais cela fait déjà beaucoup trop à mon goût. Autant d'absences qui peuvent difficilement me le faire considérer autrement que comme un jouet, relativement à ce que je chercherais à faire avec, quand bien même cette expression pourrait paraître déplaisante à ces utilisateurs.
c'est la combinaison des type sommes avec sous-typage qui nous permettent d'encoder, ce qui relèvent des types dépendants, les droits de lecture et écriture sur un fichier. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.