Perthmâd a écrit 224 commentaires

Le cas de Coq est un peu particulier, parce qu'il s'agit en fait d'au moins deux langages différents, Gallina, le langage de preuve en tant que tel, et Ltac, un langage de métaprogrammation qui est à Gallina ce que PHP est à HTML. Autant Gallina est plutôt bien spécifié[1], autant Ltac est un bousin sans nom qui est la source d'un tas de problèmes, le genre de code qu'il suffit de regarder fixement pour faire péter un développement à l'autre bout de la planète. Ceci dit, il y a eu du progrès depuis et l'utilisation d'une infrastructure d'intégration continue un peu sérieuse permet de jauger la casse avant la publication d'une version.

En ce qui concerne Bedrock, je me permets quand même de juger que c'est un cas vraiment extrême. C'est un projet notablement connu pour avoir été implémenté par des gens qui sont des spécialistes internationaux de l'exploitation de bug à des fins particulièrement créatives. Personnellement, ma réaction naturelle serait de les secouer très fort jusqu'à ce qu'ils comprennent que ce qu'ils font donne des envies suicidaires et/ou meutrières à l'équipe de développement de Coq.

[1] Bon en fait, n'importe quel spécialiste de la théorie des types sait que c'est pas vrai non plus, mais au moins c'est un langage plutôt robuste en terme de compatibilité.

Je me permettrai d'avoir une pensée émue pour FacWeb, une interface dédiée au remplissage de feuille de temps pour les projets ERC d'Inria-inventeurs-du-monde-numérique. Outre le fait que l'ergonomie de l'interface en elle-même rendrait fou un hiéromoine tibétain, sa finalité, voire sa sémantique demeurent pour moi parfaitement mystérieuses. Serge Abiteboul, qui est loin d'être un perrave, a d'ailleurs un jour ragé publiquement à ce sujet avec bien plus de classe que moi, qui suis un peu just.

La seule chose qui me fait chaud au cœur, c'est l'image d'Épinal que des technocrates en blazer se paluchent devant des métriques d'excellence, en songeant que le 12 janvier 2016 j'ai effectué 0.85 unités de recherche pour faire progresser l'innovation.

Par planter je veux dire : signal fatal genre SIGSEGV… ou SIGILL.

Note bien que SIGSEGV c'est le cas idéal du code qui fait n'importe quoi avec la mémoire : ça veut dire que ton OS s'en est rendu compte. Il y a bien plus insidieux, c'est quand ton programme corrompt la mémoire silencieusement dans ton dos, et là t'es dans la mouise. Le système de types de Rust ne dit rien à propos d'un signal fatal, et plus généralement que ton programme est correct par rapport à une spécification qui n'existe que dans la tête du développeur (quand elle existe). Par contre, il te garantit le même genre de sûreté que les langages à GC, sans avoir de GC lui-même, ce qui n'a rien à voir avec 'planter'.

Il y a une issue de secours : le mot clé unsafe. […] Vous savez alors que vous avez une petite partie de votre code qui n’est pas sûre. Si ensuite votre programme plante, ça viendra de là !

Bien que fervent soutien de Rust (et même actuellement membre de RustBelt), je me permets de réagir à cette remarque. Je souhaiterais faire remarquer que ceci est une croyance assez répandue, mais complètement foireuse.

La programmation à coup d'unsafe en Rust a des répercussions non-locales qui sont dues au fait que la sémantique d'une structure de donnée est décrite par son API, qui constitue un tout, et non pas par chaque fonction une par une. En gros, ça veut dire que la validité d'un code unsafe dépend de l'ensemble des interfaces transparentes qui en dépendent, ce qui peut être nettement plus vaste que le code dans un bloc unsafe. Il y a un très bon post de blog par Ralf Jung à ce sujet pour les gens intéressés.

Moi perso j'utilise ibus + latex-tables, qui fournit des caractères unicodes avec les mnémoniques LaTeX. C'est pas trop mal, modulo le fait que ça utilise l'anti-slash très mal placé sur mon clavier comme caractère d'échappement.

