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
C'est connu... depuis quand ? J'ai l'impression que c'est une erreur de conception qui leur a échappé, et dont ils ne se sont rendu compte qu'ensuite (par exemple dans l'intervalle de temps entre la spécification du langage Oak et l'écriture de la spécification de Java).
le lambda calcul n'est pas oblige d’être cantonne a une évaluation statique. Je me trompe ?
Non, tu ne te trompes pas; d'ailleurs c'est ce que fait l'article sur la "traduction de Java vers un lambda-calcul typé" dont tu parlais, il rajoute des tests dynamiques pour compenser la sémantique cassée du système de typage statique (et ses difficultés à modéliser la récursion ouverte en conservant le sous-typage, qu'on sait maintenant résoudre).
Cependant, une idée de base du typage est de refléter la sémantique du langage. Une relation de sous-typage était que si S est sous-type de T, alors toute valeur de type S peut être considérée comme une valeur de type T. Dans la théorie, c'est l'idée sémantique derrière le sous-typage, donc très important. Dans la pratique, c'est le principe de substitution de Liskov (LSP), énoncé en 1987 (donc avant la conception du langage Java) et donc connu, on l'espère, des concepteurs de Java. Or, la relation de sous-typage qui est présente dans Java viole ce principe de substitution, puisque S[] peut être sous-type de T[] sans qu'un tableau de type S[] puisse être utilisé de la même façon qu'un tableau de type T. C'est bête, et ça ressemble assez à une erreur de conception, non ?
Si ce test qui tue les performances et qui contrarie tout le monde est là, c'est sans doute parce que les gens n'ont pas vu le problème au départ et ont cru que c'était correct, parce qu'ils ne connaissaient pas le modèle théorique derrière. C'est une hypothèse (que j'ai déjà formulée dans mon post qui s'est fait descendre en flamme) crédible puisque le problème n'est pas mentionné dans les premières spécifications du langage.
Le rasoir d'Ockham me suggère que cette explication est plus plausible que l'hypothèse selon laquelle James Gosling, qui est en fait un gro pgm des systèmes de types qui cache bien son jeu, s'est amusé à cacher les failles sémantiques dans son système pendant plusieurs années (jusqu'à qu'un chercheur indépendant les pointes du doigt), à définir une relation de typage non-standard violant le LSP, pour le plaisir de rajouter un test de typage dynamique à chaque accès dans un tableau et de donner l'opportunité aux chercheurs en typage de se torturer pour trouver une manière raisonnable d'étendre le langage de façon sensée par la suite (... ce qu'ils n'ont pas tout à fait réussi, si on en croit les avis sur les génériques Java).
Encore une fois, je serais très intéressé par toute source confirmant que les concepteurs de Java ont pensé au modèle théorique de leur système de typage pendant la conception du langage (c'est à dire entre grosso-modo 1991, premières mentions de Oak, et 1994, arrivée de Guy Steele à Sun pour bosser sur la spec. du langage déjà conçu).
[^] # Re: Encore le type Null...
Posté par gasche . En réponse à la dépêche Dart va‐t‐il remplacer JavaScript comme langage dans les navigateurs ?. Évalué à 3.
C'est connu... depuis quand ? J'ai l'impression que c'est une erreur de conception qui leur a échappé, et dont ils ne se sont rendu compte qu'ensuite (par exemple dans l'intervalle de temps entre la spécification du langage Oak et l'écriture de la spécification de Java).
Non, tu ne te trompes pas; d'ailleurs c'est ce que fait l'article sur la "traduction de Java vers un lambda-calcul typé" dont tu parlais, il rajoute des tests dynamiques pour compenser la sémantique cassée du système de typage statique (et ses difficultés à modéliser la récursion ouverte en conservant le sous-typage, qu'on sait maintenant résoudre).
Cependant, une idée de base du typage est de refléter la sémantique du langage. Une relation de sous-typage était que si S est sous-type de T, alors toute valeur de type S peut être considérée comme une valeur de type T. Dans la théorie, c'est l'idée sémantique derrière le sous-typage, donc très important. Dans la pratique, c'est le principe de substitution de Liskov (LSP), énoncé en 1987 (donc avant la conception du langage Java) et donc connu, on l'espère, des concepteurs de Java. Or, la relation de sous-typage qui est présente dans Java viole ce principe de substitution, puisque S[] peut être sous-type de T[] sans qu'un tableau de type S[] puisse être utilisé de la même façon qu'un tableau de type T. C'est bête, et ça ressemble assez à une erreur de conception, non ?
Si ce test qui tue les performances et qui contrarie tout le monde est là, c'est sans doute parce que les gens n'ont pas vu le problème au départ et ont cru que c'était correct, parce qu'ils ne connaissaient pas le modèle théorique derrière. C'est une hypothèse (que j'ai déjà formulée dans mon post qui s'est fait descendre en flamme) crédible puisque le problème n'est pas mentionné dans les premières spécifications du langage.
Le rasoir d'Ockham me suggère que cette explication est plus plausible que l'hypothèse selon laquelle James Gosling, qui est en fait un gro pgm des systèmes de types qui cache bien son jeu, s'est amusé à cacher les failles sémantiques dans son système pendant plusieurs années (jusqu'à qu'un chercheur indépendant les pointes du doigt), à définir une relation de typage non-standard violant le LSP, pour le plaisir de rajouter un test de typage dynamique à chaque accès dans un tableau et de donner l'opportunité aux chercheurs en typage de se torturer pour trouver une manière raisonnable d'étendre le langage de façon sensée par la suite (... ce qu'ils n'ont pas tout à fait réussi, si on en croit les avis sur les génériques Java).
Encore une fois, je serais très intéressé par toute source confirmant que les concepteurs de Java ont pensé au modèle théorique de leur système de typage pendant la conception du langage (c'est à dire entre grosso-modo 1991, premières mentions de Oak, et 1994, arrivée de Guy Steele à Sun pour bosser sur la spec. du langage déjà conçu).