kantien a écrit 1131 commentaires

tu as des bug d'intégration, tu a des bug qui apparaissent dans des couches autres du service que tu rend,…

Ça ne change pas le problème : il faut voir la preuve comme la totalité des couches et composants qui composent le service. Peu importe dans quel composant se trouve le bug, ou que celui résulte d'une mauvaise interaction des composants : c'est une erreur dans l'ensemble que constitue la « preuve ». C'est ainsi qu'il faut analyser un système à travers le prisme de la correspondance de Curry-Howard. Quand je parle de preuve ici, ce n'est pas d'une preuve que le système fait ce qu'on attend de lui. C'est le système lui-même que j'identifie à une preuve, et c'est celle-ci qui est erronée s'il y a un bug.

Tu présente une gestion de la portée que tu considère comme une erreur, ce n'est pourtant pas un bug.Ça fait parti de la définition de python et une preuve de l'interpréteur python devra garantir que cette erreur existe.

Non ce n'est pas un bug, ça fait parti de la définition de python, c'est juste un choix quelque peu saugrenu pour un langage qui a commencé au début des années 90.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

il est donc bien plus intéressant d'avoir un langage et un programme qui manipulent des sémantiques triviales plutôt que de perdre beaucoup de monde sur l'autel de la pureté sémantique.

Le problème n'est pas de savoir si la sémantique est triviale ou pure, ou je ne sais quoi; mais que la sémantique affichée en langue naturelle (confusion entre sous-classe et sous-type) ne correspond pas du tout à la sémantique réelle des langages en question. Lorsque l'on dit à quelqu'un qu'une pomme est un fruit, il comprend sans difficulté et cela à un sens très clair pour lui. Par contre quand on lui dit que pour cela il faut faire une classe pomme qui hérite d'une classe fruit : on lui ment ! car alors on traduit sa pensée dans une autre langue sans aucun respect pour la sémantique de sa proposition (la phrase traduite n'a plus le même sens) : traduttore, traditore.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est peut être mathématiquement n'importe quoi, mais cela a une existence informatique.

Je ne dis pas le contraire, mais il y a plein de choses qui existent en informatique mais qui ne devrait pas. Je rêve, par exemple, d'un monde où les bugs dans les logiciels ne serait pas la norme mais l'exception; même d'un monde où les bugs n'existent plus (et je ne suis pas le seul). Un bug ça veut dire un programme qui correspond à une preuve fausse : c'est mal d'écrire des preuves erronées. ;-)

les règles sont aussi faites pour être transgresser, c'est un peu comme cela que l'on avance :)

Certes, mais encore faut-il ne pas faire cela n'importe comment. ;-)

>>> x = 1
>>> def f(y) : return x + y
... 
>>> f(0)
1
>>> x = "foo"
>>> f(0)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 1, in f
TypeError: Can't convert 'int' object to str implicitly
>>>

et là, j'ai ri. :-D
C'est juste une adaptation en python de l'exemple donné dans ce cours en LISP de la fin des années 50. Ça a vite était corrigé, et cette gestion de la portée des variables est considérée comme une erreur depuis les années 60. ;-)

Ceci étant j'ai essayé de redéfinir l'addition sur les entiers, mais ce n'est pas permis.

>>> int.__add__ = lambda x:x
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
TypeError: can't set attributes of built-in/extension type 'int'

Donc au final, je ne vois pas de quoi tu voulais parler. Si c'est du polymorphisme ad-hoc, c'est-à-dire, surchargé un opérateur pour qu'il soit définit aussi sur les int, les string, les float… comme dans :

>>> 1 + 2
3
>>> 1.5 + 3.4
4.9
>>> "foo" + "bar"
'foobar'

alors oui cela correspond à des principes de base des mathématiques, c'est même le degré zéro de l'algèbre moderne. J'en ai parlé ici.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je crois qu'il y a un malentendu : je n'ai pas de problème particulier avec les mixins, ni avec wikipédia (pas au point d'aller corriger ce qui s'y trouve). Mon problème vient de la manière dont sont présentés les principes de la POO tant dans les livres que dans l'enseignement : on y soutient des choses logiquement fausse (que l'on retrouve ensuite sur wikipédia).

Au lieu de prendre un exemple sur wikipédia, j'aurais pu prendre cette discussion sur linuxfr avec le commentaire final de Tonton Th :

C'est quoi le sous-entendu sur les devs Ada ?

C'est que si tu ne fais pas gaffe dès la première minute, tu vas au marché, tu achètes cinq pommes et deux poires, ben quand tu es rentrée chez toi, tu ne sais pas combien de fruits tu as :)

D'autant qu'Ada gère très bien le sous-typage et les problèmes de covariance-contravariance qui y sont associés (en logique, ces notions se ramènent à la distinction entre une raison suffisante et une raison nécessaire).

Ce que je reproche à la POO, c'est de prétendre que pour modéliser ce genre de situation, on va avoir une classe fruit qui aura deux sous-classes pomme et poire : sauf que ce n'est pas du tout cela la relation sémantique entre ces concepts. La relation qu'il y a entre eux est une relation de sous-typage et non de sous-classe. C'est cette relation d'héritage entre classe à laquelle faisait allusion mon extrait de wikipédia : les pommes sont une sorte de fruits. Or quand on dit que les pommes sont une sorte de fruits, on affirme que le type pomme est un sous-type (et non une sous-classe) du type fruit. De la même manière que les femmes sont une sorte d'être humains, ou que les femmes entre 18 et 28 ans sont une sorte de femmes. Et c'est là que l'on revient sur l'intérêt d'étudier les patatoïdes, ou les principes de bases de la logique formelle. ;-)

En gros, la POO mélange allègrement la notion de concepts et de théories sur un concept donné : elle met tout cela dans un gros sac fourre-tout qu'elle appelle classe. Ainsi, comme exemple d'aberration, si l'on ajoute un résultat à une théorie (mais sans changer le moins du monde le concept dont elle parle), c'est-à-dire si l'on rajoute une méthode à une classe donnée, on obtient une autres famille d'objets (une autre classe). Ce qui revient tout bonnement à dire que Archimède ne parlait pas des même cercles qu'Euclide, sous ce très pernicieux prétexte qu'il avait consigné d'autres résultats sur eux que lui. Tout personne normalement constituée trouverait cela inepte, et c'est pourtant ce que l'on dit en permanence quand on fait de la POO.

En POO, notamment avec Python, je peu surcharger les operateurs et dénaturer complétement les fondements de l'arithmétique en ré définissant l'addition la soustraction et tout les opérateurs si je le souhaite.

Existe t il un principe mathématique derrière cela ?

