Est-ce que "non typé" signifie également "dynamiquement typé" dans le monde universitaire de la société civile ?

Question

Je lis un diaporama qui dit que "JavaScript est untypé". Cela contredisait ce que je pensais être vrai, alors j'ai commencé à creuser pour essayer d'en savoir plus.

Chaque réponse à JavaScript est-il un langage non typé ? dit que JavaScript est no non typée et offrait des exemples de diverses formes de typage statique, dynamique, fort et faible avec lesquelles je suis familier et heureux donc ce n'était pas la voie à suivre.

J'ai donc demandé à Brendan Eich, le créateur de JavaScript, et il a répondu :

les types académiques utilisent "untyped" pour signifier "pas de types statiques". ils sont assez intelligents pour voir que les valeurs ont des types (duh !). le contexte importe.

Les informaticiens à vocation académique utilisent-ils "untyped" comme synonyme de "dynamically typed" (et est-ce valable ?) ou y a-t-il quelque chose de plus profond que je ne comprends pas ? Je suis d'accord avec Brendan sur le fait que le contexte est important, mais toute citation d'explications serait la bienvenue, car mes livres actuels ne jouent pas le jeu sur ce sujet.

Je veux en avoir le cœur net afin d'améliorer ma compréhension et parce que même Wikipédia ne fait pas référence à cet usage alternatif (que je peux trouver, du moins). Je ne veux pas m'embrouiller en utilisant le terme ou en remettant en question son utilisation à l'avenir si je me trompe :-)

(J'ai également vu un grand Smalltalker dire que Smalltalk est "untyped" aussi, donc ce n'est pas un cas isolé qui m'a poussé à cette quête ! :-))

Answer 1

Oui, c'est une pratique courante dans la littérature académique. Pour le comprendre, il faut savoir que la notion de "type" a été inventée dans les années 1930, dans le contexte du lambda-calcul (en fait, même avant, dans le contexte de la théorie des ensembles). Depuis lors, une branche entière de la logique informatique a vu le jour, connue sous le nom de "théorie des types". La théorie des langages de programmation repose sur ces fondements. Et dans tous ces contextes mathématiques, le terme "type" a une signification particulière et bien établie.

La terminologie "typage dynamique" a été inventée beaucoup plus tard - et elle est une contradiction dans les termes face à l'utilisation mathématique commune du mot "type".

Par exemple, voici la définition de "système de types" que Benjamin Pierce utilise dans son livre de texte standard Types et langages de programmation :

Un système de type est une méthode syntaxique traçable pour prouver l'absence de certains comportements de programme en classant les phrases en fonction de la nature de leur contenu. types de valeurs qu'elles calculent.

Il remarque également :

Le mot "statique" est parfois ajouté explicitement - on parle d'une "langage de programmation à typage statique", par exemple, pour distinguer les le type d'analyses de compilation que nous considérons ici des analyses typage dynamique ou latent que l'on trouve dans des langages comme Scheme (Sussman et Steele, 1975 ; Kelsey, Clinger et Rees, 1998 ; Dybvig, 1996), où les balises de type à l'exécution sont utilisées pour distinguer les différents types de structures dans le tas. Des termes tels que "dynamiquement typé" sont sans doute des et devraient probablement être remplacées par "vérifié dynamiquement", mais mais l'usage est standard.

La plupart des personnes travaillant dans ce domaine semblent partager ce point de vue.

Notez que cela ne no signifie que "non typé" et "dynamiquement typé" sont synonymes. Plutôt, que le second est un nom (techniquement trompeur) pour un cas particulier du premier.

PS : Et pour info, il se trouve que je suis à la fois un chercheur universitaire en systèmes de types et un implémenteur non universitaire de JavaScript, donc je dois vivre avec la schisma :).

Answer 2

Je suis un informaticien universitaire spécialisé dans les langages de programmation, et oui, le mot "non typé" est fréquemment (mal) utilisé de cette façon. Ce serait bien de réserver ce mot aux langages qui ne portent pas de balises de type dynamique, comme le Forth et le code assembleur, mais ces langages sont rarement utilisés et encore plus rarement étudiés, et il est beaucoup plus facile de dire "non typé" que "typé dynamiquement".

Bob Harper aime à dire que des langages comme Scheme, Javascript, etc. devraient être considérés comme des langages typés avec un seul type : la valeur. Je penche pour ce point de vue, car il permet de construire une vision du monde cohérente en utilisant un seul formalisme de type.

P.S. Dans le lambda-calcul pur, les seules "valeurs" sont les termes de la forme normale, et les seules "valeurs" sont les termes de la forme normale. fermé Les termes sous forme normale sont des fonctions. Mais la plupart des scientifiques qui utilisent le calcul de lambda ajoutent des types de base et des constantes, et ensuite, soit vous incluez un système de type statique pour lambda, soit vous revenez directement aux balises de type dynamiques.

P.P.S. À l'attention de l'auteur de la lettre d'origine : lorsqu'il s'agit de langages de programmation, et en particulier de systèmes de types, les informations figurant sur Wikipédia sont de mauvaise qualité. Ne vous y fiez pas.

Answer 3

