lasher a écrit 2738 commentaires

Ben visiblement il y a des confs/workshops concernant le sujet: Algebraic methodology and software technology.

De plus je sais que presque tous les programmes peuvent être exprimés sous forme algébrique (l'algèbre étant définie en fonction du langage). Par exemple XQuery et les autres langages FLWR ont une algèbre bien définie pour exprimer des requêtes (là encore, ce sont des vestiges de mes cours datant d'il y a quelques années — en l'occurrence, de données semi-structurées & XML).

Ce fichier PDF montre comment les AST sont utilisés pour l'analyse de programmes, du point de vue de l'analyse du flot de données (dataflow analysis). Ce genre de trucs remonte à loin, mais en gros si je peux toucher à un graphe, je peux du coup toucher à la théorie des groupes, et donc je peux d
définir des relations algébriques entre diverses parties de mon graphe/AST. De façon générale, n'importe quelle relation algébrique peut être représentée sous forme d'arbre. Donc forcément, un AST peut être « traduit » en relation algébrique.

Et pourquoi pas en référence « Journal TV de telle chaîne, tel jour, telle heure » ? Après tout, c'est une référence valide, non ?

Oups, j'ai oublié de donner le lien (trouvé sur Wikipedia) : http://www.infoq.com/presentations/gosling-jvm-lang-summit-keynote

Alors, pour info, je suis en train de regarder une vidéo où Gosling présente les origines de Java. Avant de faire des études, il a programmé et écrit (ou maintenu) plusieurs langages. Entre autres il a maintenu une implémentation de Simula.

Sa thèse décrit comment considérer l'expression d'un programme sous forme algébrique (repris d'un de ses slides : « Code-as-algebra is awesome! »,: il a bossé sur les Arbres syntaxiques abstraits (AST)) [1]

Gosling décrit Java comme étant une tentative d'obtenir un langage avec un « "scripting" feel », sans perdre trop en termes de performance. [2] Il parle ensuite d'introduire le loup dans la bergerie, en gardant une syntaxe à-la-C, mais en introduisant les bonnes idées d'autres langages (Lisp,Smalltalk,Simula,etc.). [3]

Il dit que Java (et la JVM) est quasiment un copier-coller de Simula. [4]

À propos des types : les types primitifs ont été uniquement introduits à cause des performances (pouvoir faire a = b + c en une instruction de la JVM). Malheureusement il ne parle pas des types mis à part ça.

[1] 07:30
[2] 26:30
[3] 27:00
[4] 42:00
[5] 46:00

Manque de bol, les hiéroglyphes étaient bien phonétiques. Tu confonds avec les idéogrammes.

Pour commencer, je tiens à préciser que je me suis absolument pas un expert en lambda calcul ni en théorie des types/sûreté des types.

Le terme "type-safe" peut désigner plusieurs choses.

D’après mon prof de l’époque (ça commence à faire quelques années maintenant, donc si j'ai commis une imprécision, c'est ma faute, pas la sienne),

La sûreté des types garantit qu'un programme ne peut jamais être dans un état indéterminé (eg un état "bloqué" ou rendre une valeur incorrecte que le type ne devrait pas permettre) à l’exécution.

Donc, que celle-ci soit garantie à l’exécution ou à la compilation importe peu : un langage est type-safe s'il garantit cette propriété.

Un langage comme Python est "type-safe" dans le sens où avant chaque opération, on effectue un test dynamique pour vérifier que l'opérande a bien la forme attendue. Ça évite les erreurs de langages moins méfiants comme C qui segfault rapidement si les types ne correspondent pas (ce que le système de typage, en plus, ne sait pas vérifier, en raison entre autres de l'habitude de transporter tout ce qui doit être générique dans un void *).

Tout à fait. En ce qui concerne Java, il existe une sûreté des types à "deux niveaux" :

1. Statique : tant que je reste dans le cadre des types non primitifs (instanciations de classes, donc tout ce qui peut se passer par référence), alors le transtypage n'est autorisé que s'il se passe d'une instance de classe particulière vers une instance plus générique, autorisé par une relation d’héritage (Object étant un ancêtre commun à toutes les classes) [1]. Oui, cela signifie bien que si j’écris quelque chose du genre :

public class Test {

    static void toto(Object o) {
        String s = (String) o;
        System.out.println(s);
    }
    
    public static void main(String[] args) {
        Integer i = new Integer(1);
        String s = "toto";
        toto(s);
        toto(i);
    }
}

Le compilateur me laissera faire.

1. Dynamique : le fait qu'on puisse transtyper d'un type "générique" vers un type plus précis mais appartenant à une autre sous-branche dans l'arbre d’héritage que celui d'origine fait que le runtime doit pouvoir attraper ce genre d'erreurs de type. Oui, cela a un coût. En même temps, en OCaml, le coût est dans le fait que pour pouvoir utiliser une fonction, il faut que je gère explicitement l’intégralité des types gérés par cette fonction. Faire le produit cartésien des types, c'est pas rigolo tous les jours si je suis cense gerer beaucoup de types dans ma fonction (c'est d'ailleurs pour ça que CDuce a été créé -- enfin, en partie : cf. les papiers dispos sur le site de CDuce à propos du sous-typage sémantique).

Bien que le système de typage statique de Java soit incorrect, le langage est dynamiquement type-safe grâce au test dynamique qui est effectué à chaque écriture dans un tableau.

Exactement. Tu dis que le typage statique est incorrect. Je ne suis pas d'accord. Il est conçu ainsi, ça ne le rend pas incorrect. A moins que lorsque tu parles "d'incorrect", tu ne veuille dire "laisse passer des comportements incorrects", auquel cas, oui, pourquoi pas, mais c'est connu, et "rattrapé" par le comportement du runtime.

Bien sûr, il est difficile pour moi de prouver que James Gosling ne connaissait pas telle ou telle chose, puisque le fait qu'il n'en parle pas ne nous permet pas de savoir s'il le connaissait ou pas. Puisque tu sembles persuadé que Java a été conçu dès le départ avec un modèle théorique "rempli de lambda-calcul", peut-être as-tu eu accès à des documents sur l'histoire de Java qui en parlent ?

Je n'ai jamais parlé de type-safety totalement statique. Je réagissais principalement au fait qu'Ontologia semblait considérer Java et Dart comme des langages/plate-formes qui n'avait pris aucune considération théorique en compte, ce qui est faux. Bien qu'il soit bien entendu surtout considéré pour une évaluation statique (surtout auprès des gens qui font dans la prog fonctionnelle j'ai l'impression), le lambda calcul n'est pas oblige d’être cantonne a une évaluation statique. Je me trompe ?

Concernant la thèse de Gosling : j'ai simplement repris l'info depuis Wikipedia. Maintenant, la manipulation algebrique de contraintes, c'est peut-être (sans doute) pas lie a la sûreté des types, mais c'est clairement applicable a la compilation !

[1] Evidemment, passer par la réflexivité et l'introspection permet de casser la sûreté des types en Java, mais c'est consciemment que le programmeur utilise ces outils.

... et plus de 10x plus cher.

« Il n'y a pas de mauvaise publicité. » :-)

Tiré de l'abstract du papier que tu pointes, première phrase :

Java offers the real possibility that most programs can be written in a type-safe language

Non, je ne pense pas que Java ait été conçu avec un modèle théorique en tête. Je ne sais pas à quoi tu fais référence en disant qu'il est "rempli de lambda-calcul".

Ben Java est type-safe, et ça passe par du lambda calcul si tu veux le faire correctement. Tu peux avoir toutes les impressions que tu veux, ça reste vrai. Dire que Java n'a pas de modèle théorique en tête, c'est tout simplement ne pas être au courant de comment Java a été conçu. Java est un des premiers langages « grand public » qui a tenté d'intégrer le parallélisme et la concurrence dès le départ. Du point de vue théorique, ça passe par un modèle de concurrence ainsi qu'un modèle mémoire (il est démontrable que le premier modèle mémoire est cassé, et le deuxième modèle, introduit en 2005-2006, bien que bien meilleur, reste contesté, avec des papiers qui démontrent que certaines propriétés demandées par le modèles sont invérifiables).

L'impression que j'ai est plutôt que les ingénieurs qui ont conçu Java n'étaient pas forcément très au courant de la recherche dans le domaine, mais ont surtout retiré les fonctionnalités les plus complexes de C++ pour faire un langage simplifié.

L'un n'empêche pas l'autre. Cependant la JVM est parfaitement spécifiée, et la traduction de code Java vers le bytecode itou.

Ensuite, dans les versions récentes de Java, l'importance pratique du langage a motivé des spécialistes de la théorie des types à se pencher sur la question des génériques notamment.

Définis « récentes ». La théorie des types, etc., appliquée aux types / classes de Java ça fait un moment (je dirais au moins 10 ans) que c'est intégré à l'implémentation de référence. Exemple, le bouquin de B. Pierce, Types and Programming Languages, est sorti en 2002, et propose déjà un « mini-java » typesafe en guise d'exercice…

Une simple recherche google avec les mots-clef « lambda calculus type safety java » renvoient vers le bouquin de Pierce, puis vers des rapports techniques sur la possibilité de compiler Java vers du lambda calcul typé (rapport datant de 1998).

C'est là que sont apparus des modèles formels de sous-ensembles de Java, basés sur la recherche faite indépendamment sur la théorie des langages objets. Mais ça ne veut pas dire que Java dans son ensemble ait été conçu par des gens connaissant la théorie.

Les mecs qui ont conçu Java n'étaient certes pas des dieux de la compilation et de la théorie des langages, mais une rapide recherche sur J.Gosling (l'un des papas de Java avec Bill Joy) montre que sa thèse de 1983 s'intitule The Algebraic Manipulation of Constraints. Bref, pas un p'tit joueur non plus.

