kantien a écrit 1227 commentaires

C'est l'anti-thèse de Ocaml, très beau sur le plan théorique mais en pratique, c'est trop compliqué pour le développeur lambda, pas assez performant, trop peu utilisé etc.

Il n'a jamais fait de phrase à trou dans son enfance en cours de français le développeur lambda ? Parce qu'écrire un programme en OCaml c'est le même principe. Elle est où la difficulté ?

Exemples:

• Je mange du pain
• Je bois de l'eau

de ces deux phrases, on peut abstraire un motif sous la forme :

• Je verbe de qqchose

ce motif, on peut l'appliquer soit au couple manger - pain, soit au couple boire - eau, afin d'obtenir les phrases précédentes.

Après, certes, on peut commencer à construire des phrases plus complexes, en partant par exemple de ce patron :

• je regarde qqchose

ce qui peut donner :

• je regarde la télé
• je regarde le chien du voisin

Dans le deuxième exemple, le complément d'objet est lui-même un composé dont on peut abstraire un motif. Disons, celui-ci :

• l'animal de qqu'un

qui peut être instancier sous la forme :

• le chien du voisin
• le chat de ma tante
• le poisson rouge de Nicolas

et ainsi de suite. Ensuite, en composant les patrons de phrases, on construit des phrases de plus en plus complexes (ce qui ne veut pas dire compliquée ;-).

Tu t'y prends autrement pour exprimer ta pensée de manière écrite? Le développeur lamabda, aussi, a une autre façon de procéder? Si c'est le cas, j'aimerais bien savoir laquelle.

En programmation fonctionnelle, abstraire un mot pour former un patron c'est ce qui se nomme la lambda abstraction (le mot clef fun de OCaml), puis appliquer un patron à des cas particuliers cela s'appelle l'application de fonction, et la phase qui remplace le paramètre formelle par le paramètre effectif se nomme la beta reduction (c'est-à-dire l'exécution du code).

