Ours & Hippy — le blog [méditation]

Oui, c'est troublant et ça fait peur ! Et plus on le souligne (merci méchantloup), plus c'est choquant !
Penser que dans un domaine capital/potentiellement puissant/dangereux comme l'informatique, peut de gens s'instruisent ou, disons-le, reste des demeurés... C'est la porte ouverte à 1984, au négationnisme, au VIH qui ne cause pas le SIDA, à l'obscurantisme !

Décemment et pour le bien de l'Humanité, les gens des pays riches (j'entends "qui ont le temps de penser") doivent voir la différence entre un ordinateur et leur télévision ou leur minitel ! De la même façon qu'on doit être au courant de notre passé...

Je rejoins un peu BadWolf sur l'idee du strict minimum d'education.

Non pas que voir tout le monde devenir un power-user m'enchante (sinon apres comment je pourrais me la peter avec mes connaissances "de ouf" et mes bureaux en tuile ?), mais une partie considerable de l'energie de chacun pourrait etre sauvegardee si tout a chacun prennait au moins la peine de lire un manuel (concu pour les beotiens, tout de meme) sur le fonctionnement exterieur de leur machine, ou sur quel clic faire suivant tel probleme.

Il le font bien pour monter leur armoire ikea, pourquoi pas pour cliquer au bon endroit ? Faudrait-il vendre toutes les machines en kit ?

Et puis l'exemple du sport n'est pas completement pertinent: en soi, la culture sportive n'apporte strictement rien a l'homme, si ce n'est le plaisir de l'expression de sa passion. Ce n'est pour lui ni un besoin ni une necessite.

Par contre, l'informatique est un outil de travail pour beaucoup, et un outil ca s'entretien, on apprend comment l'utiliser pour etre vraiment plus efficace avec et que ca ne nous apporte pas plus de galeres que ca nous en enleve.

Donc, je ne comprends toujours pas pourquoi Madame michu ne fait pas le strict necessaire pour ne pas avoir a dependre de son petit-ils (qui habite a 500km de chez elle).

Si moi, n'etant vraiment pas fan de taule qui roule je suis capable de changer une roue, une batterie ou une bougie, pourquoi ne sait-elle pas cliquer sur le bouton qui clignote et qui lui pop a la gueule tous les quarts d'heure "mettre a jour votre systeme" ? Il n'y a vocabulairement rien de complique dans cette phrase.

Ça ne les intéresse pas, ils ne vont faire aucun effort pour apprendre quelque chose dans ce domaine, et ils sont dans leur droit le plus légitime.

Certes, pour ce qui concerne par exemple les concepts du libre, ou même à la limite "lancer Google".

Pour rejoindre un peu ce que dit Amaury : le problème c’est que le jour où la page d’accueil du non-informaticien se retrouve changée par accident, il ne sait plus se balader sur Internet. Bien sûr, il appelle son neveu/voisin/facteur qui « s’y connaît » à la rescousse, qui essaye de lui expliquer que non non, Google n’a pas disparu de la surface de la Terre, et qui résout le problème tout en essayant d’expliquer ce qu’est une page d’accueil. Mais le non-informaticien s’en tamponne, et une semaine plus tard, quand le problème resurgit, le neveu/voisin/facteur est reparti pour un tour de manège.

Alors autant je peux comprendre qu’on n’en ait rien à faire des concepts du libre, autant c’est plus embêtant quand on pense que ça ne dérange pas le neuveu/voisin/facteur de venir faire 153 fois une manipulation tout simple parce que le non-informaticien ne veut pas faire l’effort de comprendre.

Étant perçu dans mon entourage proche comme "l'expert en informatique" (comme quoi tout arrive), je trouve bien plus agaçant cette manie qu'ont certains de mes amis à s'imaginer que règler leurs petits pépins représente un challenge intellectuel que je me dois de relever. Je n'appelle pas mes amis artistes pour repeindre mes toilettes après tout. Ceci dit, le hobbyiste passionné peut être horriblement agaçant aussi. Les grandes campagnes d'évangélisation qui fleurissent sur le net pour un navigateur, un langage ou tout autre logiciel minoritaire (à divers degrés), même si elles partent d'une bonne intention, se transforment bien trop souvent en guerre des chiffres, et toute cette énergie serait probablement bien mieux utilisée à contribuer à un projet phare mettant en valeur le-dit logiciel.

