Toi, tu connais pas les gens qui passent leur temps à essayer d'intégrer les effets au lambda-calcul à coups de types ésotériques... (Et qui en profitent pour réaliser l'axiome du choix dépendant avec.)
Captatio benevolentae : je n'ai rien d'un khmer vert et les partis écolos me paraissent à côté de la plaque, occupés qu'ils sont à attirer leur électorat essentiellement constitué de ces horripilants bourgeois qui s'ignorent, éthiques et écolo-responsables.
Certes. Mais qu'on me permette d'élever une timide remarque à l'encontre des imprimantes 3D.
Cette mode des imprimantes 3D m'insupporte au plus haut point. Alors que justement la force de l'ère de l'information réside dans la dématérialisation des activités humaines, nous voilà reparti dans un délire méta-consumériste. Pourquoi une imprimante 3D ? Pourquoi vouloir refabriquer de ces merdes en plastique dont on arrive pas déjà à se débarrasser ? Pourquoi ce désir de « cocooning » qui voudrait que tous les amateurs éclairés auraient un de ces engins chez eux, générant ainsi une demande supplémentaire aux usines du tiers-monde pour les construire, et saturant l'espace ambiant de cochonneries, qui au fond, ne servent pas à grand chose.
L'imprimante 3D est le reflet d'un fantasme conciliant avant-gardisme et rétrograde. Rétrograde, car il croit que l'avenir de la société se joue dans la manufacture et le concret. Avant-gardiste, parce qu'il sous-tend l'idée que l'individu devrait être à même de contrôler sa propre chaîne de fabrication.
Le premier point s'oppose à la marche de l'histoire et aux contraintes écologiques qui sont en train de nous tomber doucettement sur la gueule. Le second trahit un individualisme galopant, et nie la possibilité de collectifs et de coopératives pour arriver au même résultat, en mieux, car mutualisant les ressources.
Tu ne voudrais pas publier les photos en CC-BY sur Wikimedia Commons ? Je suis sûr qu'il y a une palanquée de gens qui seraient intéressés par ce genre de clichés, et puis ça éviterait que ça se perde dans la nature quand tu ne les hébergeras plus...
c'est bien une fonction polymorphe, pourtant, je ne vois nulle trace de décision dynamique en fonction du type... On a beau appeler polymorphisme des choses qui n'ont rien à voir, on utilise quand même des adjectifs pour les différencier : ad-hoc vs. paramétrique, ici.
Allons bon, tout ce que tu cites touche plus ou moins à l'algorithmique, mais il y a aussi un pôle moins maths discrètes qui comprend plusieurs sous-domaines, dont entre autres :
L'étude concrète des langages de programmation : la plupart des langages fonctionnels sont des produits du monde académique. Haskell/Agda et OCaml/Coq sont deux traditions issues de la recherche sur le mode « plus il y a de types, plus on rit ».
L'étude abstraite des langages de programmation : ce qu'on a coutume d'appeler la sémantique. Modèles divers et variés, théorie des domaines, théorie des catégories à foison. Ce qu'on appelle ici « langage de programmation » a en général peu à voir avec la conception qu'on s'en fait habituellement.
La logique : pour des raisons historiques, les logiciens sont souvent considérés comme des informaticiens, la faute à Curry-Howard. Et la logique, c'est cool : Théorie des Types de Martin-Löf, logique linéaire de Girard, et autres lambda-calculs en pagaille.
Il s'agit d'un environnement qui remplace avantageusement le système d'exploitation prioritaire habituellement utilisé sur la majorité des ordinateurs.
Les élus n'ont pas encore l'air très à l'aise avec le vocabulaire du libre...
En ce qui concerne Coq et Agda, et sans doute Epigram, mais je ne connais pas assez, ces langages ne sont pas Turing-complets, donc en parler comme « langages de programmation », c'est discutable.
Par ailleurs, parce qu'il vaut toujours mieux préférer l'original à la copie, je pense que OCaml est supérieur à F#. (Et puis le tout objet, c'est hideux).
Sinon, dans les langages rigolos, il y a ATS.
Et dans les langages exotiques, il y a Unlambda, parce que call/cc, c'est bien.
Ceci est un témoignage VÉRIDIQUE d'un utilisateur convaincu de l'efficacité de MultiDeskOS®.
Avant, j'avais de nombreux problèmes dans ma vie. Les femmes me fuyaient, j'avais honte de mon corps, mon ordinateur ne m'aimait pas. Alors, quand j'ai vu cette publicité pour un ESSAI GRATUIT de MultiDeskOS® pendant 8 jours, j'étais un peu dubitatif.
Cependant, j'ai quand même fait la démarche.
J'ai été tout de suite SÉDUIT par l'efficacité impressionnante de MultiDeskOS®. Conçu dans les plus grands laboratoires du monde, sous la direction du très célèbre Pr. Jayce, c'est un produit INCOMPARABLE. Mon écran a au moins gagné 4 POUCES en une semaine !
Aujourd'hui, ma vie a changé du tout au tout. Je peux enfin sortir dans la rue avec FIERTÉ !
Vous aussi vous pouvez profiter de cette OFFRE EXCEPTIONNELLE en envoyant un courriel à l'adresse enl4rgeUrOS@MultiDeskOS.org.
Ce que tu veux faire ressemble pas mal à des monades, qui est la méthode habituelle de Haskell pour traiter les exceptions. J'avais vu passer du code python utilisant une telle structure un jour, mais je ne sais plus où.
C'est vrai, mais je n'avais alors pas la chance de savoir que la capitale du Cap-Vert s'appelait Praia. Que celui qui n'a jamais séché me jette la première pierre !
Et c'est encore plus vicieux dans la mesure où le nom tchèque de Prague est Praha, et je penchais pour une faute de frappe...
Parce que si c'est un attachement au constructivisme, ta démonstration par l'absurde ne vaut pas tripette.
Si c'est un axiome mathématique, en particulier, si je suis ce que tu racontes, il y a une plâtrée de nombres réels qui n'existent pas. Tiens, celui-là, par exemple : http://fr.wikipedia.org/wiki/Om%C3%A9ga_de_Chaitin.
L'athée amateur de logique (constructiviste) que je suis voit ses poils se hérisser devant un tel raisonnement.
« Logique pure » déjà, ça veut rien dire. Dans quel système logique travailles-tu ? Tu veux prouver l'inexistence de Dieu dans ZF(C) ? OK, vas-y, définis-moi Dieu.
Pour ne pas être emporté dans un torrent de relativisme monothéisto-anthropocentrique, je propose de remplacer toutes les occurences de « Dieu » (qui est une dérive) par « gloubiboulga » quitte à avoir un terme neutre qui ne conflictera pas avec d'autres notions de la langue française.
Donc déjà, avant d'invoquer la logique, préciser dans quel système tu te places. Manifestement, ton appel au tiers-exclu dès la première étape te force à utiliser une logique assez puissante. Accessoirement, elle est non-constructive, donc tu risques de ne pas pouvoir extraire de témoin (de Jéhova ?).
Bon, ensuite, définis-moi gloubiboulga dans ton système axiomatique. Là on pourra commencer à montrer des trucs. Parce que c'est bien beau mais : « soit E l'ensemble des ensembles qui ne se contiennent pas eux-mêmes. » Contradiction (dans ZF) paf, boum, c'est plié.
Enfin, on est en train de parler d'un concept physique, pas mathématique, donc le recours à la logique me paraît un peu déplacé.
En définitive, pour apporter de l'eau au moulin, je crois que la question « Est-ce que Dieu existe ? » a à peu près autant d'intérêt que l'existence des schtroumpfs à poil ras et qu'au lieu de se tripoter sur des concepts flous qui n'ont AUCUNE validité mathématique, les gens feraient mieux de tenter de prouver la conjecture de Goldbach ou P != NP (un simple N != NL serait déjà beaucoup).
Au passage, je ne crois pas au gloubiboulga divin, mais je sais (par des arguments statistiques, hein, les OVNI c'est du pipeau) que la vie existe ailleurs que sur Terre.
[^] # Re: Hum ...
Posté par Perthmâd (site web personnel) . En réponse au journal Votre langage idéal ?. Évalué à 0.
Toi, tu connais pas les gens qui passent leur temps à essayer d'intégrer les effets au lambda-calcul à coups de types ésotériques... (Et qui en profitent pour réaliser l'axiome du choix dépendant avec.)
[^] # Charybde et Scylla
Posté par Perthmâd (site web personnel) . En réponse au journal You wouldn't download a car !?. Évalué à 9.
Captatio benevolentae : je n'ai rien d'un khmer vert et les partis écolos me paraissent à côté de la plaque, occupés qu'ils sont à attirer leur électorat essentiellement constitué de ces horripilants bourgeois qui s'ignorent, éthiques et écolo-responsables.
Certes. Mais qu'on me permette d'élever une timide remarque à l'encontre des imprimantes 3D.
Cette mode des imprimantes 3D m'insupporte au plus haut point. Alors que justement la force de l'ère de l'information réside dans la dématérialisation des activités humaines, nous voilà reparti dans un délire méta-consumériste. Pourquoi une imprimante 3D ? Pourquoi vouloir refabriquer de ces merdes en plastique dont on arrive pas déjà à se débarrasser ? Pourquoi ce désir de « cocooning » qui voudrait que tous les amateurs éclairés auraient un de ces engins chez eux, générant ainsi une demande supplémentaire aux usines du tiers-monde pour les construire, et saturant l'espace ambiant de cochonneries, qui au fond, ne servent pas à grand chose.
L'imprimante 3D est le reflet d'un fantasme conciliant avant-gardisme et rétrograde. Rétrograde, car il croit que l'avenir de la société se joue dans la manufacture et le concret. Avant-gardiste, parce qu'il sous-tend l'idée que l'individu devrait être à même de contrôler sa propre chaîne de fabrication.
Le premier point s'oppose à la marche de l'histoire et aux contraintes écologiques qui sont en train de nous tomber doucettement sur la gueule. Le second trahit un individualisme galopant, et nie la possibilité de collectifs et de coopératives pour arriver au même résultat, en mieux, car mutualisant les ressources.
# Back to the future
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Sortie de la version 0.1 de Rust. Évalué à 10.
Inférence de types, types algébriques avec polymorphisme, clôtures, garbage collection, message-passing...
Scoop : « le programmeur lambda vient de découvrir la programmation fonctionnelle ! »
# Les vrais théoriciens s'en foutent
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Le colonel Moutarde, sur la table (de hachage), avec un livre de maths. Évalué à -5.
Parce que O(n) et O(n²), c'est pareil, c'est polynomial...
Et puis quelle idée d'utiliser des tables de hachage, les arbres binaires de recherche, c'est quand même plus classe !
# CEDICT
Posté par Perthmâd (site web personnel) . En réponse au journal Apprendre à lire et taper en chinois avec des outils libres. Évalué à 3.
En dico libre, il y a CEDICT aussi.
# Publication
Posté par Perthmâd (site web personnel) . En réponse au journal photos libre d'Antarctique. Évalué à 9.
Tu ne voudrais pas publier les photos en CC-BY sur Wikimedia Commons ? Je suis sûr qu'il y a une palanquée de gens qui seraient intéressés par ce genre de clichés, et puis ça éviterait que ça se perde dans la nature quand tu ne les hébergeras plus...
# Vive la 3D !
Posté par Perthmâd (site web personnel) . En réponse au journal Cinéma : une histoire de tipiaks à rendre récursive. Évalué à 10.
Non, je ne suis pas d'accord, ce film est la révélation que tous attendaient pour célébrer la 3D.
Parce qu'on peut y voir de somptueuses plongées sur les vastes décolletés dévoilant les éminences mammaires de Pénélope Cruz.
Et ça, ça n'a pas de prix.
[^] # Re: Ça rejoint les typeclass de haskell, template du C++, Go
Posté par Perthmâd (site web personnel) . En réponse au journal Le problème de la POO pratiquée par des étudiants. Évalué à 5.
Ah bon ? Pourtant :
⊢ λx.x : ∀α.α → α
c'est bien une fonction polymorphe, pourtant, je ne vois nulle trace de décision dynamique en fonction du type... On a beau appeler polymorphisme des choses qui n'ont rien à voir, on utilise quand même des adjectifs pour les différencier : ad-hoc vs. paramétrique, ici.
# Paronomase
Posté par Perthmâd (site web personnel) . En réponse au journal La déclaration des droits numériques du lecteur . Évalué à 3.
Dans librarian il y a libre !
[^] # Re: Les jeunes fuient les filières scientifiques ?
Posté par Perthmâd (site web personnel) . En réponse au journal Populariser la science informatique. Évalué à 9.
Allons bon, tout ce que tu cites touche plus ou moins à l'algorithmique, mais il y a aussi un pôle moins maths discrètes qui comprend plusieurs sous-domaines, dont entre autres :
L'étude concrète des langages de programmation : la plupart des langages fonctionnels sont des produits du monde académique. Haskell/Agda et OCaml/Coq sont deux traditions issues de la recherche sur le mode « plus il y a de types, plus on rit ».
L'étude abstraite des langages de programmation : ce qu'on a coutume d'appeler la sémantique. Modèles divers et variés, théorie des domaines, théorie des catégories à foison. Ce qu'on appelle ici « langage de programmation » a en général peu à voir avec la conception qu'on s'en fait habituellement.
La logique : pour des raisons historiques, les logiciens sont souvent considérés comme des informaticiens, la faute à Curry-Howard. Et la logique, c'est cool : Théorie des Types de Martin-Löf, logique linéaire de Girard, et autres lambda-calculs en pagaille.
# Logiciel prioritaire
Posté par Perthmâd (site web personnel) . En réponse au journal Les logiciels libre à l'école.. Évalué à 9.
Les élus n'ont pas encore l'air très à l'aise avec le vocabulaire du libre...
[^] # Re: Synchrones
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Apprendre un langage de programmation par an. Évalué à 1.
http://linuxfr.org/2010/12/20/27690.html#1193039
[^] # Re: Différents langages
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Apprendre un langage de programmation par an. Évalué à 1.
Par ailleurs, parce qu'il vaut toujours mieux préférer l'original à la copie, je pense que OCaml est supérieur à F#. (Et puis le tout objet, c'est hideux).
Sinon, dans les langages rigolos, il y a ATS.
Et dans les langages exotiques, il y a Unlambda, parce que call/cc, c'est bien.
[^] # Re: Attention !
Posté par Perthmâd (site web personnel) . En réponse au journal Le Web sauvera Internet. Évalué à 10.
# Merci MultiDeskOS® !
Posté par Perthmâd (site web personnel) . En réponse au journal MultiDeskOS version 7. Évalué à 8.
Avant, j'avais de nombreux problèmes dans ma vie. Les femmes me fuyaient, j'avais honte de mon corps, mon ordinateur ne m'aimait pas. Alors, quand j'ai vu cette publicité pour un ESSAI GRATUIT de MultiDeskOS® pendant 8 jours, j'étais un peu dubitatif.
Cependant, j'ai quand même fait la démarche.
J'ai été tout de suite SÉDUIT par l'efficacité impressionnante de MultiDeskOS®. Conçu dans les plus grands laboratoires du monde, sous la direction du très célèbre Pr. Jayce, c'est un produit INCOMPARABLE. Mon écran a au moins gagné 4 POUCES en une semaine !
Aujourd'hui, ma vie a changé du tout au tout. Je peux enfin sortir dans la rue avec FIERTÉ !
Vous aussi vous pouvez profiter de cette OFFRE EXCEPTIONNELLE en envoyant un courriel à l'adresse enl4rgeUrOS@MultiDeskOS.org.
Merci MultiDeskOS® !
[^] # Re: mediawiki et git
Posté par Perthmâd (site web personnel) . En réponse à la dépêche Sortie de MediaWiki 1.16.0 et 1.15.5. Évalué à 1.
M'enfin, s'il y a des gens motivés...
# Monades
Posté par Perthmâd (site web personnel) . En réponse au message systeme de message ??. Évalué à 2.
# Écrire du code Perl maintenable.
Posté par Perthmâd (site web personnel) . En réponse au journal Écrire du code Perl maintenable.. Évalué à 10.
[^] # Re: Et il est déjà vicelard
Posté par Perthmâd (site web personnel) . En réponse au journal OpenStreetGame : un jeu pour vous faire réviser votre géographie. Évalué à 2.
Et c'est encore plus vicieux dans la mesure où le nom tchèque de Prague est Praha, et je penchais pour une faute de frappe...
# Et il est déjà vicelard
Posté par Perthmâd (site web personnel) . En réponse au journal OpenStreetGame : un jeu pour vous faire réviser votre géographie. Évalué à 5.
Forcément, je clique sur la république Tchèque, pensant à un bug, et paf, plus de 5000 km d'erreur...
[^] # Re: La licorne invisible.
Posté par Perthmâd (site web personnel) . En réponse au journal Athéisme, agnostisme: manifeste agnostique. Évalué à 2.
[^] # Re: [X] agnostique radical
Posté par Perthmâd (site web personnel) . En réponse au journal Athéisme, agnostisme: manifeste agnostique. Évalué à 3.
rm -rf /Pour accéder au nirvâna, débarrassez-vous de la matérialité qui vous encombre !
[^] # Re: Le rasoir d'Ockham retourné
Posté par Perthmâd (site web personnel) . En réponse au journal Athéisme, agnostisme: manifeste agnostique. Évalué à 2.
http://estatis.coders.fm/falso/
[^] # Re: Vraie question
Posté par Perthmâd (site web personnel) . En réponse au journal Athéisme, agnostisme: manifeste agnostique. Évalué à 2.
Parce que si c'est un attachement au constructivisme, ta démonstration par l'absurde ne vaut pas tripette.
Si c'est un axiome mathématique, en particulier, si je suis ce que tu racontes, il y a une plâtrée de nombres réels qui n'existent pas. Tiens, celui-là, par exemple : http://fr.wikipedia.org/wiki/Om%C3%A9ga_de_Chaitin.
[^] # Re: Vraie question
Posté par Perthmâd (site web personnel) . En réponse au journal Athéisme, agnostisme: manifeste agnostique. Évalué à 3.
1) Soit dieu existe, soit il n'existe pas.
L'athée amateur de logique (constructiviste) que je suis voit ses poils se hérisser devant un tel raisonnement.
« Logique pure » déjà, ça veut rien dire. Dans quel système logique travailles-tu ? Tu veux prouver l'inexistence de Dieu dans ZF(C) ? OK, vas-y, définis-moi Dieu.
Pour ne pas être emporté dans un torrent de relativisme monothéisto-anthropocentrique, je propose de remplacer toutes les occurences de « Dieu » (qui est une dérive) par « gloubiboulga » quitte à avoir un terme neutre qui ne conflictera pas avec d'autres notions de la langue française.
Donc déjà, avant d'invoquer la logique, préciser dans quel système tu te places. Manifestement, ton appel au tiers-exclu dès la première étape te force à utiliser une logique assez puissante. Accessoirement, elle est non-constructive, donc tu risques de ne pas pouvoir extraire de témoin (de Jéhova ?).
Bon, ensuite, définis-moi gloubiboulga dans ton système axiomatique. Là on pourra commencer à montrer des trucs. Parce que c'est bien beau mais : « soit E l'ensemble des ensembles qui ne se contiennent pas eux-mêmes. » Contradiction (dans ZF) paf, boum, c'est plié.
Enfin, on est en train de parler d'un concept physique, pas mathématique, donc le recours à la logique me paraît un peu déplacé.
En définitive, pour apporter de l'eau au moulin, je crois que la question « Est-ce que Dieu existe ? » a à peu près autant d'intérêt que l'existence des schtroumpfs à poil ras et qu'au lieu de se tripoter sur des concepts flous qui n'ont AUCUNE validité mathématique, les gens feraient mieux de tenter de prouver la conjecture de Goldbach ou P != NP (un simple N != NL serait déjà beaucoup).
Au passage, je ne crois pas au gloubiboulga divin, mais je sais (par des arguments statistiques, hein, les OVNI c'est du pipeau) que la vie existe ailleurs que sur Terre.