Pas vraiment, la curryfication c'est juste l'isomorphisme A × B → C ≅ A → B → C, et il n'y a pas de type fonctionnel impliqué ici. Ici ça serait plutôt genre l'associativité du produit ou un truc comme ça.

Fun fact: la curryification n'est pas valide en call-by-value avec effets (donc en particulier en OCaml). Il y a plus de monde dans A → B → C que dans A × B → C. Exemple: fun (x : unit) -> (raise Exit : unit -> unit) ne peut pas être écrite comme une fonction de la forme fun (x, y) -> qqch.

Ce n'est pas monstrueux, c'est le comportement uniforme des types inductifs. Le seul point un peu subtil vient du front-end, qui fait que dans la syntaxe des arguments des types inductifs, les parenthèses sont signifiantes à toplevel. On peut s'en rendre compte en pratique en écrivant :

type foo = Foo of (int * int)
let pfoo (Foo p) = p (* marche, type foo -> int * int *)

type bar = Bar of int * int
let pbar (Bar p) = p (* marche pas, mismatch du nombre d'arguments *)

C'est implicitement spécifié dans la syntaxe formelle de la description des types inductifs, qui dit bien que ça prend une expression de la forme typexpr1 * ... * typexprn et pas juste un typexpr.

Ceci dit, avec les dernières version d'OCaml on peut commencer à faire des trucs vraiment gorky en utilisant des attributs unboxed pour compiler certains types sans les indirections intermédiaires. Heureusement c'est opt-in, et c'est pas observable dans le langage de toute façon. Seuls les gens qui font des bindings C doivent faire gaffe à ce genre de truc, ou à la rigueur si le programme est vraiment tendax sur les perfs.

Ta solution, bien que résolvant ta problématique, rajoute une indirection en mémoire : tes types sont des pointeurs sur des couples de int

Pas forcément, ça dépend de la manière dont le type est écrit. Si tu écris

type coord = Coord of (int * int)

la représentation sera un constructeur à un argument (i.e. un 'fat pointer') vers une paire d'entiers (soit au total 5 mots mémoire). Si tu écris au contraire

type coord = Coord of int * int

sans les parenthèses, cela sera représenté par un constructeur à deux arguments entiers (soit au total 3 mots mémoire) ce qui est strictement équivalent en mémoire à un terme de type int * int.

En pratique, la différence entre 0 et -0 est faible.

Je me souviens cependant d'un exposé d'un chercheur bossant sur la preuve de programmes flottants qui nous avait expliqué qu'un avion de chasse avait failli partir dans le décor à cause de cette différence…

Je doute fortement que ce soit un vulgaire commentaire pour l'auteur : il m'est parfaitement compréhensible, et je suppute qu'il en est de même pour son auteur.

C'est dommage, parce que ce commentaire n'a précisément aucun sens, vu que la catégorie Hask n'existe pas!

Sept personnes préfèrent faire de la preuve en Coq ! Sans parler du fait même que l'option apparaisse dans le sondage. Probablement un paradoxe temporel dont l'issue engendrerait une réaction en chaîne qui pourrait déchirer le tissu même du continuum espace-temps, provoquant la destruction totale de l'Univers…

J'ai néanmoins une question sur la source de l'efficacité de la construction dans le cas où l'on ne parcours l'arbre qu'une seule fois. L'AST semble être représenté par des fermetures sur ses « constructeurs », ce qui en fait une sorte de construction paresseuse, et quand on l'évalue on le construit pour le consommer de concert, c'est cela ? Si je vois à peu près ce que l'on gagne en temps (ça évite de construire l'arbre d'abord, puis de le parcourir ensuite pour l'interpréter), quel est le coût en espace de toutes ces fermetures ?

D'après nos tests, c'est en pratique toujours plus efficace en mémoire que de construire l'arbre d'un coup. En effet, la taille des clôtures est plus généralement petite que la taille de l'arbre en cours de création qui est garbage collectée au fur et à mesure, ce qui n'est pas le cas quand l'arbre est construit à priori.