Je pense que tu as une vision très juste du problème des "spécialistes" et des gens que ça n’intéresse simplement pas.

Par contre, si je conçois bien que pour "ma mère" la question du logiciel libre soit de l’ordre du méta-physique, ce qui me choque vraiment, c’est dans le milieu professionnel, lorsque quelqu’un refuse de sortir de sa "petite" spécialisation (ex : "Non, moi je code _uniquement_ en tel langage, le reste, je n’y touche pas.").

Merci pour cet article fort instructif qui couplé à ton tutoriel sur le siteduzero permet de pénétrer dans le monde, qui semble magnifique, du typage. Typed Scheme me semble être très intéressant vu que pour le moment, je ne me suis attardé que sur des langages au typage dynamique (Python, Scheme) malgré une rapide lecture d'un début d'Ada. En tout cas, ce fut un article édifiant.

Merci beaucoup pour cet article très interessant, et très concret. Il apporte de nouveaux élements par rapport à ton texte sur le siteduzero, et je comprend maintenant mieux tous les enjeux du typage.

Le typage dynamique attend l’exécution du programme pour faire les vérifications de correction du typage. C’est un modèle « moins prise de tête » puisqu’il est toujours plus facile de vérifier dynamiquement que statiquement, mais on ne vérifie pas les mêmes choses. Typiquement un programme statiquement typé qui ne produit pas d’erreur de typage à la compilation te garantit qu’il « ne provoquera pas d’erreur de typage quel que soit le chemin d’exécution d’une instance du programme » (quelles que soient les entrées que tu lui donnes, les nombres aléatoires qu’il choisit, etc.), alors qu’un programme dynamiquement typé qui s’est exécuté et a terminé sans erreur de typage te garantit que « ce chemin d’exécution particulier ne contient pas d’erreur de typage ». C’est une garantie beaucoup plus faible, et donc aussi beaucoup plus facile à obtenir (c’est un avantage) : il s’agit d’un compromis.

De plus, pour des raisons théoriques fondamentales, le typage statique d’un langage généraliste ne peut pas être parfaitement précis : si le typage statique rejette tous les programmes erronés, il doit aussi rejeter quelques programmes corrects (par exemple print_int (if true then 1 else "impossible") ne peut pas provoquer d’erreur de typage, mais le compilateur le rejette). Plus les systèmes de types sont simples, plus ils sont contraignants, et rejettent des programmes qu’on aimerait qu’ils acceptent; inversement, plus ils sont compliqués, et plus le programmeur doit faire d’effort pour travailler avec le système de type, ce dont il n’a pas forcément envie.

Enfin, les langages dynamiques proposent en général des méthologies de développement un peu différentes de celle des langages statiques, qui ont leurs avantages et leurs inconvénients. Certains programmeurs affirment même qu’on pense différemment quand on programme dans l’un ou l’autre; je ne suis pas convaincu, mais ce qui est certain c’est que beaucoup de gens sont très satisfaits de langages très dynamiques, et qu’ils font avec des choses intéressantes.

