Le terme "type-safe" peut désigner plusieurs choses. 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 *).
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.
Comme je l'ai déjà dit, je doute que les concepteurs de Java se soient posé la question de la sûreté du typage statique, sinon ils auraient repéré ce problème et, à défaut de le corriger (ce qui n'est pas évident), l'auraient mentionné clairement dans les premières spécifications du langage. Ce n'est pourtant pas le cas dans la "Oak language specification" (version 0.2, la seule que j'ai trouvé facilement sur Internet). Il faut attendre 96, la première "Java language specification", écrite en grande par Guy Steele qui n'a pas participé au design de Java. Cette spécification discute le problème de l'assignement non statiquement sûr dans un tableau en détail, mais elle dit en même temps:
The following conversions are called the widening reference conversions:
[...]
From any array type SC[] to any array type TC[], provided that SC and TC
are reference types and there is a widening conversion from SC to TC .
[...]
Such conversions never require a special action at run time and therefore never
throw an exception at run time. They consist simply in regarding a reference as
having some other type in a manner that can be proved correct at compile time.
La spécification dit que la covariance des tableaux est "prouvée correcte statiquement". Au mieux c'est une formation ambiguë (ils veulent dire "on sait que c'est faux mais, sachant qu'il y a le test dynamique, plus tard, c'est quand même pas trop grave") qu'une personne attentive à l'aspect théorique de la chose aurait évitée, au pire c'est une erreur.
Après on pourrait dire qu'ils ont effectivement fait une étude théorique et juste laissé passer une erreur dans une preuve. Ça arrive. Mais ça ne colle pas avec la réalité historique qui est que les chercheurs en langages de programmation connaissaient à l'époque déjà très bien le problème. La question du sous-typage est apparue au milieu des années 80, est devenu un sujet chaud et a été très étudiée jusqu'au début des années 90. Le langage Quest de Cardelli contient des types paramétriques (donc sensiblement plus avancé que Java à l'époque), du sous-typage, et des variables modifiables; il discute clairement des problèmes liés à la mutabilité et précise explicitement que les tableaux sont invariants. La spécification de Quest a été publiée en 1994, mais la recherche sur laquelle elle se base date des années 80 (tous les articles cités ont été publiés avant 1990). Si les concepteurs de Java étaient au courant, comme tu le prétends, de la recherche théorique dans le domaine qui les concerne directement, ils auraient certainement été au courant et il me semble fort curieux qu'ils n'en aient donné aucun signe.
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 serais très intéressé par ces sources qui, comme je l'ai dit, iraient à l'encontre de mon intuition propre. Le fait qu'il ait écrit une thèse dans un domaine qui à priori n'a rien à voir avec les langages de programmation1 ne signifie pas grand chose (et par ailleurs si tu as pu mettre la main sur le manuscript de la thèse, je suis intéressé, parce que moi je n'ai rien trouvé).
1: même s'il faut faire attention : son directeur de thèse faisait de l'IA et l'IA, au moins à ses débuts, était très liée à la conception de langages de programmation. Les gens qui faisaient de l'IA s'intéressaient cependant beaucoup plus aux aspects dynamiques des langages (programmation logique, backtracking, systèmes multi-agents, modèles d'acteurs...) qu'aux aspect statique (lambda-calcul typé). Lisp est clairement un produit de la recherche en IA, mais Fortran vient des calculs scientifiques, C de la programmation système et ML des assistants à la preuve formelle.
[^] # 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é à 5.
Le terme "type-safe" peut désigner plusieurs choses. 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 *).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.
Comme je l'ai déjà dit, je doute que les concepteurs de Java se soient posé la question de la sûreté du typage statique, sinon ils auraient repéré ce problème et, à défaut de le corriger (ce qui n'est pas évident), l'auraient mentionné clairement dans les premières spécifications du langage. Ce n'est pourtant pas le cas dans la "Oak language specification" (version 0.2, la seule que j'ai trouvé facilement sur Internet). Il faut attendre 96, la première "Java language specification", écrite en grande par Guy Steele qui n'a pas participé au design de Java. Cette spécification discute le problème de l'assignement non statiquement sûr dans un tableau en détail, mais elle dit en même temps:
La spécification dit que la covariance des tableaux est "prouvée correcte statiquement". Au mieux c'est une formation ambiguë (ils veulent dire "on sait que c'est faux mais, sachant qu'il y a le test dynamique, plus tard, c'est quand même pas trop grave") qu'une personne attentive à l'aspect théorique de la chose aurait évitée, au pire c'est une erreur.
Après on pourrait dire qu'ils ont effectivement fait une étude théorique et juste laissé passer une erreur dans une preuve. Ça arrive. Mais ça ne colle pas avec la réalité historique qui est que les chercheurs en langages de programmation connaissaient à l'époque déjà très bien le problème. La question du sous-typage est apparue au milieu des années 80, est devenu un sujet chaud et a été très étudiée jusqu'au début des années 90. Le langage Quest de Cardelli contient des types paramétriques (donc sensiblement plus avancé que Java à l'époque), du sous-typage, et des variables modifiables; il discute clairement des problèmes liés à la mutabilité et précise explicitement que les tableaux sont invariants. La spécification de Quest a été publiée en 1994, mais la recherche sur laquelle elle se base date des années 80 (tous les articles cités ont été publiés avant 1990). Si les concepteurs de Java étaient au courant, comme tu le prétends, de la recherche théorique dans le domaine qui les concerne directement, ils auraient certainement été au courant et il me semble fort curieux qu'ils n'en aient donné aucun signe.
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 serais très intéressé par ces sources qui, comme je l'ai dit, iraient à l'encontre de mon intuition propre. Le fait qu'il ait écrit une thèse dans un domaine qui à priori n'a rien à voir avec les langages de programmation1 ne signifie pas grand chose (et par ailleurs si tu as pu mettre la main sur le manuscript de la thèse, je suis intéressé, parce que moi je n'ai rien trouvé).
1: même s'il faut faire attention : son directeur de thèse faisait de l'IA et l'IA, au moins à ses débuts, était très liée à la conception de langages de programmation. Les gens qui faisaient de l'IA s'intéressaient cependant beaucoup plus aux aspects dynamiques des langages (programmation logique, backtracking, systèmes multi-agents, modèles d'acteurs...) qu'aux aspect statique (lambda-calcul typé). Lisp est clairement un produit de la recherche en IA, mais Fortran vient des calculs scientifiques, C de la programmation système et ML des assistants à la preuve formelle.