Sauf que ça fait un moment que les bons compilos C/C++ font de l'optimisation inter-procédurale, et peuvent donc générer des « pseudo » fichiers objets qui contiennent des infos pertinentes pour faire de l'optim au moment de l'édition des liens. Alors certes, parfois ça mène au compilateur qui t'explique que y'a beaucoup trop de choses à analyser, et du coup il s'arrête ou bien il continue en faisant de la compilation uniquement par module. Mais l'IPC est censée être utilisée uniquement pour ce qui en vaut la peine (noyau de calcul très utilisé à plusieurs endroits d'un code, bibliothèque de code optimisée aux petits oignons, etc.).

De plus en ce qui concerne les templates, à cause de la façon dont ils fonctionnent en C++, s'il s'agit d'un template de classe, alors de toute manière il est forcément inclus en entier dans le fichier qui l'utilise et le compilateur a donc toutes les informations nécessaires pour optimiser à fond.

Hum. Java est rempli de lambda calcul pour la sûreté des types au niveau des classes. Google compte parmi ses employés des mecs très, très forts en compilation. Tu as pris pile-poil le mauvais exemple, vu que Dart est très clairement une resucée de Java. :-)

OCaML et Haskell ont une grosse infra derrière, avec une base mathématique théorique de très haut niveau (Théorie du lambda calcul de type), c'est pas à la portée du premier implémenteur de compilateur venu.