Dans un langage fonctionnel, il y a des valeurs qui dépendent d’autres valeurs (par exemple, let singleton x = [x]), ce sont des fonctions, et des types qui dépendent d’autres types, ce sont les types paramétrés (type 'a liste = Nil | Cons of 'a * 'a liste).

Un type dépendant est un type qui dépend d’une valeur (autrement dit, indexé par une valeur). Ça n’existe pas en OCaml. Un exemple courant serait le type ('a, n) vect, où n est un entier, qui représente le type des tableaux à n éléments de type 'a.

C’est un typage très expressif mais aussi très sophistiqué, et qui casse un peu la distinction habituelle « phase de typage / phase d’exécution » : pour typer correctement un programme, il faut aussi en exécuter des parties. C’est cantonné à des langages de recherche pour l’instant.

Les types dépendants ont des liens forts avec les systèmes de preuve, car tu peux encoder des propositions logiques avec des types dépendants, et inversement quand tu as des types dépendants, tu as envie de pouvoir exprimer des propositions logiques. Par exemple la fonction d’accès à un tableau dépendant ressemblera à ('a, n) vect -> {m tel que 0 <= m < n} -> 'a : si tu ne peux pas exprimer le fait que l’index d’accès est dans les bornes du tableau, ce n’est pas très intéressant d’avoir accès à sa taille au niveau du typage. Ici le tel que ... est un bout de programme « logique ».

• En quoi consistent exactement les types dépendants ?
• Quels sont les avantages du typage dynamique par rapport au typage statique, dans quels cas est-ce vraiment nécessaire ?

Bonjour !

J'arrive après la bataille, mais je tiens à dire tout l'intérêt que j'ai porté à cet article. Il me semble que l'idée maîtresse développée ici peut être généralisée et sortie hors du domaine de l'informatique. Ainsi, l'interaction entre un langage et un méta-langage est féconde car elle oblige à prendre du recul vis-à-vis de ce que l'on fait et amène à des changements de perspective très profitables (que l'on ne pratique pas spontanément).

Merci pour vos commentaires. Je suis déoslé d’avoir mis si longtemps à répondre, mais voilà.

SpiceGuid : je ne suis pas complètement convaincu par ton idée de « typage comme outil de conception » . Je vois bien comment le typage peut renforcer une méthode de conception donnée, en rendant les interfaces plus explicites par exemple, mais je ne vois pas ce que tu as en tête quand tu parles du typage comme une « assistance à la conception » qui remplacerait une méthodologie particulière (UML, patterns, waterfall, iterative refinement..). Par exemple, dans Coq (je prends cet exemple parce que je sais que tu connais), qui a un système de typage des plus expressifs, la conception logicielle à moyenne/grande échelle ne va pas du tout de soi, au contraire il y a souvent plusieurs façons de faire les choses (par exemple on peut souvent définir un prédicat dans Prop par un type inductif paramétré, et c’est une approche intéressante mais qui ne convient pas forcément dans toutes les situations).

Je n’essaie pas de te contredire, je pense simplement que je ne saisis pas vraiment ce que tu veux dire, et que tu devrais développer un peu plus. Ton autre idée de « types dont la sophistication accompagne celle du programmeur » est par contre bien connue, et intéressante (je pense que c’est en fait un cas particulier de l’approche de « couches de langages » croissantes utilisées pour l’enseignement, cf. DrScheme par exemple). En pratique elle n’est pas complètement triviale, mais demande une réflexion sur la présentation du langage. Par exemple si la bibliothèque standard utilise des types très sophistiqués (on aurait a priori envie qu’elle nous apporte le typage le plus expressif possible, pour ne pas avoir à réinventer la roue), il faut que ça reste compréhensible pour le novice, sinon son monde des types simples prend l’eau. Ça demande donc une réflexion sur des types "peu invasifs" (éviter les choses comme les variantes polymorphes de OCaml par exemple qui ont tendance à se glisser rapidement dans les messages d’erreurs du code utilisateur, ou les types équi-récursifs qui ont des conséquences subtiles sur les programmes acceptés), et sur une "vulgarisation" des types du langage, comme le font les gens de C++ pour utiliser la STL sans comprendre les templates (c’est aussi lié au débat sur les concepts de C++[01]x), ou les débutants en Haskell qui font de l’entrée-sortie sans comprendre les monades. À ce sujet, j’avais lu un article sur la présentation de la monade IO aux débutants, en présentant main comme une "entrée du contexte extérieur" dans le programme, mais je n’arrive plus à remettre la main dessus.

Proairgun : le polymorphisme ad-hoc est une fonctionnalité parfois intéressante, mais dont on abuse à mon avis souvent (un peu comme la frénésie POO pousse les gens à voir de l’héritage dans tous les sens alors que c’est parfois la pire des solutions). Beaucoup de gens utilisent le polymorphisme ad-hoc d’une façon en fait analogue aux types sommes des langages fonctionnels (un type dont les valeurs sont divisées en plusieurs "cas" : adulte, enfant, vieillard par exmple), sans voir qu’ils ne gagnent pas en simplicité ou clarté par rapport à cette solution fonctionnelle.

Sprank : le typage d’OCaml permet évidemment d’exprimer la taille des entiers que tu manipules. Jette un oeil par exemple à la bibliothèque Bigarray (déjà mentionnée sur ce blog d’ailleurs). Après, je ne cherche pas qu’à défendre ma chappelle, le langage C peut être un bon choix pour ce genre d’applications, ou C++ quand tu veux du plus haut niveau sans perdre l’interface bas niveau du C, cf. Factor (si j’en ressors indemne… ;), mais pas pour des raisons de typage. Du reste, les même manipulation en OCaml seront sans doute moins efficaces, car le compilateur n’offre pas de support particulier à ces valeurs, qui font donc bien la bonne taille mais ont tendance à être boxées, ce qui nuit aux performances. Les bénéfices d’abstraction, et des choix soigneux d’interface bas-niveau peuvent quand même rendre le Caml compétitif dans ce secteur.

Comme le dit très bien minh, il faut faire attention à l’implicite en programmation. Je pense que la propriété fondamentale qui rend le typage ML agréable, ce n’est pas qu’il est possible d’inférer les types des programmes, mais que c’est une opération simple et bien définie. Un utilisateur peut très raisonnablement, avec un peu d’entraînement, deviner le type qui sera inféré pour son programme. Au contraire, un système dont les déductions sont imprévisibles (et ça a tendance à être le cas quand on monque en sophistication, car la puissance entraîne souvent une certaine fragilité, cf. le problème de l’arrêt) serait dangereux. Dans la recherche des gens qui font de l’inférence pour des typages plus sophistiqués que ML, une grande partie des efforts consiste à trouver des systèmes plutôt faciles à comprendre, et dont les erreurs soient compréhensibles et simple à réparer (en ajoutant par exemple une annotation à un endroit donné, mais il faut qu’on sache où annoter, et pas tatonner jusqu’à que le compilateur accepte).

Il y a en fait un parallèle avec l’idée formulée par SpiceGuid selon laquelle les types utilisés par un programmeur correspondent à son niveau d’expertise : utiliser des types plus puissants demande plus d’efforts (qu’un expert est plus à même de fournir). Alors, l’intérêt de l’inférence totale diminue, car les annotations se mettent à représenter une partie nettement plus faible de l’effort de typage, indépendamment du fait qu’une inférence complète devient en général indécidable.

Je ne connaissais pas le problème de l'arrêt et effectivement, s'il n'y a aucun algorithme qui puisse déterminer si un programme arrête ou non dans tous les cas, mon rêve de super-compilateur tombe à l'eau.

HS : C'est qui "la carotte" ?

Pour l'histoire de la factorielle, il me semble que réaliser ce que tu proposes reviendrait à réaliser un compilateur qui saurait détecter une boucle ou une récursion infinie, ce qui est impossible (car équivalent au problème de l'arrêt si je ne me trompe).

Comme toujours, article extrêmement intéressant en tout cas ! Un grand merci Bluestorm !

Sprank > À mon avis, un tel compilateur serait difficile à utiliser, car à partir du moment où certaines informations utiles (comme le domaine de ta fonction factorielle, p.ex.) sont inférables mais d’autres non, le programmeur risque de laisser passer des choses qu’il aurait pu spécifier explicitement mais qu’il a cru que le compilateur saurait inférer pour lui, et c’est un chemin dangereux…

’Fin bon, chui pour des choses plus systématiques ; quoi qu’en disent les puristes comme SpiceGuid ici présent, je pense que la méthodologie, ça a du bon, dans la pratique. :-° Trop de finesse dans le fonctionnement tend à introduire des erreurs dues à un malentendu entre le programmeur et l’outil. (Wow, avec un commentaire comme ça, si j’en ressors indemne… :-’)

Sinon, pour l’histoire des types 4 ou 12 bits, à mon avis, c’est pas pertinent de considérer que c’est plus bas niveau, parce qu’à moins que tu programmes sur des cartes intégrées que tu construis toi-même, il y a peu de chances pour que le proco offre de tels types ; en ce sens, les proposer au programmeur, ce serait créer une abstraction supplémentaire donc c’est du haut niveau, à mon sens.

Récemment je me suis (re)mis un à projet plutôt bas niveau par rapport à ce que je suis habitué de faire (un émulateur Chip-8 si vous voulez savoir). J'ai choisi de le faire en C++ (pour utiliser SFML et la pile de la STL sinon c'est du C). Le typage de C++ ici m'est plus utile que celui d'OCaml (par exemple) car plus expressif : il me permet de facilement jongler entre entiers signés/non-signés de 8 ou 16 bits, même si pour d'autres projets OCaml et son typage seraient probablement d'un plus grand secours. Je me suis même surpris à vouloir un typage encore plus "bas niveau" pour pouvoir définir des entiers de 12 ou 4 bits. Ça m'amène à me demander si ça a du sens de parler d'expressivité haut/bas niveau pour un système de typage.

