Ours & Hippy — le blog [langages]

Hum, ouais, avant on écrivait facilement x << 1 au lieu de x * 2. C’est d’ailleurs pas mal resté, dans certains cas. Mais yavait des trucs bien plus gores, genre des macros REGISTERn qui sont remplacées par des déclarations register selon la machine (ça permettait de classer par priorité les variables à mettre dans des registres ; les suivantes devenaient automatiques).

À propos de rugosité, je suis tombé récemment sur un assez vieil (2003) article sur MSDN sur comment rendre le code managé rapide et on peut y lire :

Good C programmers knew. Each operator and operation in C, be it assignment, integer or floating-point math, dereference, or function call, mapped more or less one-to-one to a single primitive machine operation.

C’est de moins en moins vrai avec l’avénement des compilateurs optimisants modernes, mais il y a toujours une certaine vérité à cela, en ce que l’on peut se donner une vague borne pessimiste sur nos performances, en gros. :p

Après, pour ce qui est d’instruire au compilateur comment effectuer certaines optimisations, euh… je ne vois pas trop où tu veux en venir. Tu peux développer ? Au final, on est limité au niveau langage, on ne peut pas vraiment toucher au-dessous. Que suggères-tu ? À quels langages penses-tu ?

J’ai toujours trouvé dommage qu’en C, les optimisations ne soient que locales : Il est facile de rajouter une couche d’abstraction pour spécialiser un bout de code avec des macros, mais le gain est limité au programme courant. Passer au cap supérieur et instruire directement le compilateur d’une optimisation possible n’est pas aussi simple que, par exemple, abstraire une fonction d’un bloc de code répétitif.

À mes yeux, il semble y avoir une ambivalence entre le désir d’être explicite (j’écris x.foo et j’ai une bonne idée mentale du code produit par le compilateur) et le désir d’être efficace, c’est à dire de rajouter des optimisations non existante dans le compilateur (ou qu’on suppose non existante.) Avec ton exemple, on perd complètement l’explicite et on obtient quelque chose d’assez boite noire, mais qui "fait le travail."

J’ai envie de penser que les "optimisations" suivantes devaient exister lors des premiers compilateurs (non-optimisants) (bien qu’elles aient probablement toujours été écrites directement) :

#define MUL(x, y) (x) * (y)
#define MUL2(x)   (x) << 1

En résumé, je ne suis pas sûr d’apprécier la distance entre ces optimisations de bas niveau et le compilateur (le pré-procésseur et l’assembleur étant placés aux extrêmes), mais ça résume assez bien ma vision du C. C’est un langage assez riche et compliqué, mais il est rugueux : Chaque concept est clairement délimité syntaxiquement, ce qui introduit sa dose de complexité au niveau de la grammaire, mais permet aux programmeurs de s’agripper solidement.

En Scheme, le problème est inverse : Il n’y a pas de rugosité du tout et le programmeur est perdu. Je trouve donc amusant que les macros C, qui sont nettement inférieures aux macros Lisp, aient l’avantage de cette limitation pour la structuration intellectuelle du programmeur. "S’il y a de la magie, elle tient toujours dans ma tête." Le problème n’est donc pas la notation préfixe mais "qu’est-ce qui se passe derrière ?"

D’une certaine manière, je trouve qu’OCaml a hérité de cette rugosité vis à vis des records, des accès aux tableaux et des constructeurs. Et ça m’emmerde à chaque fois que je les utilise. :)

Plutôt que de reciter Lisp et Forth, qui sont des solutions à mon goût à ce problème, mais qui souffrent également de leur solution, voici un lien qui propose d’utiliser des compilateurs orientés "extensions" pour le C : http://pdos.csail.mit.edu/xoc/ .

Je m’intéresse assez aux à la question de l’encodage, dans un langage plus bas niveau, des fonctionnalités d’un langage plus haut niveau. C’est un outil qui permet de comparer différents langages entre eux (tant d’un point de vue pratique que théorique : la traduction d’une solution vers une autre est une façon courante pour des chercheurs en langages de programmation de comparer ces solutions). J’ai récemment fait un monologue à ce sujet sur le siteduzéro.