(* j'ai les motifs suivants *)
1 + 2
2 + 3

(* j'abstrais le patrons suivants *)
fun x y -> x + y

(* je l'utilise pour retrouver les exemples du dessus *)
(fun x y -> x + y) 1 2

(* et là le runtime fait des substitutions successives ou beta reduction *)
(* on commence par susbstituer le premier paramètre x *)
(fun y -> 1 + y) 2

(*on fait pareil avec y *)
1 + 2

(* on calcule *)
3

Après le langage va rajouter des catégories grammaticales ou types pour bien vérifier que l'on utilise les patrons avec des mots ou construction conforme au règle de la grammaire, comme tout langage à typage statique. Autrement dit, dans le patron "je verbe de qqchose", il n'est pas correcte de vouloir utiliser le mot "bouchon" à la place du verbe car il n'appartient pas à la bonne catégorie grammaticale.

Qui y a-t-il de compliquer à comprendre dans tout cela ?

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

La pour le coup, le calcul me semble pas si simple. Ce cargo a un énorme avantage: il ne consomme (quasiment) pas de carburant.

Sur ce point, je dirais quand même que l'expérience reste en faveur du pétrole. Le turbovoile d'Anton Flettner fut construit au début des années 1920 et, de fait, cette technologie n'a pas du tout prise. Je crains qu'il ne faille pas compter sur cet apparent avantage économique pour espérer la voir fleurir.

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

Il serait pas awesome ce produit ? Genre revolutionary ?

Je crois qu'il y a méprise : ce n'est pas revolutionary mais It’s gonna be legen… wait for it… dary ! Legendary! L'awesomeness c'est totalement Stinson-proof. Par contre cela risque de ne pas être très inclusive, ce qui est à la mode en ce moment. :-)

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

Après, je ne comprends pas ce mépris sous-jacent pour les techniciens.

Je ne crois pas qu'il y ait un quelconque mépris envers les techniciens. Il me semble que l'idée générale serait plutôt que la difficulté technique d'exécution d'une œuvre ne détermine nullement sa qualité musicale. Cela se rapproche de ce qu'exprimer Duke Ellington avec son It don't mean a thing (if it ain't got that swing).

Pour rester dans l'instrument de Van Halen, Bibi (aka Biréli Lagrène), un des virtuoses de la guitare, aurait pu mal tourner à la fin des années 80, début 90, s'il avait suivit ce courant. Heureusement, par la suite, il est revenu à la raison (petit clin d'œil à Beethoven sur la fin ;-). Ceci étant il lui arrive encore de composer des pièces qui me laisse de marbre, comme son mouvements : la partie du sax soprano se prête très bien à la tessiture et au timbre de cet instrument, en revanche je trouve qu'il gâche la pièce avec sa guitare.

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

Le type 'null' est toujours là. Les types de base ne sont pas des objets.

Tout ça, OK (et à mon sens le null est peut-être le plus gros problème de Java). Il y avait un projet pour se débarasser des types de base, mais ça fait longtemps que je n’en ai plus entendu parler.

C'est étrange comme projet, j'aurais plutôt eu l'idée contraire : virer les objets et n'avoir que des types comme ceux de base. :-)

Les définitions mathématiques ne peuvent jamais être fausses. En effet, comme le concept est d’abord donné par la définition, il ne contient exactement que ce que la définition veut que l’on pense par ce concept. Mais, s’il ne peut rien s’y trouver de faux quant au contenu, il peut y avoir parfois, mais rarement, quelque défaut dans la forme (dans l’expression), je veux dire du côté de la précision. Ainsi cette définition ordinaire de la ligne circulaire, qu’elle est une ligne courbe dont tous les points sont également éloignés d’un point unique (du centre), a le défaut d’introduire sans nécessité la détermination courbe. En effet il doit y avoir un théorème particulier qui est dérivé de la définition, et qui peut être aisément démontré, à savoir que toute ligne dont tous les points sont également éloignés d’un point unique est courbe (qu’aucune partie n’en est droite).

Kant, Critique de la raison pure.

Un type c'est un concept et l'interface d'une classe la définition d'un concept (celui mal fait d'algèbre sur un concept). Celui qui définit ses concepts comme des classes s'y prend aussi mal que ce qui est reproché dans le texte ci-dessus. Si au lieu de ce théorème, on prend le fait qu'un cercle a une circonférence dont la valeur est le diamètre multiplié par une constante (Pi) et que l'on met cela dans une méthode d'une classe, alors on définit le cercle comme une quiche sur patte. ;-)

Le problème étant que, si l'on a que des classes, ce défaut qui touche à la forme des définitions, au lieu d'être rare, se retrouve être permanent.

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

La commutativité et l'associativité sont des points super importants en calcul sur des gros volumes. Que ce soit en C++ ou en n'importe quoi.

• Associativité: tu peux séparer en morceaux indépendants
• Commutativité: l'ordre n'est pas important, ainsi tu peux traiter les morceaux quand ils arrivent et ne pas dépendre de la latence réseau par exemple.

Ce n'est pas moi qui dirait le contraire : ces propriétés permettent d'effectuer les calculs dans n'importe quel ordre, i.e. quelque soit la permutation effectuée sur la séquence d'opérations on aboutit toujours au même résultat. Ainsi, on est moins tributaire du temps d'accès aux données (peu importe l'ordre dans lesquelles elles arrivent) que ce soit du à de la latence réseau, ou à des échanges répétés entre le cache et la ram. ;-)

;)

Il y a une série d'articles de blogs (compilé en un livre) sur le thème théorie des catégories pour les programmeurs. L'auteur y donne des illustrations de code en Haskell et C++ : c'est dingue à quel point la syntaxe du C++ est tordue et peu « parlante ». Si l'on prend la notion élémentaire de monoïde (cf chapitre 3), en Haskell cela se définit ainsi :

class Monoid m where
    mempty  :: m
    mappend :: m -> m -> m

autrement dit un monoïde sur un type m est la donnée d'un élément neutre et d'une opération associative (important l'associativité, même si le contrat est implicite entre les programmeurs ;-). Là où en C++, avec les concepts, on se retrouve à le définir ainsi :

template<class T>
  T mempty = delete;

template<class T>
  T mappend(T, T) = delete;

template<class M>
  concept bool Monoid = requires (M m) {
    { mempty<M> } -> M;
    { mappend(m, m); } -> M;
  };

Non, mais what the fuck !? :-o

Par comparaison, en ML, c'est proche du Haskell mais plus conforme à la définition formelle des mathématiciens :

module type Mondoid = struct
  type t
  val mappend : t -> t -> t
  val mempty : t
end

c'est-à-dire la donnée conjointe d'un type (ou concept, ou ensemble…), d'une loi de composition interne associative et d'un élément neutre pour cette loi. La différence avec Haskell étant que le type fait partie du dictionnaire, là où en Haskell le type support du monoïde paramétrise le dictionnaire qui n'a que deux éléménts. C'est similaire à ce type produit :

type 'm monoid = {
  mempty : 'm ;
  mappend : 'm -> 'm -> 'm
}

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

Ai-je bien compris ?

Oui c'est cela, mais plus proche des packages génériques : c'est tout une section de code qui peut être paramétrée, pas seulement une fonction. Mais les concepts n'ajoutent rien de nouveau là-dessus, c'est ce qu'on toujours fait les template. Les concepts c'est juste un système de types pour les template. Le langage des template est interprété par le compilateur et, avant, lorsqu'il y avait une problème lors de l'instantiation d'une template, il y a avait l'équivalent d'une stack trace en guise de message d'erreur, qui pouvait faire 3km de long si le code utilisé était très générique. Là, ils auront des messages plus clairs du au système de type.

Peut-on faire des trucs encore plus forts avec les concepts que juste spécifier les opérations nécessaires ?

Je ne crois pas, mais on peut les utiliser en dehors des templates. Par exemple, pour contraindre le mécanisme d'inférence de type :

Sortable auto x2 = f(y);

ne compilera que si la fonction f retourne une valeur que l'on peut trier.

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

Mais je pense amicalement que tu me provoques un peu sachant que tu sais cela très bien.

Ce n'était pas de la provocation, j'étais bien sérieux avec ma question. Je me doutais bien que cela devait être affirmé sans preuve, mais j'ai préféré avoir confirmation. Là où j'étais un peu railleur, c'est en te demandant la syntaxe choisie pour exprimer cela (de manière générale je me demandes quels genres de psychotropes prennent les responsables du standard C++, mais ils devraient réduire la dose, j'ai rarement vu une syntaxe aussi laide).