Je ne suis pas sûr de comprendre la question, mais je dirais que cela s'appelle l'art de refuser de se soumettre à de fortes contraintes (principalement en Python) afin de pouvoir écrire à peu près tout et n'importe quoi, mais surtout n'importe quoi. :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'allais te le dire, mais tu m'enlèves les mots de mon clavier … :)
C'est bien d'être lucide :)

La lucidité est essentielle dans la vie, surtout dans ce cas.

En tout cas je te remercie pour tes citations qui m'ont bien plus, apparemment il n'y a pas que les mathématiques qui t'intéresse.

Mes centres d'intérêt, en science, se concentrent essentiellement autour de la mathématique, de la logique formelle et de la philosophie (de tradition kantienne). D'ailleurs pour rester sur le thème du journal et de la fomation NSI, j'ai pu voir que le programme de terminal traite du paradigme de la POO. Le logicien en moi espère une seule chose : que ce sera l'occasion de faire disparaître, une bonne fois pour toute, de la tête de la future génération de programmeurs une des plus grosses inepties logiques qu'il m'ait été donné de voir. Je veux dire celle qu'illustre, par exemple, cet article de wikipédia sur les mixins :

Contrairement à une classe, un mixin n'est pas destiné à être utilisé seul.

Sémantiquement, il n'y a pas de relation « est une sorte de » entre une instance et un mixin.

Non, non et non!!!! les classes sont la pire chose au monde pour représenter cette relation sémantique. C'est la notion de type qui fait cela ! Et cela devient pire lorsque l'on dit que les canards sont des animaux, donc la classe canard doit hériter de la classe animale. Ce que l'on a, en réalité, ce sont deux concepts (ou types) « canard » et « animal » dont l'un est le sous-type de l'autre (l'un se nomme le genre, ici animal, et l'autre l'espèce, ici canard). Le verbe est, que les logiciens nomment dans ce cas copule, correspond au : dans le code que j'ai écrit plus haut :

let vision_du_queutard (l : femme list) = List.map ignore list

L'expression l : femme list se lit « l est une liste de femmes », et les sous classes ne sont pas toujours des sous-types : Subtyping, Subclassing, and Trouble with OOP. Le problème qui arrive dans le cas de l'article est un non respect du principe de substitution de Liskov. Bien que ce principe tire son nom d'un article datant du début des années 1990, il est en réalité connu depuis bien plus longtemps que cela. Ce principe n'est rien d'autre que le dictum de omni et nullo des logiciens qui a reçu cette dénomination latine au moyen âge, et il était déjà connu d'Aristote.

Cela fait donc des années que les adeptes de la POO professent et propagent une ineptie logique qui est connue, comme telle, depuis l'antiquité : il serait peut être temps d'y mettre un terme. ;-)

Pour finir une citation qui revient sur le lien programmation-mathématique :

On est accoutumé à nommer beauté les propriétés évoquées des figures géométriques aussi bien que des nombres […] C'est bien plutôt une démonstration de telles propriétés que l'on serait en droit de nommer belle, parce que, par son intermédiaire, l'entendement comme pouvoir des concepts et l'imagination comme pouvoir de leur présentation a priori se sentent renforcés (ce qui, combiné avec la précision que donne la raison, se nomme l'élégance de la démonstration); car, en tout ceci, du moins la satisfaction, bien que le fondement s'en trouve dans des concepts, est-elle subjective, tandis que la perfection implique une satisfaction objective.

Kant, Critique de la faculté de juger.

Les programmes étant des démonstrations, tout programmeur verra dans ce texte une référence aux sentiments qu'il a pu resentir devant un beau code.  ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Evoquer des listes chainées en parlant de célibataires hommes et femmes de 18 à 28 ans … faut oser … :)

c'est, à peu de chose près, la représentation unaire des entiers naturels.

Et c'est la que je m'aperçois que l'on ne doit pas imaginer les mêmes choses … :)

J'ai écrit cela pour pointer du doigt la relation entre programmation et mathématique. Il ne faut pas oublier que l'objectif de l'option NSI est d'initier les élèves à la programmation, et que l'étude des structure de données (dont les listes chaînées) est au programme de terminale.

Ceci étant, j'ai déjà croisé des personnes pour qui une liste de femmes était un entier unaire : on appelait cela des queutards. ;-)

let vision_du_queutard (l : femme list) = List.map ignore l

Autrement dit, un queutard fait totalement abstraction des femmes sur la liste, mais ne voit en chacune d'elle qu'une croix de plus sur son tableau de chasse : il transforme la liste de femmes en une liste de croix, c'est-à-dire un entier unaire. ;-)

Si j'ai compris : kant dit intelligement ce que Rabelais disait plus simplement :

"Science sans conscience n'est ruine de l'âme"

Non, pas vraiment, il dit juste ici que la philosophie et la mathématique sont deux matières fondamentalement distinctes et que quiconque utilisera la méthode mathématique (définition, axiome et démonstration) en philosophie ne construira que des châteaux de cartes. Ce qui n'est pas le cas en programmation : une API est une axiomatique, programmer contre une interface générique cela revient à faire usage d'axiomes — comme en mathématique.

Après, je ne dis pas qu'il ne faut aborder la programmation que sous l'angle des mathématiques, ni ne pas montrer la plante et le fruit, mais qu'éluder la partie mathématique de la programmation n'est pas une chose à faire.

Il ne faut pas perdre de vue que l'objectif de l'option NSI au lycée est, avant tout, non de former un futur Steve Jobs, mais d'initier à l'informatique et à la programmation celles et ceux qui seront peut être un jour ses ingénieurs.

Ceci étant, je trouve les mathématiques bien plus lumineuse et flamboyante que tout ce qui a jamais pu sortir de la tête d'un Steve Jobs; mais j'ai bien conscience d'avoir une vision ultra-minoritaire au sein de la population. :-P

Les mathématiques ont un triple but. Elles doivent fournir un instrument pour l’étude de la nature.

Mais ce n’est pas tout : elles ont un but philosophique et, j’ose le dire, un but esthétique. Elles doivent aider le philosophe à approfondir les notions de nombre, d’espace, de temps.

Et surtout leurs adeptes y trouvent des jouissances analogues à celles que donnent la peinture et la musique. Ils admirent la délicate harmonie des nombres et des formes ; ils s’émerveillent quand une découverte nouvelle leur ouvre une perspective inattendue ; et la joie qu’ils éprouvent ainsi n’a-t-elle pas le caractère esthétique, bien que les sens n’y prennent aucune part ? Peu de privilégiés sont appelés à la goûter pleinement, cela est vrai, mais n’est-ce pas ce qui arrive pour les arts les plus nobles ?

Henri Poincaré, La valeur de la science

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il y a une coquille dans le paragraphe sur le dépôt github :

cette cet institut

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Tu pourrais prévenir quand tu fais de la mauvaise foi … :)

La programmation c'est :

de la logique mais il y en a de partout comme en philo par exemple
du bon sens … beaucoup de bon sens …
une certaine capacité d'abstraction, comme chez les poêtes par exemple