Je me suis penché sur la question et j'ai découvert que la réponse à votre question est simplement, et de manière surprenante, "oui" : les types CS académiques, ou du moins certains d'entre eux, utilisent "non typés" pour signifier "typés dynamiquement". Par exemple, Langages de programmation : Principes et pratiques , troisième édition (par Kenneth C. Louden et Kenneth A. Lambert, publié en 2012) dit ceci :

Les langages sans système de types statiques sont généralement appelés les langues non typées (ou les langages typés dynamiquement ). Ces langages comprennent Scheme et d'autres dialectes de Lisp, Smalltalk et la plupart des langages de script tels que Perl, Python et Ruby. Notez cependant qu'un langage non typé ne permet pas nécessairement aux programmes de corrompre les données - cela signifie simplement que toutes les vérifications de sécurité sont effectuées au moment de l'exécution. [ ]

[ enlace ] (note : caractères gras dans l'original) et utilise ensuite "untyped" de cette manière.

Je trouve cela surprenant (pour à peu près les mêmes raisons qu'afrischke et Adam Mihalcin), mais voilà :-)

---

Modifié pour ajouter : Vous pouvez trouver d'autres exemples en branchant "untyped languages" dans Google Book Search. Par exemple :

[ ] Il s'agit du principal mécanisme de dissimulation de l'information dans de nombreux langages non typés. Par exemple, le PLT Scheme [4] utilise le mécanisme génératif de la struct s, [ ]

- Jacob Matthews et Amal Ahmed, 2008 [ enlace ]

[ ] nous présentons une analyse du temps de liaison pour un langage fonctionnel non typé [ ]. [ ] Elle a été implémentée et est utilisée dans un évaluateur partiel pour un dialecte de Scheme sans effets secondaires. L'analyse est cependant suffisamment générale pour être valable pour des langages fonctionnels non strictement typés tels que Haskell. [ ]

- Charles Consel, 1990 [ enlace ]

D'ailleurs, mon impression, après avoir parcouru ces résultats de recherche, est que si un chercheur écrit sur un langage fonctionnel "non typé", il est très probable qu'il le considère comme "non typé" dans le même sens que le lambda calculus non typé mentionné par Adam Mihalcin. En tout cas, plusieurs chercheurs mentionnent Scheme et le lambda calculus dans le même souffle.

Ce que la recherche n'a pas dire, bien sûr, est de savoir s'il existe des chercheurs qui rejettent cette identification, et Ne le fais pas. considèrent que ces langues sont "non typées". J'ai trouvé ça :

J'ai ensuite réalisé qu'il n'y avait pas vraiment de circularité, car les langages typés dynamiquement ne sont pas des langages non typés - c'est juste que les types ne sont généralement pas immédiatement évidents dans le texte du programme.

- quelqu'un (je ne peux pas dire qui), 1998 [ enlace ]

mais évidemment le plus les personnes qui rejettent cette identification ne ressentiraient pas le besoin de le dire explicitement.

Answer 4

Untyped et dynamically typed ne sont absolument pas synonymes. Le langage le plus souvent appelé "non typé" est le Lambda Calculus, qui est en fait un langage unipolaire - tout est une fonction, et nous pouvons donc prouver statiquement que le type de tout est la fonction. Un langage dynamiquement typé possède plusieurs types, mais n'ajoute pas de moyen pour le compilateur de les vérifier statiquement, ce qui oblige le compilateur à insérer des vérifications à l'exécution sur les types des variables.

Ensuite, JavaScript est un langage dynamiquement typé : il est possible d'écrire des programmes en JavaScript de telle sorte que certaines variables x peut être un nombre, une fonction, une chaîne de caractères ou autre chose (et pour déterminer lequel de ces éléments il faudrait résoudre le Halting Problem ou un autre problème mathématique difficile). x à un argument et le navigateur doit vérifier au moment de l'exécution que x est une fonction.

Answer 5

Les deux affirmations sont correctes, selon que l'on parle de valeurs ou de variables. Les variables JavaScript ne sont pas typées, les valeurs JavaScript ont des types, et les variables peuvent s'étendre sur n'importe quel type de valeur au moment de l'exécution (c'est-à-dire "dynamiquement").

En JavaScript et dans de nombreux autres langages, ce sont les valeurs et non les variables qui portent les types. Toutes les variables peuvent s'étendre sur tous les types de valeurs et peuvent être considérées comme "dynamiquement typées" ou "non typées" - du point de vue de la vérification du type, une variable dont le type est inconnu ou inconnu et une variable qui peut prendre n'importe quel type sont logiquement et pratiquement équivalentes. Lorsque les théoriciens des types parlent de langages et de types, ils parlent généralement de cela - des variables portant des types - parce qu'ils sont intéressés par l'écriture de vérificateurs de types et de compilateurs, etc., qui opèrent sur le texte du programme (c'est-à-dire les variables) et non sur un programme en cours d'exécution en mémoire (c'est-à-dire les valeurs).

En revanche, dans d'autres langages, comme le C, les variables portent des types mais pas les valeurs. Dans des langages comme Java, les variables et les valeurs portent toutes deux des types. En C++, certaines valeurs (celles qui ont des fonctions virtuelles) portent des types et d'autres non. Dans certains langages, il est même possible que les valeurs changent de type, bien que cela soit généralement considéré comme une mauvaise conception.