C'est juste un problème d'interface ou de contrat que tu passes avec ton développeur et la libraire. Si on reprend l'exemple de la commutativité, si en tant que développeur je sais que le type générique (e.g. template) que j'utilise est commutatif pour mon opération, alors je peux me permettre certaines choses. On peut me mentir, mais au moins j'aurais prévenu. Inversement, en demandant que le type en entrée soit commutatif, je préviens l'utilisateur et il ne peut pas rater la contrainte que je lui demande.

Ça se tient. C++ étant orienté performance, avoir la commutativité permet de choisir un parcours de données plus efficace pour optimiser l'usage du cache du CPU, par exemple.

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

Avec un concept tu pourra aussi demander à ce que + soit commutatif.

C'est fascinant ça. Mais comment on prouve au type checker que l'opérateur + que l'on définit est bien commutatif ? On se contente de l'affirmer sans preuve ? Dans les faits, elle ressemble à quoi la syntaxe pour ce genre de propriété ?

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

Qu'ai-je loupé?

T'as le message d'erreur d'un type checker au lieu d'avoir une stack trace à la python. En gros, le système de template c'était du lamba-calcul non typé, ils y ont rajouté un système de types. Le langage est interprété par le compilateur : en l'absence de typage statique, tu as une stack trace lors de l'appel, avec un système de types tu as tous les avantages du typage statique.