mais pas autant de mathématique que cela …

Là c'est toi qui est de mauvaise foi. D'une manière générale j'ai du mal à comprendre ton insistance à vouloir dissocier la programmation et les mathématiques. Comme t'a répondu JeanClaude, la science qui formalise tout cela c'est les mathématiques, et le résultat qui constate cela c'est la correspondance de Curry-Howard : un programme est la preuve d'un théorème dont l'énoncé est sa spécification.

L'exemple assez trivial et usuel pour illustrer cela est le théorème énonçant qu'il existe une infinité de nombres premiers. On peut le formuler ainsi : pour tout entier n, il existe un entier p ≥ n tel que p est premier; et comme l'exprime l'énoncé précédent, toute preuve de ce théorème est un algorithme qui prend un entier n en entrée et renvoie un entier p en sortie qui est premier et plus grand que l'entrée.

La différence entre la programmation et la pratique usuelle des mathématiques est que les mathématiciens s'intéressent peu au contenu algorithmique de leurs preuves, contrairement aux programmeurs.

Toutes les structures de données (liste, arbres, graphes…) sont des concepts qui relèvent entièrement de la science mathématique, et d'aucune autre. Par exemple, les listes chaînées (qui pourrait être le type de retour d'une requête SQL pour avoir la liste des femmes ou hommes célibataires de 18 à 28 ans ;-) c'est, à peu de chose près, la représentation unaire des entiers naturels.

J'ai surtout l'impression que tu as une vision réductrice de ce que sont les mathématiques, et ce n'est pas réduire la programmation que de l'identifier aux mathématiques, mais réduire les mathématiques dans leur contenu que de nier cette identité. Quand tu parles de sinusoïdales ou de recherche dichotomique, cela ne concerne qu'une infime partie de ce que traite et contient la mathématique. Pour comparer à la géographie, c'est un peu comme si tu me disais que la surface du globe se réduit à l'Ile de France, mais que l'Andalousie ou la pampa argentine étaient des régions inexistantes.

On pourra plutôt envisager les choses dans l'autre sens, comme le suggérait JeanClaude :

on peut envisager les choses autrement et imaginer que l'informatique peut donner des angles d'enseignements différents et bien plus concrets aux mathématiques.

Soit dit en passant, tu te contredis quelque peu au fil des commentaires. Les patatoïdes ce n'est pas des plaisanteries mathématiques, mais de la logique : cela sert à représenter, de manière sensible, les différents rapports entre l'extension de plusieurs concepts, rapports qui relèvent de la logique formelle. Or la logique est la première des composantes de la programmation, d'après ta liste, mais il ne faudrait pas en parler dans les cours ? C'est un peu étrange comme approche de l'enseignement. ;-)

Pour finir, tu as sous-entendu que la philosophie pouvait se ramener aux mathématiques, sauf que c'est absolument faux.

il est nécessaire d'enlever encore en quelque sorte sa dernière ancre à une espérance fantastique, et de montrer que l'application de la mathématique dans cette sorte de connaissance ne peut procurer le moindre avantage, si ce n'est peut être de lui découvrir plus clairement ses propres faiblesses; que la géométrie et la philosophie sont deux choses tout à fait différentes bien qu'elles se donnent la main dans la science de la nature, et que par conséquent le procédés de l'une ne peuvent être imités par l'autre.

La solidité des mathématiques repose sur des définitions, des axiomes et des démonstrations. Je me contenterai de montrer qu'aucun des ces éléments ne peut être ni fourni ni imité par la philosophie dans le sens où les mathématiciens le prend; que le géomètre, en suivant sa méthode, ne construirait, dans la philosophie, que des châteaux de cartes; que le philosophe, en suivant la sienne dans le domaine de la mathématique, ne pourrait faire naître que du verbiage; encore que la philosophie tienne son rôle dans cette science, rôle qui est d'en connaître les limites, et que le mathématicien lui-même, quand son talent n'est pas déjà limité par la nature et restreint à sa partie, ne puisse pas rejeter les avertissements de la philosophie, ni encore se mettre au-dessus d'eux.

Kant, Critique de la raison pure.

Ce qui distingue, entre autre, la mathématique et la philosophie, est que la philosophie est la connaissance rationnelle par concepts là où la mathématique est la connaissance rationnelle par la construction des concepts. Or, construire un concept, c'est présenter a priori l'intuition qui lui correspond; c'est-à-dire présenter, dans nos deux formes de l'intuition sensible que sont l'espace et le temps, un objet qui correspond à notre concept. Autrement dit, la notion de type en informatique est un synonyme de celui de concept mathématique, c'est-à-dire de concept dont les objets sont construits a priori dans l'espace et dans le temps (les deux notions centrales de la complexité algorithmique).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Il paraît que Facebook a une alternative dérivée d'ocaml.

Oui, c'est le langage Reason. Par contre ce n'est pas dérivée de OCaml, c'est du OCaml mais avec une syntaxe à la javascript. Dinosaure en avait fait une présentation lors de la dépêche sur les sorties 4.04 et 4.05 de OCaml (au passage le choix de l'image pour illustrer n'est pas de moi, mais de lui ;-) et pour le citer :

Reason n’est ni plus ni moins qu’une option dans le compilateur. Nous parlons ici de l’option -pp qui permet de remplacer la partie frontale du compilateur par un préprocesseur ad hoc. Le préprocesseur Reason prend donc du code Reason en entrée, le transforme en arbre de syntaxe abstrait OCaml et passe cet arbre au compilateur OCaml classique.

Il est tout à fait possible de mélanger du code Reason et du code OCaml : c'est le même langage mais avec deux syntaxes concrètes distinctes. On peut compiler du Reason en natif ou vers du bytecode OCaml. Pour la compilation vers javascript, la communauté Reason utilise le backend bucklescript, mais il en existe un autre plus ancien (quant à l'origine, il est toujours actif et surtout utilisé par les personnes de la communauté OCaml) à savoir js_of_ocaml.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

En fait je crois qu’on devrait s’en foutre un peu, excusez-moi le langage. Je ne pense pas que c’est un problème de se dire que Kant aurait pu dire une connerie monumentale en disant que l’infanticide ne serait pas un crime du même niveau qu’un assassinat d’adulte. Je crois qu’il a lui aussi le droit à la connerie.

Je crois qu'il y'a méprise sur mon intention. Ma volonté était simplement de remettre un peu d'ordre sur la vérité de ce qu'à pu dire Kant sur certain sujet. La question de l'infanticide était présentée de telle manière, dans la vidéo, que cela pouvait faire dire à Kant le contraire de ce qu'il avait dit : il me fallait rétablir la vérité sur ce point.

