Re: Joli journal

Merci pour ton commentaire.

L'inconvénient bien sûr, c'est que le résultat est très long, trop long je pense pour que quelqu'un qui découvre puisse confortablement le lire en une seule fois. Il faut espérer que les gens ont la discipline de faire des pauses et de reprendre la suite un autre jour, même si la structure ne l'encourage pas forcément.

Effectivement, l'article est long et dense. Il faudra y revenir plus d'une fois pour les lecteurs qui voudraient le comprendre. Et encore, j'ai fait des coupes : au départ j'abordais la problématique de l'héritage multiple par exemple. J'ai hésité, également, à le couper en plusieurs journaux mais j'ai finalement choisi cette forme en me disant que le lecteur le lirai plus d'une fois.

As-tu envisagé de le convertir en un tutoriel sur Zeste de Savoir ? C'est un site avec de bonnes valeurs d'ouverture et de diffusion de la connaisance, une équipe sympathique, et plus adaptée au stockage à long terme des connaissances que les journaux de LinuxFR, il me semble.

Je ne connaissais pas, j'y réfléchirai. Pour un tutoriel comme celui-ci, c'est sans doute une bonne idée.

Quand tu dis que le typage des GADTs n'est pas "décidable", tu veux dire qu'il n'est pas "inférable": c'est le fait de deviner le type qui n'est pas décidable, pas le fait de vérifier qu'un type donné est correct (qui est ce qu'on entend par "typage décidable").

Effectivement je me suis mal exprimé, je voulais bien dire que c'est l'inférence qui est indécidable dans le cas général pour les GADT. Vérifier la correction d'une preuve, c'est toujours décidable. Trouver une preuve, en revanche... ;-)

Un pointeur complémentaire sur les GADTs, francophone, serait le cours de Programmation Fonctionnelle Avancée de Roberto di Cosmo (ou des autres enseignants ayant donné le même cours à Paris 7).

Merci pour la référence, je n'y avais pas pensé. Pourtant je me suis rendu plus d'une fois sur le site de Roberto Di Cosmo.

Au passage, une question qui n'a rien à voir avec le thème du journal. Sais-tu pourquoi les where statement ont disparu du langage OCaml ? Je pense à cela car dans le cours de Paris 7, il y a une leçon sur les zipper, et dans son article sur le sujet Gérard Huet en faisait usage. Je trouve cette perte dommage, cela permet d'écrire des codes plus élégants, et la beauté dans le code c'est important ! Comme il répondait dans un interview, sur le blog de la SIF (Société Informatique de France), intitulée Poésie et esthétisme du logiciel :

— Binaire : [...] Mais tu as dépassé l’état de le compréhension. Tu nous parles d’esthétique : un programme informatique peut-il être beau ?

—Gérard Huet : Bien sûr. Son rôle est d’abord d’exposer la beauté de l’algorithme sous-jacent. L’esthétique, c’est plus important qu’il n’y paraît. Elle a des motivations pratiques, concrètes. D’abord, les programmes les plus beaux sont souvent les plus efficaces. Ils vont à l’essentiel sans perdre du temps dans des détails, des circonvolutions inutiles. Et puis un système informatique est un objet parfois très gros qui finit par avoir sa propre vie. Les programmeurs vont et viennent. Le système continue d’être utilisé. La beauté, la lisibilité des programmes est essentielle pour transmettre les connaissances qui s’accumulent dans ces programmes d’une génération de programmeurs à l’autre qui ont comme mission de pérenniser le fonctionnement du système.

Pour les programmes, de même que pour les preuves, il ne faut jamais se satisfaire du premier jet. On est content quand ça marche, bien sûr, mais c’est à ce moment là que le travail intéressant commence, qu’on regarde comment nettoyer, réorganiser le programme, et c’est souvent dans ce travail qu’on découvre les bonnes notions. On peut avoir à le réécrire tout ou en partie, l’améliorer, le rendre plus beau.

Et je suis bien d'accord avec lui : un théorème vrai, c'est important. Mais une belle démonstration l'est tout autant ! Elle permet de mieux saisir les raisons profondes de la vérité du résultat et d'éclairer son harmonie sous-jacente.

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.

Et comme les programmes sont des preuves. :-)

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