Par contre le choix du nom pour la fonctionnalité n'est pas très judicieux : un concept c'est un type (les deux mots sont synonymes), donc des concepts il y en avait déjà depuis le début en C++. Là, cela revient à paramétrer du code par un type muni de certaines opérations : ça s'appelle une algèbre. ;-)

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

Moi perso j'ai 6 pieds de tomate, et cette année j'ai quasi rien récupéré. Et je sais pas quoi faire pour l'an prochain

Demande à eingousef ! :D

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

Personnellement, l'apprentissage de la théorie de la relativité m'a surtout fait comprendre a quel point j'étais ignorant, et je ne suis d'ailleurs toujours pas très sur de savoir ce que ce que c'est que la gravité.

Il me semble que tu es un ancien marin, alors pour approfondir cette question, sans avoir besoin d'un lourd formalisme géométrique, je peux te proposer de retourner à la source et de lire le Dialogue sur les deux grands systèmes du monde de Galilée. Si tu as lu le livre d'Einstein sur la rélativité, son personnage enfermé dans sa cabine est un lointain cousin d'un personnage de Galilée : un marin enfermé dans sa cabine et qui se demande si avec les expériences qu'il y fait, il peut déterminer si le bateau est en mouvement ou non. ;-)

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

Au début (avant la norme AFNOR), je suivais ton patron (merci, au passage pour ton journal de l'époque) ou celui du CHU de grenoble. ;-)

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

J'en sais rien, mais pas besoin de le faire si tu ne veux pas. C'est un carré de 20cm sur 20cm que tu dois replier d'une certaine façon : tu as un tuto ici, avec les dimensions en bas de page.

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

Pour ma part, j'utilise un masque maison en coton à chaque sortie depuis le début du confinement.

Au niveau de l'entretien, je ne le passe pas à la machine, mais je le fait tremper dans l'eau chauffée à la bouilloire électrique (entre 80°C et 90°C) avec de la javel [1] pendant 30 minutes, puis je finis par un coup de fer à repasser. Avec une telle température de lavage, il finit par rétrécir et j'en refais un autre : c'est assez rapide à faire si on a du stock de tissu ou de vieux draps, et pour le patron je suis maintenant celui fournit par l'AFNOR.

[1]: je mets aussi de la lessive, puis un rinçage rapide avec un adoucissant pour que le tissu ne deviennent pas trop rêche.

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

je serais d'ailleurs curieux de ce que Kant aurait à dire sur le sujet

Littéralement parlant, il n'a plus grand chose à dire sur le sujet, étant mort depuis plus de 200 ans. Mais, plus sérieusement, tu es curieux de savoir ce qu'il a dit sur quel sujet ? La tyrannie de groupe ? La première chose qui me vient à l'esprit est qu'il considérait la démocratie comme une forme de gouvernement despotique, mais ce qu'il entendait sous ce terme correspond plus à ce que nous entendons par démocratie directe et non les systèmes représentatifs (dont il était partisan) :

Pour que l’on ne confonde pas (comme on le fait communément) la constitution républicaine avec la démocratique, je dois faire les remarques suivantes. Les formes d’un État (civitas) peuvent être divisées, soit d’après la différence des personnes qui jouissent du souverain pouvoir, soit d’après la manière dont le peuple est gouverné par son souverain, quel qu’il soit. La première est proprement la forme de la souveraineté (forma imperii), et il ne peut y en avoir que trois : en effet, ou bien un seul, ou bien quelques-uns unis entre eux, ou bien tous ceux ensemble qui constituent la société civile possèdent le souverain pouvoir (autocratie, aristocratie et démocratie, pouvoir du prince, pouvoir de la noblesse et pouvoir du peuple). La seconde est la forme du gouvernement (forma regiminis) ; elle concerne le mode, fondé sur la constitution (sur l’acte de la volonté générale, qui fait d’une multitude un peuple), suivant lequel l’État fait usage de sa souveraine puissance, et elle est sous ce rapport ou républicaine ou despotique. Le républicanisme est le principe politique de la séparation du pouvoir exécutif (du gouvernement) et du pouvoir législatif ; le despotisme est le gouvernement où le chef de l’État exécute arbitrairement les lois qu’il s’est données à lui-même, et où par conséquent il substitue sa volonté particulière à la volonté publique. — Parmi les trois formes politiques, indiquées plus haut, celle de la démocratie, dans le sens propre de ce mot, est nécessairement un despotisme, puisqu’elle établit un pouvoir exécutif, où tous décident sur et même contre un seul (qui ne donne pas son assentiment), et où par conséquent la volonté de tous n'est pas celle de tous, ce qui est une contradiction de la volonté générale avec elle-même et avec la liberté.

Kant, Traité de paix perpétuel

Le texte complet est sur wikisource (mis en forme par zeroheure et moi-même ;-).

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

On leur montre le chemin.

Je ne suis pas certain que de faire l'éloge de la Corée du Sud soit le meilleur moyen d'arriver à tes fins ;-)

