«Non typé» signifie-t-il aussi «typé dynamiquement» dans le monde universitaire de la CS?

Je lis un jeu de diapositives qui indique «JavaScript n'est pas typé». Cela contredit ce que je pensais être vrai, alors j'ai commencé à creuser pour essayer d'en savoir plus.

Toutes les réponses à JavaScript est-il un langage non typé? dit que JavaScript n'est pas non typé et a offert des exemples de diverses formes de typage statique, dynamique, fort et faible avec lesquelles je suis familier et satisfait ... donc ce n'était pas la voie à suivre.

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

les types universitaires utilisent «non typé» pour signifier «aucun type statique». ils sont assez intelligents pour voir que les valeurs ont des types (duh!). le contexte compte.

Les spécialistes de l'informatique à vocation académique utilisent-ils «non typé» comme synonyme de «typé dynamiquement» (et est-ce valable?) Ou y a-t-il quelque chose de plus profond qui me manque? Je suis d'accord avec Brendan pour dire que le contexte est important, mais toute citation d'explications serait formidable car mes livres "go to" actuels ne jouent pas la balle sur ce sujet.

Je veux clouer ceci pour que je puisse améliorer ma compréhension et parce que même Wikipedia ne fait pas référence à cet usage alternatif (que je peux trouver, de toute façon). Je ne veux pas gâcher l'utilisation du terme ou remettre en question l'utilisation du terme à l'avenir si je me trompe :-)

(J'ai aussi vu un petit Smalltalker dire que Smalltalk est "non typé" aussi, donc ce n'est pas un one-off, ce qui m'a poussé dans cette quête! :-))

Oui, c'est une pratique courante dans la littérature académique. Pour le comprendre, il est utile de savoir que la notion de «type» a été inventée dans les années 1930, dans le contexte du calcul lambda (en fait, même plus tôt, dans le contexte de la théorie des ensembles). Depuis lors, toute une branche de la logique computationnelle est apparue, connue sous le nom de «théorie des types». La théorie du langage de programmation repose sur ces fondations. Et dans tous ces contextes mathématiques, le «type» a une signification particulière et bien établie.

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

Par exemple, voici la définition du «système de types» que Benjamin Pierce utilise dans son manuel standard Types and Programming Languages :

Un système de types est une méthode syntaxique traitable pour prouver l'absence de certains comportements de programme en classant des phrases selon les types de valeurs qu'elles calculent.

Il remarque également:

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

La plupart des personnes travaillant sur le terrain semblent partager ce point de vue.

Notez que cela ne signifie pas que «non typé» et «typé dynamiquement» sont des synonymes. Plutôt, que ce dernier est un nom (techniquement trompeur) pour un cas particulier du premier.

PS: Et FWIW, il se trouve que je suis à la fois un chercheur universitaire dans les systèmes de types et un implémenteur non académique de JavaScript, donc je dois vivre avec le schisme. :)

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 manière. Ce serait bien de réserver le mot pour une utilisation avec des langages qui ne portent pas de balises de type dynamique, comme Forth et le code d'assemblage, 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 les langages comme Scheme, Javascript, etc. devraient être considérés comme des langages typés avec un seul type: valeur. Je me penche sur cette vision, car elle permet de construire une vision du monde cohérente en utilisant un seul formalisme de type.

PS Dans le calcul lambda pur, les seules «valeurs» sont des termes sous forme normale, et les seuls termes fermés sous forme normale sont des fonctions. Mais la plupart des scientifiques qui utilisent le calcul lambda ajoutent des types de base et des constantes, puis vous incluez soit un système de type statique pour lambda, soit vous êtes de retour aux balises de type dynamique.

PPS Vers l'affiche originale: en ce qui concerne les langages de programmation, et en particulier les systèmes de caractères, les informations sur Wikipédia sont de mauvaise qualité. Ne lui fais pas confiance.

J'ai examiné la question et j'ai trouvé que la réponse à votre question est simplement, et étonnamment, "oui": les types de CS universitaires, ou du moins certains d'entre eux, utilisent "non typé" pour signifier "typé dynamiquement". Par exemple, Programming Languages: Principles and Practices , Third Edition (par Kenneth C. Louden et Kenneth A. Lambert, publié en 2012) dit ceci:

Les langages sans système de type statique sont généralement appelés langages non typés (ou langages typés dynamiquement ). Ces langages incluent 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. […]

[ lien ] (note: en gras dans l'original) et continue à utiliser "non typé" de cette manière.

Je trouve cela surprenant (pour à peu près les mêmes raisons qu'affrischke et Adam Mihalcin donnent), mais vous y êtes. :-)

Modifié pour ajouter: vous pouvez trouver plus d'exemples en vous connectant "untyped languages"à Google Recherche de Livres. Par exemple:

[…] C'est le principal mécanisme de dissimulation d'informations dans de nombreuses langues non typées. Par exemple, le schéma PLT [4] utilise des génératifs struct, […]

- Jacob Matthews et Amal Ahmed, 2008 [ lien ]

[…], Nous présentons une analyse en temps de liaison pour un langage fonctionnel non typé […]. […] Il a été implémenté et est utilisé dans un évaluateur partiel pour un dialecte de Scheme sans effets secondaires. L'analyse est cependant suffisamment générale pour être valable pour les langages fonctionnels typés non stricts tels que Haskell. […]

- Charles Consel, 1990 [ lien ]

En passant, mon impression, après avoir parcouru ces résultats de recherche, est que si un chercheur écrit sur un langage fonctionnel "non typé", il le considère très probablement comme "non typé" dans le même sens que le lambda non typé calcul dont parle Adam Mihalcin. Au moins, plusieurs chercheurs mentionnent Scheme et le lambda calcul dans le même souffle.

Ce que la recherche ne dit pas , bien sûr, c'est s'il y a des chercheurs qui rejettent cette identification et ne considèrent pas ces langues comme "non typées". Eh bien, j'ai trouvé ceci:

J'ai alors réalisé qu'il n'y avait vraiment pas 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 à partir du texte du programme.

- quelqu'un (je ne sais pas qui), 1998 [ lien ]

mais évidemment, la plupart des gens qui rejettent cette identification ne ressentiraient pas le besoin de le dire explicitement.

Non typé et typé dynamiquement ne sont absolument pas des synonymes. Le langage le plus souvent appelé "non typé" est le Lambda Calculus, qui est en fait un langage unitaire - tout est une fonction, nous pouvons donc prouver statiquement que le type de tout est la fonction. Un langage typé dynamiquement a plusieurs types, mais n'ajoute pas un moyen pour le compilateur de les vérifier statiquement, forçant le compilateur à insérer des vérifications d'exécution sur les types de variables.

Ensuite, JavaScript est un langage typé dynamiquement: il est possible d'écrire des programmes en JavaScript de telle sorte qu'une variable xpuisse être un nombre, ou une fonction, ou une chaîne, ou autre chose (et déterminer lequel exigerait de résoudre le problème d'arrêt ou quelque problème mathématique difficile), vous pouvez donc appliquer xà un argument et le navigateur doit vérifier au moment de l'exécution qu'il xs'agit d'une fonction.

Les deux déclarations sont correctes, selon que vous parlez 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, les valeurs et non les variables portent des types. Toutes les variables peuvent s'étendre sur tous les types de valeurs et peuvent être considérées comme «typées dynamiquement» ou «non typées» - du point de vue de la vérification de type, une variable qui n'a pas de type / inconnaissable 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 en parlent généralement - des variables portant des types - parce qu'ils sont intéressés par l'écriture de vérificateurs de type et de compilateurs, etc., qui fonctionnent 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 des valeurs).

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

Cette question concerne la sémantique

Si je vous donne ces données: 12quel est son type? Vous n'avez aucun moyen de le savoir avec certitude. Peut être un entier - peut être un flottant - peut être une chaîne. En ce sens, ce sont des données très "non typées".

Si je vous donne un langage imaginaire qui vous permet d'utiliser des opérateurs comme "ajouter", "soustraire" et "concaténer" sur ces données et sur d'autres données arbitraires, le "type" est quelque peu hors de propos (pour mon langage imaginaire) (exemple : peut-être add(12, a)donne 109ce qui est 12plus la valeur ascii de a).

Parlons C pendant une seconde. C vous permet à peu près de faire ce que vous voulez avec n'importe quelle donnée arbitraire. Si vous utilisez une fonction qui prend deux uints - vous pouvez lancer et passer tout ce que vous voulez - et les valeurs seront simplement interprétées comme uints. En ce sens, C est "non typé" (si vous le traitez de cette manière).

Cependant - et pour en venir au point de Brendan - si je vous disais que "Mon âge est 12" - alors 12a un type - au moins nous savons que c'est numérique. Avec le contexte, tout a un type - quelle que soit la langue.

C'est pourquoi j'ai dit au début - votre question est une question de sémantique. Quelle est la signification de «non typé»? Je pense que Brendan a frappé dans le mille quand il a dit "pas de types statiques" - parce que c'est tout ce que cela peut signifier. Les humains classent naturellement les choses en types. Nous savons intuitivement qu'il y a quelque chose de fondamentalement différent entre une voiture et un singe - sans jamais apprendre à faire ces distinctions.

Revenons à mon exemple du début - un langage qui "ne se soucie pas des types" (en soi) peut vous permettre "d'ajouter" un "âge" et un "nom" sans produire d'erreur de syntaxe ... mais cela ne veut pas dire que c'est une opération logique.

Javascript peut vous permettre de faire toutes sortes de choses folles sans les considérer comme des «erreurs». Cela ne veut pas dire que ce que vous faites est logique. C'est au développeur de travailler.

Un système / langage qui n'applique pas la sécurité de type au moment de la compilation / construction / interprétation est-il "non typé" ou "typé dynamiquement"?

Sémantique.

ÉDITER

Je voulais ajouter quelque chose ici parce que certaines personnes semblent être rattrapées par "ouais, mais Javascript a quelques" types "".

Dans mon commentaire sur la réponse de quelqu'un d'autre, j'ai dit:

En Javascript, je pourrais avoir des objets que j'ai construits pour être des "singes" et des objets que j'ai construits pour être des "humains" et certaines fonctions pourraient être conçues pour fonctionner uniquement sur des "humains", d'autres sur des "singes", et encore d'autres sur seulement "Things With Arms". Que le langage ait déjà été dit ou non qu'il existe une catégorie d'objets telle que «choses avec des bras» est aussi hors de propos pour l'assemblage («non typé») que pour Javascript («dynamique»). Tout est une question d'intégrité logique - et la seule erreur serait d'utiliser quelque chose qui n'a pas d'armes avec cette méthode.

Donc, si vous considérez que Javascript a une certaine "notion de types" en interne - et, par conséquent, des "types dynamiques" - et pensez que c'est en quelque sorte "distinctement différent d'un système non typé" - vous devriez voir dans l'exemple ci-dessus que toute "notion de types "qu'il a en interne est vraiment hors de propos.

Pour effectuer la même opération avec C #, par exemple, J'AI BESOIN d'une interface appelée ICreatureWithArmsou quelque chose de similaire. Pas si en Javascript - pas si en C ou ASM.

De toute évidence, le fait que Javascript comprenne ou non les «types» n'a aucune importance.

S'il est vrai que la plupart des chercheurs de CS qui écrivent sur les types ne considèrent essentiellement que les langages avec des types syntaxiquement dérivés comme des langages typés, nous sommes beaucoup plus nombreux à utiliser des langages typés dynamiquement / latemment qui prennent ombrage à cet usage.

Je considère qu'il y a 3 types [SIC] de langues:

Non typé - seul l'opérateur détermine l'interprétation de la valeur - et cela fonctionne généralement sur n'importe quoi. Exemples: assembleur, BCPL

Typé statiquement - les expressions / variables ont des types qui leur sont associés, et ce type détermine l'interprétation / la validité de l'opérateur au moment de la compilation. Exemples: C, Java, C ++, ML, Haskell

Typiquement dynamiquement - les valeurs sont associées à des types, et ce type détermine l'interprétation / la validité de l'opérateur au moment de l'exécution. Exemples: LISP, Scheme, Smalltalk, Ruby, Python, Javascript

À ma connaissance, tous les langages à typage dynamique sont de type sûr - c'est-à-dire que seuls les opérateurs valides peuvent opérer sur des valeurs. Mais il n'en va pas de même pour un langage de type statique. Selon la puissance du système de type utilisé, certains opérateurs peuvent être contrôlés uniquement à l'exécution, ou pas du tout. Par exemple, la plupart des langages à typage statique ne gèrent pas correctement le débordement d'entier (l'ajout de 2 entiers positifs peut produire un entier négatif), et les références de tableau hors limites ne sont pas vérifiées du tout (C, C ++) ou sont vérifiées uniquement à Durée. De plus, certains systèmes de types sont si faibles qu'une programmation utile nécessite des hachures d'échappement (casts en C et en famille) pour changer le type d'expressions à la compilation.

Tout cela conduit à des affirmations absurdes, telles que le fait que C ++ est plus sûr que Python car il est (de type statique), alors que la vérité est que Python est intrinsèquement sûr alors que vous pouvez tirer votre épingle du jeu avec C ++.

Je ne suis pas un informaticien, mais je serais plutôt surpris si «non typé» était vraiment utilisé comme synonyme de «typé dynamiquement» dans la communauté CS (au moins dans les publications scientifiques) car à mon avis ces deux termes décrivent des concepts différents. Un langage typé dynamiquement a une notion de types et il applique les contraintes de type à l'exécution (vous ne pouvez pas par exemple diviser un entier par une chaîne en Lisp sans obtenir une erreur) alors qu'un langage non typé n'a aucune notion de types à tous (par exemple assembleur). Même l'article de Wikipedia sur les langages de programmation (http://en.m.wikipedia.org/wiki/Programming_language#Typed_versus_untyped_languages) fait cette distinction.

Mise à jour: Peut-être que la confusion vient du fait que certains textes disent quelque chose dans la mesure où «les variables ne sont pas tapées» en Javascript (ce qui est vrai). Mais cela ne signifie pas automatiquement que la langue n'est pas typée (ce qui serait faux).

D'accord avec Brendan - le contexte est tout.

Ma prise:

Je me souviens avoir été confus, vers 2004, parce qu'il y avait des disputes pour savoir si Ruby était non typé ou dynamiquement tapé. Les gens de la vieille école C / C ++ (dont je faisais partie) pensaient au compilateur et disaient que Ruby n'était pas typé.

Rappelez-vous, en C, il n'y a pas de types d'exécution, il y a juste des adresses et si le code qui s'exécute décide de traiter tout ce qui se trouve à cette adresse comme quelque chose qu'il n'est pas, oups. C'est définitivement non typé et très différent du typé dynamiquement.

Dans ce monde, "taper" est tout au sujet du compilateur. C ++ avait un "typage fort" car les vérifications du compilateur étaient plus strictes. Java et C étaient plus «faiblement typés» (il y avait même des arguments pour savoir si Java était fortement ou faiblement typé). Les langages dynamiques étaient, dans ce continuum, "non typés" car ils n'avaient pas de vérification de type de compilateur.

Aujourd'hui, pour les programmeurs expérimentés, nous sommes tellement habitués aux langages dynamiques, que nous pensons évidemment à non typé pour signifier pas de vérification de type de compilateur ni d'interpréteur, ce qui serait incroyablement difficile à déboguer. Mais il y a eu une période là-bas où cela n'était pas évident et dans le monde plus théorique de la CS, cela n'a peut-être même pas de sens.

Dans un sens profond, rien ne peut être non typé (ou presque rien, de toute façon) parce que vous devez avoir une certaine intention de manipuler une valeur pour écrire un algorithme significatif. C'est le monde du CS théorique, qui ne traite pas des spécificités de l'implémentation d'un compilateur ou d'un interpréteur pour un langage donné. Donc, "non typé" est (probablement, je ne sais pas) totalement dénué de sens dans ce contexte.