Qu'est-ce qu'un système de type?

50

Contexte

Je conçois une langue, en tant que projet parallèle. J'ai un assembleur, un analyseur statique et une machine virtuelle en état de marche. Comme je peux déjà compiler et exécuter des programmes non triviaux en utilisant l'infrastructure que j'ai construite, j'ai pensé à faire une présentation à mon université.

Au cours de mon exposé, j'ai mentionné que la machine virtuelle fournit un système de types. On m'a demandé "À quoi sert votre système de types? ". Après avoir répondu, la personne qui me posait la question se moquait de moi.

Ainsi, même si je vais certainement perdre la réputation de poser cette question, je me tourne vers les programmeurs.

Ma compréhension

D'après ce que je comprends, les systèmes de types fournissent une couche d'informations supplémentaire sur les entités d'un programme, de sorte que le moteur d'exécution, le compilateur ou toute autre machine sache quoi faire avec les chaînes de bits sur lesquelles il opère. Ils aident également à maintenir les contrats - le compilateur (ou l'analyseur de code, ou l'exécution, ou tout autre programme) peut vérifier qu'à tout moment, le programme fonctionne sur des valeurs que les programmeurs s'attendent à ce qu'il opère.

Les types peuvent également être utilisés pour fournir des informations à ces programmeurs humains. Par exemple, je trouve cette déclaration:

function sqrt(double n) -> double;

plus utile que celui-ci

sqrt(n)

Le premier donne beaucoup d'informations: que l' sqrtidentifiant est une fonction, prend un simple doubleen entrée et en produit un autre doubleen sortie. Ce dernier vous dit que c'est probablement une fonction prenant un seul paramètre.

Ma réponse

Donc, après avoir demandé "Quel est votre système de type?" J'ai répondu comme suit:

Le système de types est dynamique (les types sont affectés à des valeurs et non à des variables les contenant), mais ils sont forts sans règles de coercition surprenantes (vous ne pouvez pas ajouter de chaîne à un entier car ils représentent des types incompatibles, mais vous pouvez ajouter un entier à un nombre à virgule flottante). .