Le système de santé sud-coréen est en passe d’être totalement privatisé. La crise de 2008 a, pour l’instant, obligé le gouvernement coréen à revoir ses plans. Il n’existe pas à proprement parler d’offre publique de santé en Corée, tant l’offre de soins repose essentiellement sur le secteur privé qui représentait en 1996, 91% des lits et 89% du personnel hospitalier.

source

L'article date de 2010 et la situation n'a pas évolué vers plus d'étatisation, bien au contraire : la Corée du Sud a l'un des systèmes de santé le plus privatisé du monde, bien davantage qu'aux États-Unis.

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

Peut-être que chez des zététiciens chevronnés il y a quelque chose de précis ?

Se rendre chez les logiciens et philosophes devraient suffire. D'autant que, pour des questions aussi fondamentales, les dernières personnes que j'irai voir sont bien des statisticiens.

Je n'ai pas compris la partie après les deux points.

À considérer les choses objectivement nous n'avons que deux sources de savoir à la base de nos jugements : notre raison et l'expérience via l'observation du monde. Comme il est impossible de tout observer et expérimenter par soi-même, il est inéluctable, dans ce type de connaissance, de substituer l'expérience d'autrui à notre propre expérience au fondement de nos jugements. Procéder ainsi c'est se reposer sur l'autorité d'autrui, ce qui n'a rien de fallacieux.

Si quelqu'un que tu croises te dis qu'en ce moment il y a une pandémie, que tu lui demandes comment il le sait, puis qu'il te répond que c'est ce que dit l'OMS, alors il fait usage d'un argument d'autorité. Rejeter, par principe, tout argument d'autorité au prétexte qu'ils sont nécessairement fallacieux, c'est au pire la porte ouverte à toutes les formes de complotisme, au mieux l'avènement d'un scepticisme radical.

En revanche, dans le champ de la connaissance rationnelle, il n'est pas acceptable de substituer le jugement d'autrui au sien propre : je reconnais le théorème de Pythagore comme vrai, non parce que des géomètres le considèrent comme tel, mais parce je suis en mesure d'en fournir la preuve. La totalité du fondement de telles propositions se trouve en moi-même, dans ma propre raison, et il en est de même pour chacun.

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

"Argument d'autorité" est le terme utilisé pour ce qui n'est pas un argument, c'est une astuce de rhétorique, une ruse. C'est la définition du truc :-)

Il me semble que ta définition de l'argument d'autorité est trop stricte : on ne peut s'en passer dans les connaissances expérimentales.