Euh... Si. J'exagère un peu hein, mais un mec qui fait un vrai compilo pour compiler du code vraiment efficace se doit de piger ce qu'est le lambda calcul. Bref.

Maintenant son analyse sera t'elle biaisée par la compétition entre les codec?

sera-t-elle

Signé : le nazi de l'orthographe.

Je crois qu'il insinue que les devs C++ ont un vi. Grand ou petit, il ne dit rien dessus.

Mmmh, par définition, une bibliothèque graphique doit maintenir un état de ce qui est affiché. Comment tu fais pour ne redessiner qu'une partie de l'écran si tu n'as que du single assignment ? Plus exactement, je sais que c'est possible, mais je me demande quelles seraient les performances dans ce cas. Faire un serveur web en Erlang est parfaitement sensé (presque tout est « write once, read many »). Pour une interface graphique avec un paradigme événementiel, je suis moins certain.

Oui, comme par exemple XmlHttpRequest. Quelle plaie, fouyaya... (et là, Grunt arrive et approuve au premier degré mon second. :P)

Puisqu'on en est à corriger les fautes...
On dit « Mais ne va-t-on pas ». On rajoute le « t » (et ses potes les traits d'union) pour des raisons phonétique de liaison. Alors que je n'ai toujours pas compris quelle était la logique derrière l'apostrophe.

C’était quand la dernière fois ? Je demande, parce que j'ai vu des journaux particulièrement nauséabonds être écrits et pas censurés, avec un contenu somme toute bien pire que ce que j'ai pu lire comme commentaires censurés dernièrement. Ils ont généré des dizaines, voire centaines de commentaires (certains aussi nauséabonds que le journal initial), mais au final la "raison" l'a emporté -- sans qu'il y ait besoin de censurer quoi que ce soit. Les trolls sont repartis chez eux, et tout s'est bien fini.

LinuxFR est l'un des rares sites que je visite régulièrement parce que justement les gens, même ceux avec des opinions qui me font gerber, restent pour 95% d'entre eux avec un discours avec lequel il est possible d'argumenter (pour ou contre, là n'est pas la question). Quelque part, LinuxFR c'est mon nouveau fcold: un nid à trolls, certes, mais avec des trolls qui pour la plupart ont une certaine éducation (et parfois même une certaine culture ;-)).