Je peux te prouver que c'est complet pour une raison bien simple : c'est exactement le fameux (et notoirement incompréhensible) visitor pattern de la programmation objet, mais typé de manière raisonnable…

Maintenant que tout ça a été re-dit, la question—que nous semblons tous aussi déjà avoir soulevée—c'est de montrer quels sont les avantages une fois qu'on a passé cette étape. Là je botte en touche… (Sans doute faudrait-il partir d'un exemple qui ne soit pas un jouet.)

Je peux témoigner que dans le cas d'OCaml, cette représentation libre est beaucoup plus efficace sous l'hypothèse qu'on ne traverse l'arbre qu'une fois, et est de plus tail-récursive par construction. Cette technique est utilisée dans Coq pour représenter des listes paresseuses dans la monade du moteur de preuve.

(À lire sur le ton de « A monad is just a monoid in the category of endofunctors » :)

Allons bon, pourquoi tant d'émerveillement devant la simple application du lemme de Yoneda à la catégorie des algèbres?

Vu que tu es (je suppose mais corrige moi si je me trompe) un homme cisgenre (pas transgenre), à priori t’es plutôt du côté privilégié

Ouaip, je sais…

Ceci étant… Pour les personnes transgenres, t’es tellement largement en-dessous des estimations les plus basses! O_o

D'après le site sur lequel j'ai trouvé ça, ça vient du rapport HAS 2009 (de mémoire).

Je pense qu’on ne peut pas comprendre correctement le genre et le patriarcat sans intégrer les personnes trans dans la réflexion. Et mieux comprendre le genre ça aide à combattre les normes de genre.

Ça va peut-être t'étonner, mais je suis complètement d'accord avec ça sur le fond.

Cependant, et pour me permettre une analogie tout à fait foireuse, la fixette sur les subtilités de genre dans le discours féministe moderne me fait le même effet que si les textes promouvant le libre commençaient tous par : « D'ailleurs, les systèmes d'exploitation libres ne se résument pas à Linux. Il y a aussi des gens sous Haiku qui en chient des briques au quotidien. » C'est vrai, mais on s'en fout. Le plus important c'est le logiciel libre, pas les tétrachiées de situations individuelles possibles.

Ceci étant dit, merci pour tes liens, j'en garde quelques-uns sous le coude !

De plus, je tiens à te faire remarquer que mâle/femelle c’est pas la même chose qu’homme/femme (même si souvent lié), mais c’est pas très simple ni intéressant pour notre sujet. D’autre part, et quasiment tous les liens ci-dessous font cette erreur, les genres ne se limitent pas qu’à homme ou femme.

Qu'on me traite d'archéo-marxiste, mais c'est bien ce qui m'emmerde avec les courants de pensée issus de la French Theory : pourquoi diable monter en épingle les histoires de genre qui concernent une infime partie de l'humanité (pour ce qui est des trans, ils représenteraient entre 0,002% et 0,01% de la population) quand la plus grande partie de celle-ci (les femmes constituent 50,5% de la population mondiale) continue à vivre sous le joug de l'oppression masculine dans une semi-indifférence molle ?

Chacun est libre de militer pour ce qu'il veut, mais je tenais quand même à rappeler les ordres de grandeurs.

Et les fonctions sont aussi des Monads…

Ça ne veut pas dire grand chose à priori que les fonctions sont des monades^*, tu veux probablement parler du foncteur (A → _) pour un A fixé. Mais dans ce cas, c'est juste la bonne vieille monade reader, pas de quoi casser trois pattes à un lambda !

[*] La théorie des catégories est le genre de contexte dans lequel n'importe quel énoncé peut avoir du sens, donc je fais gaffe quand même.

"Mon dieu, les fonctions sont aussi des Monoids"

Et les monades sont aussi des monoïdes. Mouahahaha !

D'ailleurs je suis d'origine Bretonne du côté de mon père et ma grand-mère, qui parle couramment le Breton m'a toujours dit que la langue était selon elle héritait du Gaulois. Bon après je sais pas si c'est vrai, mais c'est apparemment une croyance répandue.

C'est vraiment faux, en fait. Les langues celtiques se divisaient en deux branches, le celtique continental, éteint aujourd'hui et duquel faisait partie le gaulois, et le celtique insulaire, qui contient toutes les langues celtiques modernes dont le breton. Les deux branches sont vraiment distinctes, le celtique insulaire ayant eu son lot d'évolutions depuis l'indo-européen qui le sépare du continenal.

La branche insulaire s'appelle ainsi car elle provient exclusivement de l'archipel de la Grande-Bretagne et de l'Irlande. Le breton a été réintroduit tardivement par les populations brittoniques qui se sont faites éjecter de Grande-Bretagne par l'arrivée de populations germaniques profitant de la faiblesse de l'Empire Romain. C'est pourquoi le plus proche parent plus ou moins pas mort du breton est le cornique, parlé en Cornouailles (la grande-bretonne).

Je ne sais pas trop d'où vient la croyance de ta grand-mère, ceci dit, je n'avais jamais entendu ça avant de la part de brittophones…

Lorsqu'on ne s'attache qu'à renverser les rapports de forces, comme c'est en général le cas par chez nous, personne n'en sort grandit et finalement les puissants reprennent toujours la main.

Tant qu'une aristocratie remplit plus ou moins son rôle, il est concevable de tolérer ses vices (je ne dis pas que c'est idéal, mais comme on dit, « avec les révolutions, on sait toujours ce qu'on perd, jamais ce qu'on gagne »). Par exemple, la féodalité jusqu'à la Révolution française, la bourgeoisie paternaliste jusqu'à la fin de la seconde guerre mondiale, etc. Quand cette aristocratie est complètement en déphasage avec la réalité, c'est le moment de procéder à une petite coupe claire, qui, en général, finit par asseoir une nouvelle aristocratie en place. Immanquablement, cette dernière finit toujours par pourrir à son tour, ce qui ramène le cycle à son point de départ. Ce qui est important, c'est que de temps en temps « les puissants » changent de visage et que leur efficience soit positive.