Sinon j'ai toujours rêvé d'un super compilateur qui serait capable d'inférer encore plus de choses sur les types, un genre de compilateur OCaml puissance 10. Par exemple si je définis une fonction factorielle, le compilateur devrait être capable de deviner tout seul que le domaine de la fonction est les entiers naturels et m'avertir si des parties de mon code peuvent possiblement donner des entiers négatifs à la fonction factorielle. Un compilateur qui infère le plus de choses possible, et qui permet au programmeur de définir ce qui n'est pas inférable.

Ce que je n'arrive toujours pas à saisir malgré cette article très enrichissant, c'est l'utilité du typage statique. Ayant fait un peu d'ocaml et partant du php ( ouh le pas beau ) j'ai découvert avec émerveillement le polymorphisme ad-hoc plus que le polymorphisme tout court qui aux yeux d'amateurs comme moi, me semble gadget. Néanmoins, pour un programmeur qui organise bien son code, le typage me parait plus un accélérateur de  programme en aidant la compilation qu'une véritable instruction avec quoi  le langage révèle ses richesses. Ainsi en sacrifiant les performances, le php n'est pas limité par rapport à l'ocaml à cause de son typage ( Je serait heureux que l'on m'éclaire à ce sujet ). Pourtant je vois l'insuffisance du typage dans beaucoup de critique sue le php alors que cela  m'apparait plus une contrainte qu'un avantage.

