Catégorisation des systèmes de types (fort / faible, dynamique / statique)

23

En bref: comment les systèmes de types sont-ils classés dans des contextes académiques; en particulier, où puis-je trouver des sources fiables qui rendent les distinctions entre les différents types de système de types clairs?

Dans un sens, la difficulté avec cette question n'est pas que je ne trouve pas de réponse, mais plutôt que j'en trouve trop, et aucune ne se distingue comme correcte. Le fond est que j'essaie d'améliorer un article sur le wiki Haskell sur la dactylographie , qui réclame actuellement les distinctions suivantes:

  • Pas de dactylographie: la langue n'a aucune notion de types, ou d'un point de vue typé: il y a exactement un type dans la langue. Le langage d'assemblage n'a que le type «motif binaire», Rexx et Tk n'ont que le type «texte», le noyau MatLab n'a que le type «matrice à valeurs complexes».
  • Typage faible: il existe seulement quelques types distincts et peut-être des synonymes de types pour plusieurs types. Par exemple, C utilise des nombres entiers pour les booléens, les entiers, les caractères, les ensembles de bits et les énumérations.
  • Typage fort: ensemble de types à grains fins comme dans Ada, langues wirthiennes (Pascal, Modula-2), Eiffel

Ceci est tout à fait contraire à ma perception personnelle, qui était plus dans le sens de:

  • Typage faible: les objets ont des types, mais sont implicitement convertis en d'autres types lorsque le contexte l'exige. Par exemple, Perl, PHP et JavaScript sont tous des langages dans lesquels "1"peuvent être utilisés dans plus ou moins n'importe quel contexte qui le 1peut.
  • Typage fort: les objets ont des types et il n'y a pas de conversions implicites (bien que la surcharge puisse être utilisée pour les simuler), donc utiliser un objet dans le mauvais contexte est une erreur. En Python, l'indexation d'un tableau avec une chaîne ou un flottant lève une exception TypeError; à Haskell, il échouera au moment de la compilation.

J'ai demandé des avis à ce sujet à d'autres personnes plus expérimentées dans le domaine que moi, et l'une d'entre elles a donné cette caractérisation:

  • Typage faible: l'exécution d'opérations invalides sur les données n'est ni contrôlée ni rejetée, mais produit simplement des résultats invalides / arbitraires.
  • Typage fort: les opérations sur les données ne sont autorisées que si les données sont compatibles avec l'opération.

Si je comprends bien, la première et la dernière caractérisation appelleraient C faiblement typé, la seconde l'appellerait fortement typé. Le premier et le second appellent Perl et PHP faiblement typés, le troisième les appellent fortement typés. Tous les trois décriraient Python comme fortement typé.

Je pense que la plupart des gens me diraient "eh bien, il n'y a pas de consensus, il n'y a pas de sens accepté des termes". Si ces personnes se trompent, je serais heureux d'en entendre parler, mais si elles ont raison, comment les chercheurs CS décrivent-ils et comparent-ils les systèmes de types? Quelle terminologie puis-je utiliser qui est moins problématique?

Comme question connexe, je pense que la distinction dynamique / statique est souvent donnée en termes de "temps de compilation" et de "temps d'exécution", ce que je trouve insatisfaisant étant donné que la compilation ou non d'une langue n'est pas tellement une propriété de cette langue. que ses implémentations. Je pense qu'il devrait y avoir une description purement sémantique du typage dynamique versus statique; quelque chose comme «un langage statique est un langage dans lequel chaque sous-expression peut être saisie». J'apprécierais toute réflexion, en particulier les références, qui clarifierait cette notion.