Le point de vue que tu abordes est légèrement différent, puisqu’il est centré sur "le langage bas niveau" : en général, on discute de ce qui se passe quand on change de langage pour avoir des constructions plus haut niveau, et on néglige un peu les irréductibles qui veulent conserver leur langage d’avant, et utiliser quand même un style moderne. Les utilisateurs de C ont ce point de vue et c’est assez intéressant. Par ailleurs, la question de la portabilité est assez évidente quand on en parle, mais je n’y avais pas spécialement pensé avant, merci. Cela dit, au sujet de la portabilité, j’ai l’impression que beaucoup de langages font des choix d’implémentation relativement platform independent, comme une machine virtuelle, un bytecode, ou un langage plus bas niveau (C--, LLVM, ou même directement C), et spécialisent la partie bas niveau seulement dans ces couches là, qui sont plus basses que le C. Bien sûr, il y a quand même des choix qui sont fait très tôt, et la question des pointeurs que tu décris en fait sans doute partie.

Une autre application des études de la traduction langage-langage est l’étude de la méta-programmation à l’intérieur d’un langage donné. Par exemple, on peut considérer une partie de la métaprogrammation des LISP (macros et cie.) comme des éliminations d’abstraction syntaxique.

Pas directement lié mais intéressant quand même : http://www.cs.bath.ac.uk/~cf/eff_hyper.pdf

À mon avis certains articles ne veulent pas fermer des portes arbitrairement. Du coup ils peuvent paraitre plus algorithmiques qu’ils ne le sont en vérité.

Quand je lis ce genre de phrase :

"Coherence retains mutable state, abandoning only the Program Counter."

Je ne peux pas m’empêcher de penser que l’article traite en fait du problème de la cohérence dans la maintenance des bases de données. Quand un modèle est trop centré sur la dynamique des données ça en fait une technique d’IA ou de SGBD. Eventuellement ça pourrait aussi être un DSL pour GUI, CAO et 3D interactive.

En développant son propre interpréteur plutôt qu’une librairie pour un langage existant l’auteur prend le risque de faire apparaître la faiblesse de son approche dans le cas général tout en masquant les éventuels avantages par rapport aux approches concurrentes comme le tout impératif ou la FRP.

Pour l'instant, l'idée et le langage associé sont encore en gestation. C'est un article publié dans la conférence "Onwards!" qui s'intéresse à des idées nouvelles et pas encore éprouvées. Je pense qu'il ne gère pas certaines incohérences, par exemple on doit pouvoir provoquer des boucles infinies avec certains programme qui n'ont pas d'entrelacement correct.

Cette réaction est courte, parce que j'aimerais écrire plus de réactions.
D'une part, je ne suis pas satisfait de ma méthode actuelle : je survole beaucoup d'articles, j'en lis quelques uns, et je garde une trace écrite (résumé ou réaction) d'une petite fractions de ces derniers. J'aimerais mieux, à terme, me forcer à commenter plus souvent les articles que je lis, et c'est de là qu'est née l'idée des "réactions". Clairement, je ne peux pas me permettre de passer autant de temps sur chaque réaction que précedemment si je veux en publier plus.
D'autre part, cet article m'a un peu déçu, et je n'ai pas été motivé pour écrire quelque chose de très long. C'est la contrepartie de la volonté à terme de garder une trace de tout ce que je lis : il y aura aussi des choses qui me plaisent moins que les autres. Dans l'idée je pense que parler des papiers qui m'ont moins plu peut être aussi intéressant que parler des papiers qui m'ont plu, mais il faut faire attention à ne pas ennuyer le lecteur par vengeance.

Fondamentalement, je crois qu'il faut que je fasse des choix, entre publier un bon article long et très travaillé tous les deux mois, ou baisser un peu mon propre niveau d'exigence pour avoir des articles plus fréquents. C'est pas facile.


Je te remercie pour ton avis. J'ai bien vu que cette réaction n'avait pas motivé l'enthousiasme des foules, mais c'est beaucoup plus utile pour moi qu'on me dise comme tu l'as fait ce qui gêne ou pose problème.