Un article intéressant.
Ta réponse est satisfaisante dans le sens où elle fait quasiment le tour de la question.
À mon avis il manque quand même un aspect essentiel. C'est que le système de typage est ce qu'il y a de plus proche d'une assistance à la conception, bien plus intéressante qu'une méthode de conception planifiée. Le typage guide la conception et la rend plus explicite. Bien mieux et bien plus systématiquement que UML ou les design patterns.
Plutôt qu'un bon panorama des choix de conception en matière de systèmes de types (chose qui concerne sans doute très peu de zéros) je crois que j'aurais préféré une vraie propagande en faveur d'un typage statique plus expressif.

Ce que j'ai envie de répondre à robocop: le typage n'est pas une vérification, c'est une méthode de conception en soi. Autant que possible (et dans la mesure du raisonnable, en fonction de l'expérience de chacun) le typage peut supporter la spécification. Plus un programmeur est expérimenté plus il peut ajouter de la spécification dans le typage. Et le langage doit pouvoir l'accompagner aussi loin que possible.

Il faut tordre le coup aux paradigmes. Il n'y a pas de paradigmes, il n'y a que des styles. Il n'y a pas de fonctionnalités avancées, il n'y a que des types avancés. Par exemple il n'y aura rien que l'on puisse faire avec les valeurs-modules de ocaml 3.12 qu'on ne peut pas déjà faire avec ocaml 3.11. Par contre on pourra sans doute typer des choses qu'on ne peut pas typer actuellement. Avec pour conséquence des messages d'erreur sans doute plus obscurs. Le débutant n'y gagnera rien d'autre que de nouvelles opportunités de s'engager sur un chemin qui n'est pas pratiquable pour lui.  

Car les types c'est avant tout un éventail de possibilités pour accompagner chaque programmeur selon son niveau. C'est une assistance personnalisée. Il y a les types élémentaires ou atomiques. Il y a les types composites simples. Puis il y a des types plus structurés. Ensuite il y a des types pour les experts. Et enfin il y a les types dépendants pour les logiciens.

Je ne suis pas un Ayatollah du typage statique. Les langages à typage dynamique existeront toujours et ils n'ont pas moins de mérites que les autres, ils sont même bien souvent les pionniers. Ce que je ne comprends pas ce sont les langages comme Go, typé statiquement mais qui n'a pas le polymorphisme, qui possède les closures mais qui n'a pas de type fonctionnel.

Si un article manquait à toute la série d'articles que tu as écrite, pour moi, c'est celui-là. Ce vide est comblé, merci !