Re: Encore le type Null...

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.