Ben Millwood
la source
6
Je pense que vous avez déjà votre réponse: il n'y a pas de définition acceptée du typage faible et fort.
svick
Je ne trouverais pas cela difficile à croire, mais je pose la question dans l'espoir qu'il y en a une dont je n'ai tout simplement pas entendu parler :) ou du moins une définition plus autoritaire que ce qu'un gars qui a édité un compte wiki est le cas .
Ben Millwood
3
Pour plus de discussion à ce sujet, consultez cette question connexe sur SO .
svick
1
Pour renforcer le point de vue de svick, il n'est pas possible de trouver une référence d'autorité sur quelque chose qui n'est pas accepté. Tout ce qui prétend être autoritaire serait tout simplement faux (car un certain nombre de contre-exemples pourraient être fournis).
edA-qa mort-ora-y
Eh bien, il y a une différence entre quelqu'un qui écrit un article qui dit "voici la seule vraie définition sur laquelle tout le monde est d'accord" et quelqu'un qui écrit un article qui dit "voici les définitions que je vais utiliser pour cet article, bien que je sache qu'il y a autres". Même ce dernier serait meilleur que ce que je sais jusqu'à présent. Je pense que vous avez peut-être raison, dans ce cas, qu'est - ce que les gens ont à dire sur les différents types de système de type? La distinction dynamique / statique est-elle au moins concrète?
Ben Millwood

Réponses:

18

Historiquement, le terme «langage de programmation fortement typé» est apparu dans les années 70 en réaction aux langages de programmation largement utilisés, dont la plupart avaient des trous de type. Quelques exemples:

  • Dans Fortran, il y avait des choses appelées zones de stockage "COMMUNES", qui pouvaient être partagées entre les modules, mais il n'y avait aucune vérification pour voir si chaque module déclarait le contenu du stockage COMMUN avec les mêmes types. Ainsi, un module pourrait déclarer qu'un bloc de stockage COMMON particulier avait un entier et un autre un nombre à virgule flottante, et les données seraient corrompues en conséquence. Fortran avait également des déclarations "EQUIVALENCE", par lesquelles le même stockage pouvait être déclaré contenir deux objets différents de types différents.

  • Dans Algol 60, le type de paramètres de procédure a été déclaré comme étant simplement "procédure", sans spécifier les types de paramètres de la procédure. Ainsi, on pourrait supposer qu'un paramètre de procédure était une procédure acceptant des entiers, mais passer une procédure acceptant réellement comme argument. Cela entraînerait le même type de corruption que les déclarations COMMUNES et ÉQUIVALENCE. (Cependant, Algol 60 a éliminé les problèmes plus anciens.)

  • En Pascal, des "enregistrements de variantes" ont été ajoutés, qui étaient presque exactement comme les anciennes instructions EQUIVALENCE.

  • En C, des «transtypages de type» ont été ajoutés permettant à tout type de données d'être réinterprété en tant que données d'un type différent. Il s'agissait d'un trou de type plutôt délibéré destiné aux programmeurs qui supposément savent ce qu'ils font.

Les langages fortement typés conçus dans les années 70 étaient destinés à éliminer tous ces trous de type. Si vous explorez ce que cela signifie, cela signifie essentiellement que les représentations de données sont protégées. Il n'est pas possible de visualiser l'objet de données d'un type comme un objet d'un autre type qui se trouve avoir le même motif binaire que sa représentation interne. Les théoriciens ont commencé à utiliser le terme «indépendance de représentation» pour caractériser cette propriété au lieu de l'idée vague de «typage fort».