Il me parait évident que la situation actuelle fleure bon la période pré-révolutionnaire. Qui est partant pour un petit coup de sécateur ?

kdécole de kosmos

HS : je viens d'avoir une fulgurance rare en me rendant compte de pourquoi ce nom me disait quelque chose : c'est l'entreprise dont les bureaux sont au premier étage de mon bâtiment…

J'ai toujours eu beaucoup de mal avec certaines sciences humaines, qui se drapent de la légitimité de la méthode scientifique sans jamais l'appliquer. Ce n'est pas le cas de toutes les sciences humaines, il y a fort heureusement des gens sérieux, mais j'ai quand même la forte impression que les fameuses (fumeuses ?) sciences de l'éducation tombent en plein dans ce travers. J'ai survolé quelques articles de cette chercheuse, et si certains articles commencent par avoir l'air d'être basés sur des faits observables, avec un joli graphique en première page, le reste se mue rapidement en quelque chose qui tient plus selon moi de l'article d'opinion que du document scientifique. Où sont les hypothèses testables ? Où sont les théorèmes ? Où sont les expériences reproductibles ? Le cœur de la justification repose sur des citations d'autres articles du même acabit (argument d'autorité) ou des preuves par l'anecdote. Les rares expériences sont testées sur des échantillons ridicules. Personnellement je trouve que ça décridibilise des messages qui mériteraient malgré tout d'être entendus…

Au sujet du « faux », ne penses-tu pas que les développeurs OCaml peuvent utiliser le type polymorphe 'a option pour représenter cette notion ?

En fait, cette interprétation du faux correspond exactement à une transformation logique connue sous le nom de Friedman's trick. Du côté langage de programmation, cela correspond à ajouter une exception dynamique, ce qu'OCaml a déjà en style direct (i.e. sans passer par une traduction).