Mais Kant n'était pourtant pas un être parfait (la perfection n'est pas humaine, seule la perfectibilité est dans notre nature) et il avait bien des préjugés de son époque : il était patriarcal (la gestion du foyer doit revenir à l'homme du fait de sa supériorité naturelle sur la femme pour la gestion de cette charge), quelques peu raciste (mais certainement pas au point que le laisse entendre la vidéo), homophobe (l'homosexualité masculine n'est pas seulement immorale, elle doit être punie de castration) et j'en passe…

Ceci étant, j'admire tout de même cette homme pour son œuvre philosophique et elle n'a rien à souffrir des ses prises de positions précédentes : il est tout à fait possible d'ếtre kantien aujourd'hui, même sur le plan de philosophie pratique (droit et éthique), sans partager ces positions (même celle sur la masturbation ;-). C'est là aussi un point qui m'a dérangé dans cette vidéo : la morale kantienne se résumerait à celle d'un prussien piétiste du 18ème siècle, n'aurait pas grand chose d'universelle et serait de peu de valeur aujourd'hui.

Un jugement superficiel, habitué à conclure un peu trop rapidement et sans fondement, pourrait certes arriver à une telle conclusion en partant des exemples et de la présentation de la vidéo, mais il n'en est rien. Tout ceci n'est que des faits sans importance, sans aucune incidence, sur le cœur, et ce qui constitue l'essence, de la morale kantienne : l'impératif catégorique.

Agis de telle sorte que la maxime de ta volonté puisse valoir comme principe d'une législation universelle.

Cela est d'autant plus drôle que c'est justement ce qu'oppose Liorel à l'auteur du journal dans le commentaire initial du thread sur lequel nous discutions :

Donc si je comprends bien, tu souhaites pouvoir t'exprimer, mais le fait que d'autres critiquent (faisant ainsi usage de leur propre liberté d'expression) te chagrine ?

Liorel, et avec lui tous ceux qui partagent sa position, sont en réalité des kantiens qui s'ignorent sur le plan de la philosophie pratique. :-)

L'auteur du journal souhaite pouvoir s'exprimer librement et critiquer qui bon lui semble : telle est sa maxime. La raison pratique, moralement législatrice, lui ordonne alors (via l'impératif catégorique) que cette maxime doit être universalisable comme principe législatif. Or il semble vouloir refuser cette universalisation, ce que lui reproche Liorel. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne dirais pas « hors contexte » Monsieur Phi explique bien que c'est le point de vu d'un prussien du 18ème. Il ne rentre effectivement pas dans plus de détail, mais son point n'est justement pas de valider ou d'invalider Kant, mais d'expliquer que la morale n'est pas universelle, elle est liée à un contexte temporel et culturel.

Mais bien sûr, mais bien sûr… Sa vidéo reste globalement un tissu d'ineptie sur la morale kantienne, en prenant quelque extrait bien choisi, pour justifier ses thèses. La diffèrence avec les lecteurs du site, c'est que comme Colin Pitrat le dit dans son commentaire où il donne le lien de la vidéo :

Sur le sujet, tu peux aussi lire Kant puis regarder la dernière vidéo de Mr Phi. Ou juste regarder la vidéo …

Kant, moi, je l'ai lu en long en large et en travers et je conseillerai donc plutôt de le lire que de se fier au contenu de la vidéo qui m'est apparue (alors que contrairement à toi, et sans doute aussi aux autres, je sais très bien de quoi il en retourne) comme étant d'un grande médiocrité intellectuelle. ;-)

Lorsqu'il cite ce passage, il laisse sous entendre que l'infanticide est acceptable pour Kant et que la honte de leur mère est des plus légitime. Sauf que c'est un peu plus compliqué que cela, et que le passage est cité hors contexte, non un contexte historique, mai hors contexte dans le texte de Kant lui-même. Voici le passage complet :

Il y a cependant deux crimes qui méritent la mort et vis-à-vis desquels la question de savoir si la législation est aussi légitimée à leur infliger la peine de mort, demeure encore douteuse. Ce qui conduit à l'un comme à l'autre, c'est le sentiment de l'honneur. Dans un cas, il s'agit du sentiment de l'honneur du sexe, dans l'autre, celui de l'honneur guerrier, et assurément y va-t-il vraiment de l'honneur dans le sentiment qui s'impose à ces deux groupes de personne comme un devoir. Le premier de ces crimes est l'infanticide maternel (infanticidum maternale), l'autre est le meurtre d'un compagnon d'armes (commilitonicidium), le duel. Dans la mesure où la législation ne peut faire disparaître la honte d'une naissance en dehors du mariage, et tout aussi peut effacer la tache qui vient à tomber par soupçon de lâcheté sur un officier subalterne qui n'oppose pas à un affront reçu un force personnelle surpassant en lui la crainte de la mort, il semble que, dans un cas comme dans l'autre, les être humains se retrouvent en l'état de nature et que l*'homicide* (homicidium), sans qu'il doive nécessairement être désigné comme un meurtre (homicidium dolosum), soit certes dans les deux cas bel et bien punissable, mais ne puisse être puni de mort par le pouvoir suprême. L'enfant qui est venu au monde en dehors du mariage est né hors la loi (laquelle ici se nomme en effet mariage), par conséquent aussi en dehors de sa protection. Il s'est en quelque sorte introduit dans la république (comme une marchandise interdite) d'une manière telle que celle-ci (dans la mesure où, en toute justice, il n'aurait pas dû venir en toute justice sur ce mode) peut ignorer son existence, donc aussi son anéantissement, et que nul ne décret ne puisse supprimer la honte de la mère dès lors que son accouchement en dehors du mariage est connu. […]

Qu'est-ce donc qui, dans ces deux cas (qui relèvent de la justice criminelle), est de droit ? La justice pénale est ici placée devant de sérieuses difficultés : ou bien annuler par la loi le concept d'honneur (qui n'a ici rien de délirant) et ainsi infliger une peine de mort, ou bien dissocier du crime la peine de mort qui s'y applique, et donc être soit cruel, soit excessivement indulgent. On peut dénouer ce nœud de la façon suivante : l'impératif catégorique de la justice pénale (savoir qu'allant à l'encontre de la loi, l'homicide d'autrui doit être puni de mort) reste valide, mais la législation elle-même (par conséquent aussi la constitution civile), tant qu'elle est encore barbare et non civilisée, est responsables du fait que les mobiles de l'honneur ne consentent pas dans le peuple (subjectivement) ) s'accorder avec les mesures qui (objectivement) sont conformes au but visé, de telle sorte que la justice publique procédant ici de l'État devient une injustice vis-à-vis de celle qui procède du peuple.

Kant, Doctrine du droit.

Première il ne s'agit pas ici tant d'une question de morale que d'une question de droit. Secondement, il considère des cas bien réels qui ont cours dans la société où il évolue. Troisièmement, pour nous, ces cas sont bel et bien ceux des signataires du manifeste de 348 salopes : la différence étant que ces femmes commettaient des infanticides au lieu d'avorter, du fait que la roulette russe était à ranger à côté de la crappette comme loisir ludique vu le risque presque certain de mourir en cas d'avortement à cette époque.

En conséquence quel intérêt pour soutenir sa thèse sur la variabilité des principes moraux de sortir cet extrait tronqué ? En tout honnêteté, t'était-il venu à l'esprit, à la lecture du seul passage qu'il citait, que le problème abordé était bien celui que je décris ?

Il faut dire que de revoir sortir cet extrait m'a un peu énervé, j'avais déjà vu Michel Onfray faire le coup chez Ruquier dans On n'est pas couché. Mais bon, comme dit Gaspard Proust dans son spectacle Gaspard Proust tapine :

Parfois je me fais traverser par des idées que je ne comprends pas. Et je me dis, waouh, je suis Emmanuel Kant. Parfois ce sont des idées que je maîtrise totalement. Et là, je me dis, mince, je ne suis que Michel Onfray. Michel Onfray, vous voyez ? L'homme qui aurait aimé être Nietzsche mais hélas, un siècle trop tard.

Ensuite, soutenir dans sa vidéo (je parle de Mr Phi) que l'objectif de Kant était « ma mère avait bien raison et je vais vous le prouver en 2000 pages » est un tel foutage de gueule philosophique que j'en suis resté coi! :-O

Son objectif était plutôt celui-ci : prouver que oui, l'homme est libre et qu'il n'y a là aucune contradiction avec le principe de déterminisme des lois de la nature. Autrement dit qu'il n'y a aucune contradiction théorique entre nature et liberté. Ce qui, par exemple, n'était pas l'avis d'Einstein :

Je me refuse à croire en la liberté et en ce concept philosophique. Je ne suis pas libre, mais tantôt contraint par des pressions étrangères à moi ou tantôt par des convictions intimes. Jeune j'ai été frappé par la maxime de Schopenhauer : « L'homme peut certes faire ce qu'il veut mais il ne peut pas vouloir ce qu'il veut »;

La solution kantienne à ce problème est l'impératif catégorique, et Shcopenhauer qui était un grand lecteur de Kant ayant rejetait cette solution fut très conséquent en rejetant aussi le concept de liberté. Parce qu'il faut savoir aussi, que Kant est bien le premier philosophe a avoir tant insisté sur la contradiction apparente, sur le plan théorique, entre nature et liberté.

Mais d'un manière générale, Mr Phi semble être un utilitariste et j'ai toujours trouvé que les utilitaristes étaient de piètre théoricien. Le principe utilitariste est un corollaire trivial de l'impératif catégorique kantien, et c'est écrit déjà noir sur blanc dans la Critique de la raison pratique : soit ils ne comprennent rien aux principes kantiens, soit ils ne comprennent pas le concept de corollaire; dans chacun des cas ce n'est pas à leur honneur.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Et prends garde à tes propres déviances, si tu ne veux pas finir comme Kant dans 10 ans

Je suppose que tu fais référence à la vidéo postée dans un autre journal, et que tu as en tête le passage sur l'infanticide où il compare l'enfant né hors mariage à une marchandise de contrebande. Le problème est que cet extrait a été cité totalement hors contexte et qu'il ne rend pas justice au problème qu'il y traite.

Ce passage se trouve dans sa Doctrine du droit au chapitre sur la justice pénale. Il était partisan de la peine de mort et considérait qu'un homicide volontaire devait être puni de mort. Donc, après avoir écarté les objections du marquis de Beccaria au sujet de la peine de mort, il se pose la question de savoir si certains homicides, bien qu'étant des crimes, ne peuvent pas être dispensés d'une telle peine : tel est le cas de certains infanticides, de son point de vue.

Mais ce qu'il faut bien comprendre, c'est qu'il vivait en prusse à la fin du 18ème siècle, et que le profil des femmes ayant recours à un tel acte est globalement celui des signataires du manifeste des 343 salopes. La différence est, qu'à cette époque, le recours à l'avortement étant bien trop dangereux pour la femme enceinte, elle menait la grossesse à terme puis tuait le nouveau né. Ce qu'il dit, dans ce passage, est que bien qu'un tel crime soit punissable il ne relève pas de la peine de mort. Je ne vois pas trop où se situe sa « déviance ».

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je sais bien que Go fait du typage statique (même s'il fait fait du typage dynamique pour la généricité avec l'interface {}). Ce que je voulais dire c'est que le problème que tu cherchais à illustrer ne relève pas de la distinction typage dynamique vs. typage statique, mais d'une limitation du paradigme objet et de la façon dont il gère le polymorphisme ad-hoc. Go n'est pas orienté objet, tout comme Haskell ou Rust ne le sont pas. En Haskell ton code passera par des type classes :

class User a where
   greetings :: a -> String

data Plouf = Plouf { FirstName :: String, LastName :: String, Addr :: String }

instance User Plouf where
  grettings user = ...

En Rust, ce sera par des traits, ce qui n'est pas de l'orienté objet.

Pour illustrer la distinction entre l'approche objet et celle de Go, Haskell et Rust, faisons cela en OCaml.

Selon le paradigme objet, on aurait une méthode greetings sur notre objet

class fst_name last_name addr = object
  val fst_name = fst_name
  val last_name = last_name
  val addr = addr
  method greetings () = Printf.sprintf "Dear %s %s" fst_name last_name
end

et la fonction foo appellerait cette méthode sur notre objet

let foo o = print_endline (o#greetings ())

let u = new plouf "Matt" "Aimonetti" "chez moi" in foo u;;
(* le retour *)
Dear Matt Aimonetti

Dans l'approche objet, les opérations sur le triplet de string ne sont pas dissociables du types : c'est un tout. Ce que tu exprimais dans ton commentaire ainsi :

Le type Plouf n'a aucun rapport avec l'interface User. Ça permet d'écrire après coup des fonctions qui définissent des interfaces décrivant le contrat que doivent remplir leur arguments sans impact sur les types créé ailleurs.

Dans l'approche objet, le dictionnaire de méthodes (ici User) et le type sur lequel elles opèrent (ici Plouf) sont indissociables. Dans l'approche de Go, Haskell ou Rust le dictionnaire de méthode et le type sont dissociés. C'est ce que j'ai cherché à expliquer dans ma réponse précédente, et c'est aussi la raison pour laquelle en OCaml on passera par des modules et non des objets pour modéliser une telle problématique.

(* la version OCaml de la type classe Haskell *)
module type User = sig
  type t
  val greetings : t -> string
end

module Plouf = struct
  type t = {
    first_name : string;
    last_name : string;
    addr : string
  }

  let greetings {first_name; last_name; _} =
    Printf.sprintf "Dear %s %s" first_name last_name
end

let foo (type a) (module M : User with type t = a) x = M.greetings x

La différence ici, avec les trois autres langages, est que l'on peut définir plus d'un dictionnaire pour un même type : il doit donc être passer explicitement à la fonction foo. Là où, dans les autres langages, le dictionnaire étant unique pour un type donné, il est déterminé univoquement à partir du type de la variable x.

Pour bien illustrer la différence avec le paradigme objet, c'est cela le type d'un objet :

type 'a user_object = 'a * (module Meth : User with type t = 'a)

c'est la donnée conjointe d'une valeur de type 'a (les attributs de l'instance) et des méthodes sur ces attributs, conjonction que l'on ne peut séparer en ses composantes au niveau du système de type.

Ceci étant, bien que je trouve ce paradigme plus intelligent que celui du paradigme objet, la façon dont il existe en Go reste très limitée : tu ne peux pas surcharger des opérateurs binaires avec (addition, comparaison, test d'égalité…).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

J'ai répondu un peu vite hier, mais plus qu'un type paramétré, ton histoire ressemble à une classe paramétrée par d'autres classes. Dans le jargon des langages ML, on appelle cela des foncteurs : des modules paramétrés par d'autres modules, c'est-à-dire des fonctions des modules dans les modules. Les types paramétriques sont des foncteurs, mais tous les foncteurs de sont pas des types paramétriques (comme les canards sont des animaux, mais les animaux ne sont pas tous des canards).

Pour comprendre un peu ce qu'est un module, prenons cette classe python :

class a:
     def __init__(self, i):
         self.attr = i
     def get_attr(self):
         return self.attr

Dans les langages de la famille ML, on n'utilisera pas de classe pour exprimer cela mais un module :

module A : sig 
  type 'a t
  val init : 'a -> 'a t
  val get_attr : 'a t -> 'a
end = struct
  type 'a t = 'a
  let init i = i
  let get_attr x = x
end

Le problème général du paradigme objet est qu'il confond (de manière totalement ridicule) un concept avec une théorie sur un concept donné. Ici le concept (qui est générique) c'est le type paramétrique A.t et les autres fonctions du modules forment une théorie sur ce concept. Du point du vue du paradigme objet, on se met à dire que c'est la théorie sur A.t, soit le module A, qui définit le concept : c'est inepte. On peut tout à fait étendre la théorie (rajouter des fonctions) sans changer le moins du monde le concept dont elle parle.

Là où cela devient gênant en général, c'est quand on pratique l'héritage. On a coutume de dire, dans le monde de l'orienté objet, que comme un canard est un animal alors la classe canard hérite de la classe animale : c'est faux et absolument faux. La proposition les canards sont des animaux signifie que les canards sont un sous-type (et non une sous-classe) du type animal. Il est rare que des les deux notions de sous-classe et de sous-type se recouvre, en particulier ça ne marche plus dès qu'il y a des opérateurs binaires.

Quittons cette digression sur le monde objet, et revenons à nos modules. Je disais plus haut que les types paramétriques sont des foncteurs, voyons cela avec le type générique des listes.

(* on plonge les types dans le monde des modules *)
module type T = sig type t end

(* le type des listes est un foncteur *)
module ListF (A : T) = struct type t = A.t list end;;
module ListF : functor (A : T) -> sig type t = A.t list end

(* illustration sur les listes d'entiers *)
module Int_list = ListF (struct type t = int end);;
module Int_list : sig type t = int list end

(* pas de problèmes de typage *)
([1; 2; 3] : int_list);;
- : int_list = [1; 2; 3]

([1; 2; 3] : Int_list.t);;
- : Int_list.t = [1; 2; 3]

Maintenant si on veut que notre module paramétré (notre foncteur) n'opère par sur n'importe quel type mais sur des types munis de certaines opérations, on le précise par une contrainte de types sur la signature du paramètres.

(* les contraintes de type sur le paramètre *)
module type S = sig
  type t
  val of_string : string -> t
  val meth : t -> int
end

(* notre module paramétré *)
module A (M : S) = struct
  type owner = M.t
  let f () = M.(meth (of_string "foo"))
end

Voilà : A ne connaît absolument rien des modules qui lui seront passés en paramètre si ce n'est qu'ils doivent satisfaire les contraintes de la signature S.

On peut définir ensuite plus loin, dans d'autres entités, des modules à lui passer.

module M : S = struct
  type t = string
  let of_string x = x
  let meth = String.length
end

module N : S = struct
  type t = int
  let of_string s = try int_of_string s with _ -> 0
  let meth i = i
end

module B = A (M)
module C = A (N);;
(* note la valeur des types [owner] dans chacune des applications *)
module B : sig type owner = M.t val f : unit -> int end
module C : sig type owner = N.t val f : unit -> int end

(* application de [f] pour les modules résultants *)
B.f ();;
- : int = 3

C.f ();;
- : int = 0

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je ne suis pas bien sûr de comprendre tout ton code, mais ça m'a tout l'air d'être juste une question de généricité. Si je comprends bien, l'attribut owner_typ_id de ton instance est la classe de owner_1. Ta classe A est juste une classe paramétrée et effectivement elle n'a pas besoin de connaître toutes les classes B, C, D… Tu peux voir cela comme un type somme infini, si tu veux. Par exemple, le type paramétré List <T> peut être pensé comme List <Int> ou List <Float> ou List <String> ....

Peut être qu'ici, comme le paramètre de type ne peux pas être quelconque (il doit disposer de certaines méthodes, comme get_by_id), il faudrait utiliser des GADT pour restreindre les valeurs possibles du paramètres de type; mais rien qui ne me semble inaccessible au typage statique.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ca c'est du structural typing, non ? J'avoue que la syntaxe est tellement absconse que je pige pas tout le bout de code.

Non c'est bien du duck typing, mais les auteurs de la page wikipédia ont écrit n'importe quoi.
Pour la syntaxe absconse, c'est juste une question d'habitude sur le let binding. Pour définir une varibale, comme un entier, on écrit let i = 1 c'est-à-dire soit i l'entier 1 ou en anglais let i be the integer 1.

Pour reprendre les exemples de la page wikipédia :

class duck = object
  method fly () = print_endline "Duck flying"
end

class airplane = object
  method fly () = print_endline "Airplane flying"
end

class whale = object
  method swim () = print_endline "Whale swimming"
end

Pour savoir si un objet peut voler, c'est bien du duck typing :

let fly o = o#fly ();;
val fly : < fly : unit -> 'a; .. > -> 'a = <fun>

la notation o#fly () consiste à appeler la méthode fly de l'objet o, et l'inférence de type conclue que pour utiliser la fonction fly sur un objet o celui-ci doit posséder une méthode fly et possiblement d'autres méthodes (les ... dans le type de l'objet). Ainsi :

fly (new duck);;
Duck flying
- : unit = ()

fly (new airplane);;
Airplane flying
- : unit = ()

fly (new whale);;
Error: This expression has type whale but an expression was expected of type
         < fly : unit -> 'a; .. >
       The first object type has no method fly

L'erreur est détectée statiquement.

Pourquoi OCaml reste si confidentiel s'il est si génial ?

Je n'ai pas la réponse à la question. Peut être parce que c'est un langage académique et qu'il n'a pas la force de frappe en communication d'entreprises comme Google ou Oracle. Mais cela va peut être changer maintenant que facebook s'y est mis, bien qu'il le fasse via le langage Reason (qui n'est rien d'autre qu'une syntaxe concrète différente pour du OCaml afin qu'il ressemble plus au javascript : c'est laid, mais apparemment cela désarçonne moins leur cible de développeurs).

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Mais comment fais-tu ton type somme si tu ne sais pas quels sont les sous-types de ce type somme ?

Là il me faudrait un exemple pour mieux comprendre la situation. Tu peux illustrer avec un code minimal en python la situation que tu as en tête : pas besoins d'implémenter les méthodes, un pass suffit; je veux juste avoir une idée plus claire et précise de l'architecture globale du code.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

C'est certain, mais dans certaines fonctions de bibliothèques les spécifications sont bien connues et c'est ce que l'on teste avec les tests unitaires. Si je reprend, par exemple, mon interface Anneau d'un commentaire précédent, on doit avoir comme propriété que add x (neg x) = zero pour tout valeur de x. Ça s'exprime et se prouve en Coq, ce qui est hors de portée des tests unitaires.

Ceci étant, la référence aux systèmes avec typage dépendant avait pour seul but de justifier la proposition : plus on enrichit le système de types, moins on a besoin de tests unitaires. Proposition implicitement soutenue par rewind qui est à l'origine de cette sous discussion dans les commentaires.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je veux des conteneurs de n'importe quel type que je veux pouvoir manipuler en duck typing.
[…]
J'utilise un itérateur pour optimiser la mémoire,… quand je le décide et je réfléchis à une solution plus blindée… quand c'est nécéssaire (Lean).

Au risque de me répéter, le duck typing peut se faire tout à fait statiquement, ce n'est absolument pas une nécessité d'avoir recours au typage dynamique pour cela. Ton cas se gère très bien avec les type classes de Haskell.

Il en est de même avec l'exemple ORM de flan où il suffit d'utiliser un type somme.

J'attends toujours un exemple concret que l'on ne peut pas gérer en typage statique et donc avec perte de sécurité sur le code.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Ça tombe bien, personne n'a dit ça, et c'est une bêtise.

Je crois que c'est moi qui l'est dit, et ce n'est pas une bêtise : c'est ce qu'offre les langages avec types dépendants. Du moins il dispense de tests unitaires, sauf pour ce qui est des erreurs dans la formalisation des spécifications du code.

L'exemple le plus parlant est celui-ci :

Theorem transform_c_programm_preservation :
  forall p tp beh
  transf_c_program p = Ok tp ->
  program_behaves (Asm.semantics tp) beh ->
  exists beh', programm_behaves (C.semantics p) beh'
            /\ behavior_improves beh' beh

Laissant de côté le mot clef Theorem, le terme transform_c_programm_preservation est un terme du langage dont le type est l'énoncé exprimant que CompCert C est bien un compilateur C optimisant qui préserve la sémantique. Le terme, ou programme, est construit grâce à l'assistant de preuve Coq et il y a bien vérification statique qu'il a le bon type. Comme son type quantifie sur la totalité des programmes C (la varibale p du forall), qui est potentiellement infinie, il garantie des choses inaccessibles aux tests unitaires.

Par contre, il reste la question : la formalisation de la sémantique de l'Asm (utilisée dans le terme Asm.semantics tp) est-elle conforme à la réalité ? Question dont la réponse est inaccessible aux méthodes formelles. De même pour ce qui est de la question sur la correction de la formalisation du C.

Au niveau de la traduction en français, le type s'exprime ainsi : pour tout programme C p, tout programme assembleur tp et tout comportement observable beh, si la fonction transf_c_prgram appliquée à p renvoie le programme tp et que beh est un comportement observable de tp en accord avec la sémantique ASM, alors il existe un comportement observable beh' de p conforme à la sémantique du C et tel que beh améliore beh'.

Autrement dit le type affirme que transf_c_program est un compilateur optimisant du C vers l'ASM.

Ce cas extrême n'était pas pour inciter à l'usage des types dépendants, mais pour montrer que plus on introduit de typage statique et d'expressivité dans le système de types, moins on a besoin de tests unitaires (au point de ne plus en avoir besoin) : ce qui était bien ton propos initial. ;-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Je sais pas si c'est très clair…

Ça l'est : tu veux faire du polymorphisme ad-hoc; mais je ne vois pas où on a besoin de typage dynamique pour cela.

L'idée du polymorphisme ad-hoc est d'avoir des fonctions qui ont le même nom (ici Greeting) mais qui opère sur différents types et selon des logiques différentes (à la différence du polymorphisme paramétrique). Ensuite à l'usage (comme dans ta fonction foo) la fonction effectivement utilisée est choisie en fonction du type du paramètre (type base dispatch). C'est exactement ce que font les type classes de Haskell et les traits du Rust. Cette manière de faire est bien plus intelligente (j'ai envie de dire moins inepte) que l'approche de l'orienté objet. En OCaml on passe par des modules et foncteurs pour faire cela (avec une perte de l'implicite) et il me semble (mais là je suis moins sûr) que les template du C++ peuvent servir à cela.

Pour présenter grossièrement l'idée, il s'agit d'associer à un type un dictionnaire de fonctions pour opérer dessus, c'est l'interface contre laquelle on veut programmer de manière générique. En fonction du type du paramètre, le compilateur choisira le dictionnaire qui lui a été associé. Néanmoins, le système des interfaces du Go reste trop limité à mon goût : j'en ai déjà parlé sur un ancien journal de gasche.

Prenons l'exemple de la structure d'anneaux en mathématiques : un anneau c'est un type de données que l'on peut ajouter, soustraire et multiplier avec deux éléments neutres pour l'addition et la multiplication. Autrement dit, c'est cette interface de module :

module type Anneau = sig
  (* le type des éléments de l'anneau *)
  type t

  (* les éléments neutres *)
  val zero : t
  val one : t

  (* les opérations *)
  val add : t -> t -> t
  val neg : t -> t
  val mul : t -> t -> t
end

Plutôt que de dire que l'on peut les soustraire, je préfère exprimer l'axiomatique en disant que l'addition est une opération inversible d'où la fonction neg. À partir de là, dès que l'on a une telle structure, on peut définir dessus le polynôme :

let f (type a) (module A : Anneau with type t = a) x =
  let (+), ( * ) = A.add, A.mul in
  x * x + x + A.one

Le principe derrière les type classes de Haskell ou les traits de Rust est de dire que pour un type donnée on ne peut définir qu'une interface Anneau sur ce type. Autrement dit, ils considèrent que le type Anneau with type type t = a est un singleton pour tout type a (où plutôt le compilateur garantie que l'on ne définit pas deux valeurs distinctes de ce type), ce qui est trivialement faux mais en pratique largement suffisant. Les interfaces de Go, c'est un peu la même idée mais en beaucoup moins bien : tu ne peux pas définir l'interface Anneau par exemple, il n'est pas possible de définir des opérateurs binaires sur le type t dans les interfaces de Go.

En OCaml, comme le type en question est rarement un singleton, il faut explicitement passer le dictionnaire en argument à la fonction f, même s'il y a déjà eu des propositions pour le rendre implicites dans certaines situations.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Oui mais tu réponds à une comparaison entre C++ et python. Donner un exemple pourquoi pas venir dire que le langage foobar lui il est mieux, c'est hors sujet.

Ce n'est pas vraiment hors-sujet à mon avis. Philippe Fremy répond à rewind en postant une vidéo d'une de ses conférences sur le typage statique en python. Le slide de conclusion est :

Conclusion :

• Type annotation is powerful to bug finder. Use it !
• Type annotation is also good way to document your code.
• Feedback from developpers using type annoation: "It rocks !"
• Some python dynamic constructs are difficult to verify statically

Là où c'est déjà étrange, c'est que dans sa réponse il laisse entendre que rewind cherche à troller, alors que c'est justement ces avantages du typage statique que rewind et chimrod ont cherchait à mettre en avant.

Ensuite, oui cela relève d'une plus grande sûreté que le recours aux tests unitaires. Quand on pousse jusqu'aux systèmes à types dépéndants, non seulement on ne fait plus de tests unitaires mais en plus on obtient une sûreté que ne pourront jamais atteindre ces derniers : un test peut montrer l'existence d'un bug (dans le respect à la spécification) mais jamais son absence.

Typer son code permet effectivement de le documenter (point 2 du slide de conclusion) car le langage de types est un langage formel d'écriture de spécification du code, et permet donc d'exprimer en partie ce que doit faire la fonction. D'où mon point précédent, avec des types dépendants on peut totalement spécifier formellement le code et donc vérifier qu'il est conforme à sa spécification.

Pour le typage structurel, on peut tout à fait faire cela statiquement et sans écrire d'annotation. Quelques exemples issues de la conférence de Philippe Fremy :

(* voir à la 20ème minute *)

(* cas d'un bug détecter statiquement *)
class a ?step_init = object
  val step = step_init
  method get_step = step_init + 1
end;;
Error: This expression has type 'a option
       but an expression was expected of type int

(* première solution on teste la valeur de l'attribut [step] *)
class a ?step_init () = object
  val step = step_init
  method get_step = match step with None -> 0 | Some step-> step + 1
end;;
class a :
  ?step_init:int ->
  unit -> object val step : int option method get_step : int end

(* deuxième solution, on initialise avec une valeur par défaut *)
class a ?(step_init = 0) () = object
  val step = step_init
  method get_step = step + 1 end;;
class a :
  ?step_init:int -> unit -> object val step : int method get_step : int end


(* pour le typage structurel, voire autour de la 30ème minute *)
let validate form data = form#validate data;;
val validate : < validate : 'a -> 'b; .. > -> 'a -> 'b = <fun>

Enfin, pour ce qui est des objets et du typage structurel, la façon dont ils sont globalement utilisés en pratique cela en fait surtout des modules du pauvre. En OCaml on utilisera plutôt des modules, en Haskell des type classes, en Rust des traits et en C++ des template.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

la cuisine cuisine

La cuisine est une pratique récursive qui s'appelle elle-même ? Elle termine ? Est-on garanti d'avoir de quoi manger à l'arrivée ? :-P

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

La liste Ocaml est une fifo pour une très bonne raison d'immutabilité. Mais comprendre pourquoi elle est comme ça et pourquoi c'est très bien ainsi, est bien au delà d'une introduction à l'informatique.

Les listes OCaml sont naturellement en mode LIFO : dernier arrivé, premier sorti. Ensuite c'est juste le principe des entiers unaires : en quoi c'est au-delà d'une introduction à l'informatique ? C'est ce que fait un enfant quand il apprend à compter avec ses doigts. Si des élèves de terminale ne comprennent pas cela, il y a un gros soucis.

Les listes OCaml sont LIFO par construction :

let push x l = x :: l

let l = [] |> push `As |> push `Roi |> push `Dame;;
val l : [> `As | `Dame | `Roi ] list = [`Dame; `Roi; `As]

(* la première à sortir est la dernière arrivée, à savoir `Dame *)
List.hd l;;
- : [> `As | `Dame | `Roi ] = `Dame

Ensuite, si l'on fait abstraction des valeurs contenus dans la liste, on obtient une liste de type unit list :

List.map ignore l;;
- : unit list = [(); (); ()]

et une telle liste c'est les entiers unaires : une liste de bâtons, de traits, de points…

Qu'est-ce qu'on fait, le plus souvent, avec une liste ? On utilise un fold, c'est à dire le principe du raisonnement par récurrence sur les nombres entiers. Il vient en deux versions : fold_left (mode LIFO) et fold_right (mode FIFO).

Non, vraiment, je ne vois pas où est le problème d'aborder ces notions dans une introduction à l'informatique. Cela fait partie des concepts les plus simples à assimiler.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

Surtout, ce que tu as décrit (et que j'ai complété, c'est plutôt moi qui l'ai tendu le piège) intervient très rarement dans un process GCL digne de ce nom (à base de PR par exemple)

Si tu parlais en français, ou dans une langue que tout un chacun peut comprendre, cela faciliterait grandement les choses. Je veux parler de ces termes comme « process GCL digne de ce nom » qui chez toi on peut être un sens, mais chez moi c'est : qu'est-ce qu'il dit ? Pour le reste des tes commentaires, cela reste dans la même zone : le fait que le système puisse planter dans des cas tordus, qui ne sont même pas rejeter par Linus (toi tu les rejettes pour cacher la poussière sous le tapis), ne te déranges pas : grand bien t'en fasse, mais je comprends mieux pourquoi il y a tant de bugs dans les logiciels existants; la rigueur intellectuelle ne semble pas être une priorité pour certains.

Honnêtement, si tu penses réellement m'avoir tendu un piège, de quelque forme qu'il soit, il faudra que tu me montres où il se trouve. La seule chose que tu as fait c'est nier un problème que même Linus ne nie pas et auquel il propose une solution pour contourner les limites de git.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.