Le préjugé qui tient à la considération des personnes. — Lorsque, dans les choses qui reposent sur l’expérience et le témoignage, nous faisons porter notre connaissance sur la considération que nous avons pour d’autres personnes, nous ne tombons pas dans un préjugé ; car, en fait de choses de cette nature, comme nous ne pouvons pas tout connaître par nous-mêmes, ni tout embrasser avec notre entendement propre, nous basons nos jugements sur la considération due aux personnes. — Mais, si nous fondons nos jugements, en fait de connaissances rationnelles, sur la considération que nous accordons aux autres, ces connaissances ne sont pour nous que de véritables préjugés, car les vérités rationnelles valent anonymement ; il n’est pas question de savoir qui est-ce qui a dit cette chose, mais qu’est-ce qu’on a dit. Qu’importe qu’une connaissance soit ou ne soit pas de noble origine ! Et cependant, le penchant à la considération des grands hommes en matière scientifique est très-commun, tant à cause des limites de la pénétration ordinaire, que par le désir d’imiter ce que nous croyons grand. Notre vanité se trouve encore indirectement satisfaite par le respect que nous portons à quelque homme de génie. De même que les sujets d’un despote puissant sont fiers d’être tous traités par lui de la même manière, puisque le plus petit peut, se croire égal au plus grand, tous deux n’étant également rien en présence du pouvoir illimité de leur maître, de même les adorateurs d’un grand homme se jugent égaux, en ce sens que la supériorité qu’ils peuvent avoir les uns sur les autres, considérée quant au mérite de cet homme, est réputée insignifiante.

Kant, Logique.

Lorsque Liorel nous présente le modèle statistique pour évaluer les risques, on est dans le champ de la connaissance pure et rationnelle : nulle personne ne peut faire autorité ; chacun étant aussi proche des sources du savoir que l'auteur (il se trouve dans la commune raison humaine, c'est-à-dire en nous même). En revanche lorsqu'il fournit les données d'entrée du modèle, elles sont le résultat d'observation et de mesures statistiques : c'est l'autorité des auteurs qui fait foi pour qui n'y a pas un accès direct.

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

Mathématiquement c'est peut être une horreur, mais en cuisine cela se pratique couramment … :)

Ça n'a rien d'une horreur mathématique, et ne dit on pas couramment « ajouter un ingrédient à la liste ». Comme te l'a dit JeanClaude : tu définis juste une algèbre sur les recettes de cuisine. Il est où le problème ? D'autant que ton exemple est mal choisi pour « détourner » l'arithmétique : c'est de l'arithmétique ton opérateur. Comme je l'ai dit plus haut : d'un certain point de vue les listes c'est des entiers unaires, et là tu as défini l'opération successeur (ou « ajouter 1 »).

module Arithmetique = struct
  type nat = unit list
  let zero = []
  let succ l = () :: l
end

Voilà : un entier unaire c'est juste une liste de bâtons, zéro c'est la liste vide et la fonction qui calcule le successeur consiste à ajouter un élément dans la liste (c'est à dire ta surcharge de la fonction add).

Toi ce que tu as écris c'est cela :

module Recette = struct
  type t = {
    ingredients : string list;
    nom : string ;
  }

  let new () = {ingredients = []; nom = ""}

  let changer_nom nom recette = {recette with nom = nom}
  let add ing recette = {
    recette with
    ingredients = ing :: ingredients
  }

let _ = Recette.(
 new ()
 |> changer_nom "Soupe de"
 |> add "patate"
 |> add "potiron"
)

Et ici ce que fais ma fonction add sur ma liste d'ingrédients, c'est la même chose que fait ma fonction succ sur les entiers unaires.

Pour répondre à ton autre commentaire :

Les mathématiques s'arrêteraient elles donc ou l'informatique commence :)

ou l'informatique aurait elle une plus grande portée que les mathématiques ?

:)

Non, comme je le dis depuis le début : c'est la même chose. C'est juste une extension et une généralisation des travaux de Descartes quand il a algébrisé la géométrie mais, entre Descartes et nous, il s'est passé près de 400 ans. ;-)

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

Je ne vois pas le rapport qu'il y a entre la question traitée et la polysémie des langages¹. De même qu'elle n'a rien à voir avec le fait que toute modélisation est une vision partielle et simplifiée de la réalité. Il s'agit de sémantique des langages et du fait que la relation « est une sorte de » n'a rien à voir avec la notion de classe et d'héritage, contrairement à ce qui est couramment présenté. Un canard, même simplifié, modélisé, tout ce que tu veux, n'a jamais été et ne sera jamais une instance d'une classe canard qui hériterait d'une classe animal. C'est ce que j'avais expliqué en détail dans ce commentaire d'une dépêche.

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

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.