FAQ sur le système de type

L'auteur de l'article, dont nous publions la traduction aujourd'hui, affirme que ce billet et ses commentaires ont servi de source d'inspiration pour sa rédaction. Selon lui, les informaticiens ont des idées fausses sur les types, utilisent une terminologie incorrecte et, discutant des problèmes liés aux types, tirent des conclusions erronées. Il note qu'il n'est pas un défenseur du système de type statique. La seule chose qui le dérange est l'utilisation correcte des termes. Cela permet des discussions constructives. L'auteur dit qu'il a écrit ce matériel spontanément, mais espère qu'il ne contient aucune erreur. S'il a confondu quelque chose, il demande de le lui faire savoir.



Comprenons une fois pour toutes ce qui cause la confusion lorsque l'on parle de systèmes de types.

Saisie dynamique et manque de frappe

Certaines personnes pensent qu'un système de type dynamique est identique à un système de type non typé. L'absence de saisie signifie que dans un certain système de types, il est inutile de distinguer les types. Cela n'a aucun sens de distinguer les types même si un seul type est présent dans le système de types. Par exemple:

• Dans l'assembleur, le seul type est une chaîne de bits.
• Dans le calcul lambda, le seul type est la fonction.

Quelqu'un peut dire ceci à cette occasion: "Mais quelle différence cela fait-il - la frappe dynamique ou le manque de frappe - aussi une question pour moi." Mais cela, en fait, est un problème important et important. Le fait est que si vous assimilez le typage dynamique au manque de typage, cela signifie l'adoption automatique du fait qu'un système de type dynamique est l'opposé d'un système de type statique. En conséquence, deux camps opposés de programmeurs sont formés - le camp de typage dynamique et le camp de typage statique (et cela, comme nous le verrons dans la section correspondante, est faux).

Les langages qui ne limitent pas la plage de valeurs des variables sont appelés langages non typés: ils n'ont pas de types ou, ce qui est la même chose, ils n'ont qu'un seul type universel qui contient toutes les valeurs.
_{Systèmes de types, Luca Cardelli}

Les langages de programmation ont une fonctionnalité intéressante qui vous permet de diviser grossièrement leur monde en deux groupes:

• Langues non typées - les programmes s'exécutent simplement. Cela se fait rapidement, sans chercher à vérifier «l'uniformité des formes».
• Langages typés - une tentative est faite pour vérifier «l'uniformité de la forme» - soit pendant la compilation, soit pendant l'exécution du programme.

_{«Systèmes de types pour les langages de programmation», Benjamin Pearce}

Typage dynamique et statique