Le système de types est utilisé par la machine virtuelle pour s'assurer que les opérandes des instructions sont valides. et peuvent être utilisés par les programmeurs pour s'assurer que les paramètres transmis à leurs fonctions sont valides (c'est-à-dire du type correct).
Le système de types prend en charge le sous-typage et l'héritage multiple (les deux fonctionnalités sont disponibles pour les programmeurs). Les types sont pris en compte lors de l'utilisation de la répartition dynamique de méthodes sur des objets.

La question suivante était "Et comment le type est-il affecté à une valeur?". J'ai donc expliqué que toutes les valeurs sont encadrées et que le pointeur pointe vers une structure de définition de type qui fournit des informations sur le nom du type, les messages auxquels il répond et les types dont il hérite.

Après cela, je me suis moqué de moi et ma réponse a été rejetée avec le commentaire "Ce n'est pas un vrai système de typage.".

Donc, si ce que je décris ne peut pas être qualifié de "système de types réel", que ferait-on? Cette personne a-t-elle raison de penser que ce que je fournis ne peut pas être considéré comme un système de types?

Mael
la source
19
Lorsque les gens parlent de systèmes de types, ils parlent généralement de typage statique. Le typage dynamique n’intéresse guère les types de personnes soucieux des systèmes de typage car il ne garantit presque rien. Par exemple, quel type de valeur la variable x peut-elle contenir? N'importe quoi.
Doval
7
Je serais curieux d'entendre ce qu'ils ont à dire pour défendre / expliquer leur réaction.
Newtopian
18
@Doval La saisie dynamique peut vous éviter de passer à un état absurde en ajoutant 5 à votre chat. Bien sûr, cela ne vous empêchera pas d’ essayer , mais cela peut au moins l’empêcher de se produire et vous donner une chance de comprendre ce qui n’a pas fonctionné et de prendre des mesures correctives, ce qu’une langue vraiment sans typage ne peut pas.
8bittree
10
La personne a contesté votre réponse à "Et comment le type est-il affecté à une valeur?". Ils voulaient en savoir plus sur les règles de dactylographie et non sur les diagrammes à boîtes et à pointeurs. Rire était absolument impoli, cependant.
Gardenhead
10
La personne qui rit est très probablement fanatique d’une langue particulière (famille) avec un système de caractères fort (Haskell semble populaire), et ridiculiserait tout ce qui est moins fort (et donc un jouet) que celui-là, ou plus fort (et donc impraticable), ou juste différent. S'engager dans des discussions avec des fanatiques est dangereux et futile. Rire comme ça est tellement impoli que cela indique ce genre de problèmes plus profonds. Tu as de la chance qu'ils n'aient pas commencé à prêcher ...
Hyde

Réponses:

30

Tout cela semble être une description détaillée de ce que fournissent les systèmes de types. Et votre implémentation semble assez raisonnable pour ce qu’elle fait.

Pour certaines langues, vous n’avez pas besoin des informations d’exécution, car votre langue n’effectue pas la répartition à l’application (ou une distribution unique via vtables ou un autre mécanisme, vous n'avez donc pas besoin des informations de type). Pour certaines langues, il suffit de disposer d'un symbole / d'un espace réservé, car vous vous souciez uniquement de l'égalité de type, pas de son nom ni de son héritage.

En fonction de votre environnement, la personne peut avoir souhaité plus de formalisme dans votre système de typage. Ils veulent savoir ce que vous pouvez prouver avec cela, pas ce que les programmeurs peuvent en faire . C'est assez commun dans le monde universitaire malheureusement. Bien que les universitaires fassent de telles choses parce qu’il est assez facile d’avoir des failles dans votre système de typographie qui permettent aux choses d’échapper à la correction. Il est possible qu'ils en aient repéré un.

Si vous avez d'autres questions, Types and Programming Languages est l'ouvrage canonique sur le sujet et peut vous aider à apprendre la rigueur dont ont besoin les universitaires, ainsi que la terminologie utilisée pour décrire les éléments.

Telastyn
la source
3
"En fonction de votre environnement, la personne peut avoir souhaité plus de formalisme dans votre système de typage." C'est probablement ça. Je ne me suis pas concentré sur ce que je pouvais prouver avec le système de typage, mais je le considérais plutôt comme un outil. Merci pour la recommandation de livre!
Mael
1
@Mael Certains systèmes de type sont utilisés comme logiques (voir les frameworks logiques ). Donc, fondamentalement, le type donne les formules et les programmes sont les preuves de ces formules (par exemple, le type de fonction a -> bpeut être vu comme un implique b , c'est-à-dire que si vous me donnez une valeur de type aI, vous pouvez obtenir une valeur de type b). Cependant, pour que cela soit cohérent, le langage doit être total, et donc non complet de Turing. Ainsi, tous les systèmes de types réels définissent en réalité une logique incohérente.
Bakuriu
20

J'aime la réponse de @Telastyn en particulier en raison de la référence à l'intérêt académique pour le formalisme.

Permettez-moi d’ajouter à la discussion.

Qu'est-ce qu'un système de type?

Un système de types est un mécanisme permettant de définir, détecter et prévenir les états de programme illégaux. Cela fonctionne en définissant et en appliquant des contraintes. Les définitions de contrainte sont des types et les applications de contrainte sont des utilisations de types , par exemple dans une déclaration de variable.

Les définitions de types prennent généralement en charge les opérateurs de composition (par exemple, diverses formes de conjonction, telles que des structures, des sous-classes et une disjonction, telles que des énumérations, des unions).

Les contraintes, les usages des types, permettent parfois aussi des opérateurs de composition (par exemple, au moins ceci, exactement ceci, ceci ou cela, à condition que quelque chose d'autre soit valable).

Si le système de types est disponible dans le langage et appliqué au moment de la compilation afin de pouvoir générer des erreurs de compilation, il s'agit d'un système de types statique; Cela empêche beaucoup de programmes illégaux de compiler et encore moins d’exécuter, ce qui empêche les états de programmes illégaux.

(Un système de types statiques empêche un programme de s'exécuter, qu'il soit ou non connu (ou indécidable) qu'il atteindra jamais le code peu sain dont il se plaint. Un système de types statiques détecte certains types de non-sens (violations des contraintes déclarées) et juge le programme par erreur avant qu'il ne soit exécuté.)

Si un système de types est appliqué à l'exécution, il s'agit d'un système de types dynamique qui empêche les états de programme illégaux: mais en arrêtant le programme à mi-parcours, au lieu de l'empêcher de s'exécuter en premier lieu.

Une offre de système de type assez courante consiste à fournir des fonctionnalités statiques et dynamiques.

Erik Eidt
la source
Je ne pense pas que les systèmes de type hybride soient très répandus. Quelles langues as-tu en tête?
Gardenhead
2
@gardenhead, la possibilité de procéder au downcast n'est pas une fonctionnalité système de type statique, elle est donc généralement vérifiée de manière dynamique au moment de l'exécution.
Erik Eidt
1
@gardenhead: la plupart des langages à typage statique vous permettent de différer le typage en exécution, que ce soit simplement avec les void *pointeurs de C (très faibles), les objets dynamiques de C # ou les GADT de Haskell quantifiés de manière existentielle (ce qui vous donne des garanties plus fortes que les valeurs statiquement typées de la plupart des autres). langues).
gauche du
Certes, j'ai oublié de "casting". Mais le casting n’est qu’une béquille pour un système de type faible.
Gardenhead
@gardenhead En plus des langages statiques offrant des options dynamiques, de nombreux langages dynamiques fournissent du typage statique. Par exemple, Dart, Python et Hack disposent tous de modes ou d’outils permettant d’effectuer des analyses statiques basées sur le concept de "typage progressif".
IMSoP
14

Oh mec, je suis excité d'essayer de répondre à cette question du mieux que je peux. J'espère que je peux mettre mes pensées en ordre correctement.

Comme @Doval et le questionneur l'ont fait remarquer (bien que de manière grossière), vous n'avez pas vraiment de système de type. Vous avez un système de contrôles dynamiques utilisant des balises, qui est en général beaucoup plus faible et aussi beaucoup moins intéressant.

La question de "qu'est-ce qu'un système de types" peut être assez philosophique, et nous pourrions remplir un livre avec différents points de vue sur le sujet. Cependant, comme il s’agit d’un site pour les programmeurs, je vais essayer de garder ma réponse aussi pratique que possible (et en réalité, les types sont extrêmement pratiques en programmation, malgré ce que certains pourraient penser).

Vue d'ensemble

Commençons par un siège-du-pantalon et comprenons à quoi sert un système de types, avant de plonger dans les bases plus formelles. Un système de types impose une structure à nos programmes . Ils nous disent comment nous pouvons associer différentes fonctions et expressions. Sans structure, les programmes sont intenables et extrêmement complexes, prêts à causer des dommages à la moindre erreur du programmeur.

Écrire des programmes avec un système de types revient à conduire prudemment à l’état neuf: les freins fonctionnent, les portes se ferment en toute sécurité, le moteur est huilé, etc. en spaghettis. Vous n'avez absolument aucun contrôle sur votre.

Pour fonder la discussion, disons que nous avons un langage avec une expression littérale num[n]et str[s]qui représente le nombre n et la chaîne s, respectivement, et des fonctions primitives pluset concat, avec le sens voulu. Clairement, vous ne voulez pas pouvoir écrire quelque chose comme plus "hello" "world"ou concat 2 4. Mais comment pouvons-nous empêcher cela? A priori , il n’existe aucune méthode permettant de distinguer le chiffre 2 du littéral de chaîne "world". Ce que nous voudrions dire, c’est que ces expressions devraient être utilisées dans différents contextes; ils ont différents types.

Langues et types

Revenons un peu en arrière: qu'est-ce qu'un langage de programmation? En général, on peut diviser un langage de programmation en deux couches: la syntaxe et la sémantique. Celles-ci sont également appelées la statique et la dynamique , respectivement. Il s'avère que le système de types est nécessaire pour assurer la médiation de l'interaction entre ces deux parties.

Syntaxe

Un programme est un arbre. Ne vous laissez pas berner par les lignes de texte que vous écrivez sur un ordinateur; Ce ne sont que les représentations lisibles par un programme. Le programme lui-même est un arbre de syntaxe abstraite . Par exemple, en C, nous pourrions écrire:

int square(int x) { 
    return x * x;
 }

C'est la syntaxe concrète du programme (fragment). L'arborescence est:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

Un langage de programmation fournit une grammaire définissant les arbres valides de ce langage (une syntaxe concrète ou abstraite peut être utilisée). Ceci est généralement fait en utilisant quelque chose comme la notation BNF. Je suppose que vous avez fait cela pour la langue que vous avez créée.

Sémantique

Bien, nous savons ce qu’est un programme, mais c’est juste une arborescence statique. Vraisemblablement, nous voulons que notre programme calcule réellement quelque chose. Nous avons besoin de sémantique.

La sémantique des langages de programmation est un domaine d'étude riche. De manière générale, il existe deux approches: la sémantique dénotationnelle et la sémantique opérationnelle . La sémantique dénotationnelle décrit un programme en le mappant dans une structure mathématique sous-jacente (par exemple, les nombres naturels, les fonctions continues, etc.). cela donne un sens à notre programme. La sémantique opérationnelle, au contraire, définit un programme en détaillant son exécution. À mon avis, la sémantique opérationnelle est plus intuitive pour les programmeurs (y compris moi-même), alors restons avec cela.

Je ne vais pas vous expliquer comment définir une sémantique opérationnelle formelle (les détails sont un peu compliqués), mais au fond, nous voulons des règles comme celles-ci:

  1. num[n] est une valeur
  2. str[s] est une valeur
  3. Si num[n1]et num[n2]évalue les entiers n_1$ and $n_2$, thenplus (num [n1], num [n2]) `correspond à l'entier $ n_1 + n_2 $.
  4. Si str[s1]et str[s2]évalue les chaînes s1 et s2, alors concat(str[s1], str[s2])évalue la chaîne s1s2.

Etc. Les règles sont en pratique beaucoup plus formelles, mais vous comprenez l'essentiel. Cependant, nous rencontrons rapidement un problème. Que se passe-t-il lorsque nous écrivons ce qui suit:

concat(num[5], str[hello])

Hm. C'est tout à fait une énigme. Nous n'avons défini nulle part la règle pour concaténer un nombre avec une chaîne. Nous pourrions essayer de créer une telle règle, mais nous savons intuitivement que cette opération n'a pas de sens. Nous ne voulons pas que ce programme soit valide. Et ainsi nous sommes inexorablement conduits aux types.

Les types

Un programme est un arbre tel que défini par la grammaire d'une langue. Les programmes ont une signification grâce aux règles d'exécution. Mais certains programmes ne peuvent pas être exécutés. c'est-à-dire que certains programmes n'ont aucun sens . Ces programmes sont mal typés. Ainsi, la frappe caractérise des programmes significatifs dans une langue. Si un programme est bien typé, nous pouvons l'exécuter.

Donnons quelques exemples. De nouveau, comme pour les règles d’évaluation, je présenterai les règles de dactylographie de manière informelle, mais elles peuvent être rigoureuses. Voici quelques règles:

  1. Un jeton de la forme num[n]a le type nat.
  2. Un jeton de la forme str[s]a le type str.
  3. Si expression e1a le type natet expression e2a le type nat, l'expression plus(e1, e2)a le type nat.
  4. Si expression e1a le type stret expression e2a le type str, alors expression concat(e1, e2)a le type str.

Ainsi, selon ces règles, il y plus(num[5], num[2])a a type nat, mais nous ne pouvons pas affecter un type à plus(num[5], str["hello"]). Nous disons qu'un programme (ou une expression) est bien typé si nous pouvons lui attribuer n'importe quel type, et sinon, il est mal typé. Un système de type est sain si tous les programmes bien typés peuvent être exécutés. Haskell est sain; C n'est pas.

Conclusion

Il existe d'autres points de vue sur les types. Les types, dans un certain sens, correspondent à la logique intuitionniste et peuvent également être considérés comme des objets dans la théorie des catégories. Comprendre ces connexions est fascinant, mais ce n’est pas essentiel si l’on veut simplement écrire ou même concevoir un langage de programmation. Cependant, la compréhension des types en tant qu'outil de contrôle des formations de programme est essentielle pour la conception et le développement de langages de programmation. Je n'ai fait qu'effleurer la surface de ce que les types peuvent exprimer. J'espère que vous pensez qu'ils valent la peine d'être incorporés dans votre langue.

tête de jardin
la source
4
+1 Le plus grand truc que les passionnés de dactylographie dynamiques aient fait est de convaincre le monde que vous pouvez avoir des "types" sans système de frappe. :-)
ruakh
1
Etant donné que vous ne pouvez pas vérifier automatiquement quoi que ce soit d'intéressant pour des programmes arbitraires, chaque système de types doit fournir un opérateur de transtypage (ou son équivalent moral), sinon il sacrifie la complétude de Turing. Cela comprend Haskell , bien sûr.
Kevin
1
@ Kevin Je connais bien le théorème de Rice, mais il n'est pas aussi pertinent que vous le pourriez. Pour commencer, une grande majorité de programmes ne nécessite pas de récursion sans limite. Si nous travaillons dans un langage ne comportant qu'une récursivité primitive, tel que le système T de Godel, nous pouvons alors vérifier les propriétés intéressantes à l'aide d'un système de types, y compris en arrêtant. La plupart des programmes dans le monde réel sont plutôt simples - je ne peux pas penser à la dernière fois où j'avais réellement besoin d'un casting. Cette complétude est surestimée.
Gardenhead
9
«La dactylographie dynamique n'est pas vraiment la dactylographie» m'a toujours semblé comme des musiciens classiques disant «La musique pop n'est pas vraiment de la musique», ou évangéliques comme «Les catholiques ne sont pas vraiment des chrétiens». Oui, les systèmes de types statiques sont puissants, fascinants et importants, et le typage dynamique est quelque chose de différent. Mais (comme d’autres réponses le décrivent), il existe toute une série de choses utiles, au-delà des systèmes de types statiques, traditionnellement appelés typage, qui partagent toutes des points communs importants. Pourquoi avoir besoin d'insister sur le fait que notre type de dactylographie est le seul vrai typage?
Peter LeFanu Lumsdaine
5
@IMSoP: pour quelque chose de plus court qu'un livre, l'essai de Chris Smith Ce qu'il faut savoir avant de débattre des systèmes de caractères est formidable. Il explique pourquoi la frappe dynamique est vraiment très différente de la frappe statique.
Peter LeFanu Lumsdaine