Ça, c'est totalement dépendant de l’état ou de la ville ou tu habites. La où je vis, c'est effectivement des baux d'un an que nous devons signer. Les propriétaires sont en règle générale OK pour la sous-location (pas tout le temps cela dit) si jamais on désire bouger plus tôt. Dans la ville de New-York par exemple, quitter son appart avant la fin du bail est parfaitement possible, sans pénalité -- vu comment l'immobilier grimpe de toute manière, le nouveau bail aura un loyer plus élevée, et il y aura toujours une demande.

Donc ce que tu dis, c'est qu'il faudrait que l'Etat s'endette utilement, et commande la construction de plein de maisons/immeubles/bureaux/etc. hors Région Parisienne, afin d'encourager les entreprises à s'installer ailleurs. J'ai bon ?

En fait, j'aimerais bien que l'Etat le fasse pour de bon (je pense qu'il peut y gagner au final quand il se mettra à vendre/louer les logements a qui voudra les prendre, et à toucher des sous sur les impôts locaux, etc.), mais mon problème c'est que ça ne suffira sans doute malheureusement pas, car il faut aussi inciter les commerces (et pas que les commerces "faciles" à bouger, comme c'est le cas avec l'informatique : je parle aussi de commerces pour la vie de tous les jours) à se créer là ou les logements existent. :-/

Et puis il faudrait penser l'infrastructure pour les transports en commun dès le début aussi (même si ces derniers sont construits plus tard), etc. etc.

Je me demande combien ça coûterait, tiens ...

Bon, j'ai lu le message de cooker avant qu'il ne soit censuré, et même si je trouvais le post nauséabond, je ne vois pas en quoi il était normal de le censurer (pas d'incitation a la haine raciale ou autre joyeusetés du genre). Je trouve que le coupe-coupe a été appliqué un peu vite dans ce cas...

Quand la loi est tellement débile au point de ne plus refléter la réalité du marché, oui ça passe du côté de l'illégalité. Pas un paquet de gens, juste que les gens qui refuseront n'auront pas de logement. Quand la loi n'est plus proche de la réalité, c'est comme ça que ça arrive.

Ah oui, comme pour HADOPI et le téléchargement quoi ...

Pom pom pom...

Oui. La confession de H.Reiser.

C'était pas le PowerPC qui avait une instruction pour faire des loads (resp. stores) multiples depuis (vers) une adresse mémoire?

Je ne me souviens plus très bien, mais quelque chose du genre

ldmul 1,31,uneAdresse

qui chargerait 31 mots de 32 bits vers les registres r1 à r31?