Article intéressant sur le fond, mais j'avoue que j'aurais aimé en savoir plus sur, par exemple, la manière dont le programme va gérer l'apparition d'interférences, par exemple, comment différencie-t-il une simple interférence (donc à corriger en modifiant l'ordre des  effets de bords) d'une véritable incohérence (qui est donc à signaler comme toute erreur qui se respecte) ?

Par contre, je ne sais pas si tu as refréné ton envie d'écrire pour des raisons personnelles, ou bien parce que tu penses qu'un texte trop long risque de rebuter. Si c'est la deuxième hypothèse, personnellement, c'est toujours un plaisir de te lire, et j'avoue que la longueur de cette réaction me laisse un peu sur ma faim :p (mais ça n'engage que moi).

Merci, une fois encore !

Je te remercie énormément d’avoir pris le temps de me répondre, tout m’est plus clair maintenant.

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 ».

Bluestorm, j’ai deux questions :

• 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 !

Je sais que ce billet a été poster il y a plusieurs mois mais, je viens de le lire et la moindre des choses que je puisse faire en tant que humble lecteur est de laisser mon impression a l'auteur.

N'étant pas un habituer de la programmation fonctionnel, et ne maitrisant que vaguement la syntaxe ocaml, je dois avouer que ce biller est très difficile a lire.

D'une par, il fait appelle a des notions de mathématique qui ne sont pas nécessairement connues des développeurs habituer des langages impératif (J'ai crus entrevoir de la topologie?).
D'autre part, une bonne part de l'article repose sur des illustration reposant sur le langage ML, ce qui demande un effort particulier pour visualiser "a quoi ca ressemble" dans notre langage impératif de prédilection.

(Je conçoit que l'approche fonctionnel et impérative sont fondamentalement différente, mais il est toutefois possible d'effectuer des analogies et d'obtenir un comportement déterministe dans un langage impératif. Après tout, l'ocaml s'exécute sur des architectures matériel que l'on peut décrire comme des machine de Turing)

En fait les deux premiers paragraphes répondent à ma question, c'est cool. Mais j'aime bien aussi la précision du dernier. :)

Merci.

Alors déjà pour le traitement de (A -> B -> C), c’est curryfié, donc c’est exactement équivalent à (A -> (B -> C)). De là on peut sans doute appliquer la définition et obtenir une réponse claire, mais il faut y penser et tu as raison de demander à expliciter ce point là.

Donc : [A -> B -> C], c’est [A -> (B -> C)] soit A -> ({⊥} + [B -> C]), c’est-à-dire A -> ({⊥} + (B -> {⊥} + C)). En gros, tu commences par donner l’argument de type A, et là soit ça plante (⊥), soit tu as une fonction partielle [B -> C] à laquelle tu donnes l’argument de type B. On considère donc la fonction qui prend du B en paramètre seulement dans le cas où ça n’a pas planté.

L’idée c’est que ⊥ n’est pas une valeur. Ça ne correspond pas à un objet qui existe dans notre langage, puisque c’est au contraire l’absence de résultat. Si une fonction termine, elle renvoie une valeur (qu’on dénote par un élément de B) mais sinon elle ne termine pas (par exemple elle boucle à l’infini). Ça n’a donc pas de sens de "passer ⊥ en paramètre" puisque ce n’est pas une valeur du langage : si tu as essayé de faire un calcul qui n’a pas terminé, mathématiquement tu as "⊥", mais informatiquement tu as un plantage et tu ne peux pas "continuer" : passer des paramètres, etc.

C’est donc là qu’on rejoint la notion de "⊥ donne tout le temps ⊥" : une fois que tu atteins ⊥ mathématiquement, le calcul a "échoué" et il reste comme ça. Si f x échoue, alors g (f x) échoue, quelle que soit g : on commence par vouloir f x et c’est l’échec. C’est une autre définition des langages stricts.

On peut aussi consolider l’enrobage avec plus d’enrobage : il y a une idée implicite dans ce que je dis, que je peux formaliser. Je parle de la sémantique (l’objet mathématique correspondant au code informatique) des fonctions, mais pas de celle des applications de fonction. Si f est une expression qui désigne une fonction, et x qui désigne une valeur, quel est l’objet mathématique [f x] correspondant à l’application de f à z ?

• si [f] = ⊥, c’est ⊥
• sinon c’est [f]([x]) : [f] est une fonction partielle, donc le résultat peut encore être ⊥

Avec cette définition plus précise, tu peux raisonner formellement (et donc précisément), mais je pense pas que ce soit ce dont tu avais besoin. Ça pourrait cependant servir pour d’autres questions.