Notez que les langages typés dynamiquement comme Lisp qui effectuent une vérification complète du type au moment de l'exécution sont "fortement typés" dans le sens de protéger les représentations. Dans le même temps, les langages typés statiquement perdraient leur indépendance de représentation à moins de vérifier les limites du tableau. Ils ne sont donc pas "fortement typés" au sens strict du terme. En raison de ces conséquences anormales, le terme "fortement typé" est tombé en désuétude après les années 70. Lorsque le département américain de la Défense a élaboré des exigences rigoureuses pour la conception d'Ada, il a notamment exigé que la langue soit "fortement typée". (On pensait à l'époque que l'idée de "fortement typé" allait de soi. Aucune définition n'a été proposée. ) Toutes les propositions linguistiques soumises en réponse se sont dites "fortement dactylographiées". Lorsque Dijkstra a analysé toutes les propositions linguistiques, il a constaté qu'aucune d'entre elles n'était fortement typée et, en fait, la signification du terme n'était même pas claire. Voir le rapportEWD663 . Cependant, je vois que le terme est de nouveau utilisé maintenant, grâce à une jeune génération de chercheurs qui ne connaissent pas l'histoire mouvementée du terme.

Le terme "typé statiquement" signifie que toute vérification de type est effectuée statiquement et qu'aucune erreur de type ne se produit au moment de l'exécution. Si le langage est également fortement typé, cela signifie qu'il n'y a vraiment aucune erreur de type lors de l'exécution. Si, d'autre part, il existe des trous de type dans le système de type, l'absence d'erreurs de type au moment de l'exécution ne signifie rien. Les résultats pourraient être complètement corrompus.

Le nouveau débat sur le "typage fort vs faible" semble viser à savoir si certaines conversions de types doivent être autorisées. Autoriser une chaîne où un entier est requis est un "typage faible" selon ces gens. Il y a un certain sens à cela car tenter de convertir une chaîne en un entier peut échouer, si la chaîne ne représente pas un entier. Cependant, la conversion d'un entier en chaîne n'a pas ce problème. Serait-ce un exemple de "typage faible" selon ces gens? Je n'ai aucune idée. Je remarque que les discussions de Wikipédia sur le "typage faible" ne citent aucune publication à comité de lecture. Je ne pense pas que ce soit une idée cohérente.

Note ajoutée : Le point fondamental est que le terme "typage fort" n'est pas devenu un terme technique avec une définition rigoureuse. Cela ressemblait plus à ce que certains concepteurs de langage ressentaient: "notre système de type est solide; il capture toutes les erreurs de type; il n'a pas de trous de type" et, donc, lorsqu'ils ont publié leur conception de langage, ils ont affirmé qu'il était "fortement typé" . C'était un mot à la mode qui sonnait bien et les gens ont commencé à l'utiliser. Le document Cardelli-Wegner a été le premier que j'ai vu où une analyse a été fournie sur ce qu'il signifie. Mon message ici doit être considéré comme une élaboration de leur position.

Uday Reddy
la source
Pouvez-vous donner quelques références pour le développement historique? "L'absence d'erreurs de type au moment de l'exécution ne signifie rien" - voulez-vous dire au moment de la compilation ici?
Raphael
Voici un article sur Euclid qui est apparu sur Google Scholar. Je me souviens avoir vu plusieurs articles dans les années 70, où les langues étaient censées être fortement dactylographiées. Il était généralement considéré comme un argumentaire de vente.
Uday Reddy
1
@Raphael. Je voulais dire "erreurs de type au moment de l'exécution". Pour arriver à l'exécution, le programme devrait d'abord dépasser le vérificateur de type statique. Le fait est qu'un langage fortement typé, par exemple Java, donnera des erreurs de type lors de l'exécution lorsqu'il ne pourra pas les vérifier lors de la compilation. Un langage de type trou, par exemple, C, permettra au run-time de produire des ordures au lieu de donner des erreurs.
Uday Reddy
1
@benmachine. Voir la section sur la "vérification de type" dans l'article Euclid que j'ai cité. Je pense que le point principal est que "fortement tapé" est un mot à la mode. Ce n'est pas une notion technique. Au mieux, son contenu technique signifie qu'il n'y a pas de trous de type.
Uday Reddy
1
Sur une implémentation moderne typique où deux types entiers différents ont la même représentation (par exemple les deux intet longétant 32 bits, ou les deux longet long longétant 64, un programme qui utilise un pointeur vers un de ces types pour écrire du stockage et utilise un pointeur de l'autre type pour le lire, ne déclenchera généralement pas une erreur d'exécution détectable, mais peut arbitrairement mal fonctionner de manière arbitraire. Le C moderne perd ainsi la sécurité de type présente dans d'autres langages, sans gagner la sémantique qu'avaient les implémentations de qualité du langage de Ritchie autrefois offert en échange
supercat
7

L'article que Uday Reddy a trouvé dans sa réponse, On Understanding Types, Data Abstraction, and Polymorphism (1985), donne les réponses suivantes:

Les langages de programmation dans lesquels le type de chaque expression peut être déterminé par l'analyse de programme statique sont censés être typés statiquement. Le typage statique est une propriété utile, mais l'exigence selon laquelle toutes les variables et expressions sont liées à un type au moment de la compilation est parfois trop restrictive. Elle peut être remplacée par l'exigence plus faible selon laquelle toutes les expressions doivent être cohérentes avec le type, bien que le type lui-même puisse être statiquement inconnu; cela peut généralement être fait en introduisant une vérification de type au moment de l'exécution. Les langues dans lesquelles toutes les expressions sont cohérentes sont appelées langues fortement typées. Si un langage est fortement typé, son compilateur peut garantir que les programmes qu'il accepte s'exécuteront sans erreur de type. En général, nous devons nous efforcer de taper fort et adopter le typage statique chaque fois que possible.

benmachine
la source
publié en tant que wiki communautaire car je ne mérite pas le mérite d'avoir trouvé cela.
Ben Millwood
Le problème que j'ai ici est lié au premier commentaire de svick. Bien qu'il puisse être agréable que vous ayez trouvé une définition du typage fort, ce n'est certainement pas une définition communément acceptée.
edA-qa mort-ora-y
@ edA-qamort-ora-y: sur quelle base dites-vous cela? Avez-vous quelque chose de mieux que des preuves anecdotiques pour ce qui est et n'est pas communément accepté? Des citations? (Je comprends que vous pourriez avoir un argument valable même si ce n'est pas le cas, mais je pense que ce qui précède répond à ma question; même s'il n'y a pas de consensus, il est bon de connaître au moins une des réponses académiques sérieuses).
Ben Millwood
1
Je ne peux pas vraiment prouver l'absence d'une définition convenue, puis-je? Ce n'est logiquement pas possible. Cependant, les articles de Wikipédia sur la dactylographie forte fournissent de nombreuses preuves et références pour les désaccords et les contradictions. en.wikipedia.org/wiki/Strong_typing
edA-qa mort-ora-y
@ edA-qamort-ora-y: Les citations de Wikipedia ne sont pas vraiment utiles: certaines ne sont pas académiques, d'autres sont citées pour des raisons autres que la définition des termes. Le document de programmation Typeful semble prometteur, mais ne fait que brièvement référence aux définitions; peut-être vaut-il la peine de modifier ma réponse de toute façon. En ce qui concerne la preuve d'absence, je pense que des preuves de controverse / désaccord entre des gens qui savent de quoi ils parlent me suffiraient (ce que le document Typeful Programming peut peut-être me donner).
Ben Millwood
6

Des réponses faisant autorité peuvent être trouvées dans l'article d'enquête de Cardelli et Wegner: sur la compréhension des types, l'abstraction des données et le polymorphisme .

Rappelez-vous que, si le «typage fort» a une signification acceptée, le «typage faible» ne l'est pas. Tout échec de frappe forte peut être considéré comme faible et les gens peuvent différer sur le type d'échec acceptable et sur ce qui ne l'est pas.

Uday Reddy
la source
Excellent, c'est exactement ce que je voulais. Le document demande un peu de lecture, donc je pense qu'il devrait y avoir une réponse qui résume les points saillants. Dois-je les modifier dans votre réponse ou publier ma propre réponse wiki communautaire? Quoi qu'il en soit, je vais lui donner quelques jours de plus au cas où quelqu'un d'autre aurait une entrée, puis accepter ce qui reste :)
Ben Millwood
@benmachine. Le document complet mérite d'être lu, mais les questions conceptuelles de haut niveau ne sont couvertes que dans les deux premières sections.
Uday Reddy
4
Je pense toujours qu'il devrait être résumé sur cette page. Le lien pourrait expirer ultérieurement.
Ben Millwood
@benmachine. Vous êtes invités à publier un résumé comme votre propre réponse à votre question.
Uday Reddy