Un système de type dynamique est un système dans lequel les types sont vérifiés dynamiquement (pendant l'exécution du programme). Un système de type statique est un système dans lequel les types sont vérifiés statiquement (lors de la compilation ou de la traduction du code).

L'un de ces systèmes est-il l'opposé de l'autre? Non, ça ne l'est pas. Les deux types de systèmes peuvent être utilisés dans la même langue. En fait, la plupart des systèmes de type statiques ont également des vérifications de type dynamiques. À titre d'exemple, considérons la validation des opérations d'entrée-sortie (entrée-sortie, IO). Imaginez que vous devez lire les données fournies par un utilisateur qui doit saisir un numéro. Vous vérifierez, pendant l'exécution du programme, si le nombre est le résultat de l'analyse de la ligne correspondante (à la suite de l'analyse, une exception peut être levée ou quelque chose comme NaN sera retourné). Lorsque vous vérifiez les données entrées par l'utilisateur, en déterminant si elles peuvent être considérées comme un nombre - vous effectuez une vérification de type dynamique.

En conséquence, nous pouvons noter l'absence de confrontation entre les types statiques et dynamiques. Vous pouvez utiliser, dans la même langue, ceux-ci et les autres.

De plus, il convient de noter que la vérification de type statique est un processus complexe. Parfois, il est très difficile de vérifier statiquement certaines parties d'un programme. Par conséquent, au lieu d'appliquer des vérifications de type statique, vous pouvez recourir à des vérifications dynamiques.

Il est recommandé de considérer un système de type statique comme des types qui sont vérifiés statiquement. Un système de type dynamique est comme des types qui sont vérifiés dynamiquement.

L'utilisation de types statiques signifie-t-elle connaître les types au moment de la compilation?

La question posée dans le titre de cette section peut recevoir une réponse négative. Si vous ouvrez le code source d'un analyseur (y compris l'analyseur JavaScript), vous pouvez voir que l'analyseur connaît les types de valeurs pendant l'analyse (cela fait partie du processus de compilation).

 let x = "test"; 

Il s'avère que l'analyseur sait que "test" est une chaîne. Cela fait-il de JavaScript un langage typé statique? Non, non.

Saisie progressive

Un système de type progressif est un système de type statique qui vous permet d'ignorer les vérifications de type pour certaines parties d'un programme. Par exemple, dans TypeScript, cela est implémenté en utilisant any ou @ts-ignore .

D'une part, cela rend le système de type moins sûr. D'un autre côté, un système de typage avec typage progressif vous permet d'ajouter progressivement des descriptions de typage aux langues avec typage dynamique.

Systèmes de type fiables et peu fiables

Si vous utilisez un système de type fiable (système de type sonore), le programme ne sera pas «approuvé» lors de la vérification de type si ce programme contient des erreurs liées aux types. L'utilisation d'un système de type défectueux entraîne la possibilité d'erreurs de type dans le programme. Certes, vous ne devriez pas paniquer après l'avoir découvert. En pratique, cela peut ne pas vous affecter. La fiabilité ou la solidité est une propriété mathématique d'un algorithme de vérification de type qui nécessite une preuve. De nombreux compilateurs existants (en interne, systèmes de vérification de type) ne sont pas fiables.

Si vous souhaitez travailler avec des systèmes de type fiables, jetez un œil aux langages de programmation de la famille ML, qui utilisent le système de type Hindley-Milner.

De plus, il faut comprendre qu'un système de type fiable ne sautera pas le mauvais programme (il ne donne pas de résultats de test faussement positifs, considérant que les mauvais programmes sont corrects), mais il peut ne pas manquer le programme correct (il peut donner des résultats de test faussement négatifs).

Un système de type qui ne rejette jamais le bon programme est appelé complet.

Arrive-t-il qu'un système de type soit à la fois fiable et complet? Pour autant que je sache, de tels systèmes de types n'existent pas. Je ne suis pas sûr de cela jusqu'à la fin, mais il me semble que l'existence de tels systèmes de types, s'ils sont basés sur le théorème d'incomplétude de Gödel, est fondamentalement impossible (je peux cependant me tromper à ce sujet).

Typage faible et fort

Je trouve inapproprié d'utiliser les termes «frappe faible» et «frappe forte». Ces termes sont ambigus, leur utilisation peut donner plus de confusion que de clarté. Permettez-moi de vous donner quelques citations.

Ces langues peuvent être appelées, au sens figuré, des langues à vérification de type faible (ou des langues faiblement typées, comme elles sont généralement appelées dans diverses publications). L'utilisation d'une vérification de type faible dans la langue signifie que certaines opérations dangereuses sont détectées statiquement, et d'autres non. La «faiblesse» des vérifications de type dans les langues de cette classe varie considérablement.
_{Systèmes de types, Luca Cardelli}

La façon la plus courante de classer les systèmes de types est probablement de les diviser en systèmes de typage «faible» et «fort». Cela ne peut être que regretté, car ces mots n'ont pratiquement aucun sens en eux-mêmes. Il est possible, dans une mesure limitée, de comparer deux langues qui ont des systèmes de types très similaires et de sélectionner l'une d'entre elles comme ayant un système de types plus fort que la seconde. Dans d'autres cas, les termes «typage fort» et «typage faible» n'ont aucun sens.
_{«Choses à savoir avant de discuter des systèmes de type», Steve Klabnik}

Les termes «typage fort» et «typage faible» sont extrêmement ambigus. Voici quelques exemples de leur utilisation:

• Parfois, «typage fort» signifie «typage statique». Il n'est pas difficile de faire une telle «substitution», mais il vaut mieux, en parlant de typage statique, simplement l'appeler «statique». Le fait est que la plupart des programmeurs comprennent clairement ce terme.
• Parfois, quand ils disent «typage fort», ils signifient «l'absence d'une conversion de type implicite». Par exemple, en JavaScript, vous pouvez utiliser des expressions comme "a" - 1 . Cela peut être appelé un modèle de "typage faible". Mais presque tous les langages offrent au programmeur des opportunités de conversion de type implicite, par exemple, en prenant en charge la conversion automatique d'entiers en nombres à virgule flottante dans des expressions comme 1 - 1.1 . Dans la pratique, la plupart des professionnels qui utilisent le terme «typage fort» de cette manière distinguent les conversions de type «acceptable» et «inacceptable». Mais il n'y a pas de frontière généralement acceptée entre ces conversions de type. L '«acceptabilité» et «l'inacceptabilité» des transformations est une évaluation subjective, selon l'opinion d'une personne en particulier.
• Parfois, les langues avec "typage fort" sont appelées les langues dans lesquelles il est impossible de contourner les règles du système de types qui y existe.
• Parfois, «taper fort» signifie avoir un système de saisie qui vous permet de travailler en toute sécurité avec la mémoire. Le langage C est un exemple notable d'un langage qui n'est pas sûr avec la mémoire. Par exemple, si xs est un tableau de quatre nombres, C approuvera sans problème un code qui utilise des constructions comme xs[5] ou xs[1000] . Ils vous permettront d'accéder à la mémoire située après les adresses allouées pour stocker le contenu du tableau xs .

_{Les types, Gary Bernard}

Les langages typés statiques ont-ils besoin de déclarations de type?

Les langages typés statiquement n'ont pas toujours besoin de déclarations de type. Parfois, un système de types peut déduire des types (en faisant des hypothèses basées sur la structure du code). Voici un exemple (TypeScript):

 const x = "test"; 

Le système de type sait que "test" est une chaîne (cette connaissance est basée sur les règles d'analyse de code). Le système de types sait également que x est une constante, c'est-à-dire que la valeur de x ne peut pas être réaffectée. Par conséquent, on peut conclure que x est de type chaîne.
Voici un autre exemple (Flow):

 const add = (x, y) => x / y //            ^        [1]   . add(1, "2") 

Le système de vérification de type voit que nous appelons la fonction add , en lui passant un nombre et une chaîne. Ceci analyse la déclaration de fonction. Le système de vérification de type sait que pour effectuer l'opération de division, les numéros doivent être à droite et à gauche de l'opérateur correspondant. L'un des opérandes impliqués dans l'opération de division n'est pas un nombre. En conséquence, nous sommes informés de l'erreur.

Il n'y a pas de déclaration de type ici, mais cela n'empêche pas une vérification de type statique du programme ci-dessus. Si vous rencontrez des situations similaires dans le monde réel, alors, tôt ou tard, vous devrez déclarer certains types. Le système de types ne peut pas déduire absolument tous les types. Mais vous devez comprendre qu'un langage peut être appelé «statique» non pas parce qu'il utilise des déclarations de type, mais parce que les types sont vérifiés avant le démarrage du programme.

TypeScript est-il un langage dangereux car le code qui y est écrit est compilé en code JavaScript?

TypeScript est un langage malsain. Par conséquent, le code écrit dessus peut se transformer en applications dangereuses. Mais cela n'a rien à voir avec ce qu'il compile.

La plupart des compilateurs de bureau convertissent les programmes en quelque chose qui ressemble à un langage d'assemblage. Et l'assembleur est un langage encore moins sécurisé que JS.

Ici, si vous revenez à l'idée que TS n'est pas sécurisé en raison de la compilation dans JS, vous pourriez obtenir la pensée suivante: «Le code compilé est exécuté dans le navigateur, JS est un langage dangereux, et il peut tout à fait substituer null à l'endroit où la ligne est attendue ". La pensée est sensée. Mais cela, encore une fois, ne donne pas de raison d'appeler TS un langage dangereux. Afin que TS garantisse la sécurité au sein de l'application, vous devez placer les «mécanismes de défense» aux endroits où le code TS interagit avec le monde extérieur. C'est-à-dire, par exemple, que vous devez vérifier l'exactitude des données entrant dans le programme via les mécanismes d'entrée-sortie. Disons que cela peut être de vérifier ce que l'utilisateur entre, de vérifier les réponses du serveur, de vérifier les données lues à partir du stockage du navigateur, etc.

Par exemple, le rôle de ces «mécanismes de défense» dans Elm est joué par les « ports ». Dans TS, vous pouvez utiliser quelque chose comme io-ts pour cela.

Le «mécanisme de protection» correspondant crée un pont entre les systèmes de type statique et dynamique.

Voici un exemple simplifié:

 const makeSureIsNumber = (x: any) => {  const result = parseFloat(x);  if (isNaN(result)) {    throw Error("Not a number");  }  return result; } const read = (input: any) => {  try {    const n = makeSureIsNumber(input);    //     n, ,      //              // makeSureIsNumber "" , n    } catch (e) { } } 

Est-il vrai que les types ne sont nécessaires que pour les compilateurs?

Les types ne sont que le hack nécessaire pour donner des indices au compilateur.
_{Waut Mertens}

Les types sont-ils uniquement nécessaires aux compilateurs? C'est une question philosophique. Les types sont nécessaires pour les gens, pas pour les voitures. Les compilateurs ont besoin de types car ce sont des programmes écrits par des personnes.

Le phénomène des types existe à cause des gens. Les types n'existent que lorsqu'une personne perçoit quelque chose sous la forme d'un «type de données». L'esprit humain divise différentes entités en différentes catégories. Les types n'ont pas de sens sans un observateur.

Organisons une expérience de pensée. Pensez au jeu Life. Vous avez une grille bidimensionnelle composée de cellules carrées. Chacune des cellules peut être dans deux états possibles. Il peut être "vivant" ou "mort". Chaque cellule peut interagir avec ses huit voisins. Ce sont des cellules qui la bordent verticalement, horizontalement ou en diagonale. Dans le processus de recherche de l'état suivant du système, les règles suivantes s'appliquent:

• Une cellule «vivante» avec moins de deux voisins «vivants» «meurt», comme dans une faible densité de population.
• Une cellule «vivante» avec deux ou trois voisins «vivants» survit et tombe dans la génération suivante.
• Une cellule «vivante», avec plus de trois voisins «vivants», «meurt», comme en surpopulation.
• La cellule «morte», qui a exactement trois voisins «vivants», devient «vivante», comme dans la reproduction de la population.

Extérieurement, il ressemble à un champ, divisé en cellules carrées, qui sont constamment «activées» et «désactivées». Ici, vous pouvez jeter un œil à cela.

Si vous observez la vie pendant un certain temps, des structures stables comme des «planeurs» peuvent apparaître sur le terrain.


Planeur

Tu le vois? Un planeur se déplace sur l'écran. Non? Maintenant, ralentissons un peu. Ce planeur existe-t-il vraiment? Ce ne sont que des carrés individuels qui apparaissent et disparaissent. Mais notre cerveau peut percevoir cette structure comme quelque chose qui existe objectivement.

De plus, on peut dire que le "planeur" existe parce que les carrés ne sont pas indépendants (ils dépendent des voisins), et même si le "planeur" lui-même n'existe pas, alors il y a un "planeur" dans la forme idées platoniques.

Résumé

Considérez tout programme écrit dans un langage de programmation typé. On peut observer les types. Non? Mais le programme se compile en codes machine. Dans ces codes, la même chose est exprimée que dans le programme d'origine (bien qu'il soit difficile pour une personne de lire les représentations de programmes de la machine). D'un point de vue informatique, il n'y a pas de types. Il ne voit que la séquence de bits - des ensembles de zéros et de uns (cellules "mortes" et "vivantes"). Les types existent pour les gens, pas pour les voitures.

Chers lecteurs! Quel type de système pourriez-vous considérer comme idéal pour le développement Web?