Pourquoi deux points pour indiquer qu'une valeur appartient à un type?

Pierce (2002) introduit la relation de frappe à la page 92 en écrivant:

La relation de typage pour les expressions arithmétiques, écrite "t: T", est définie par un ensemble de règles d'inférence affectant des types aux termes

et la note de bas de page indique que le symbole est souvent utilisé au lieu de:. Ma question est simplement pourquoi les théoriciens des types préfèrent utiliser: over ? Si un type est un ensemble de valeurs, il est parfaitement logique d'écrire , aucune nouvelle notation n'est nécessaire.$\in$$\in$$T$$t \in T$

Est-ce similaire à la façon dont certains auteurs cs préfèrent même s'ils pensent qu'il s'agit d'un abus de notation et devrait être écrit ?$3n^2 = O(n^2)$$3n^2 \in O(n^2)$

Parce que ce qui est à droite des deux points n'est pas nécessairement un ensemble et ce qui est à gauche des deux points n'est pas nécessairement un membre de cet ensemble.

La théorie des types a commencé au début du 20e siècle en tant qu'approche du fondement des mathématiques. Bertrand Russel a découvert un paradoxe dans la théorie naïve des ensembles, et il a travaillé sur la théorie des types comme moyen de limiter le pouvoir expressif de la théorie des ensembles pour éviter ce paradoxe (et tout autre). Au fil des ans, Russel et d'autres ont défini de nombreuses théories de types. Dans certaines théories des types, les types sont des ensembles avec certaines propriétés, mais dans d'autres, ils sont un type de bête différent.

En particulier, de nombreuses théories des types ont une formulation syntaxique . Il y a des règles qui font qu'une chose a un type. Lorsque les règles de frappe sont utilisées comme fondement d'une théorie, il est important de distinguer ce que disent les règles de frappe de ce que l'on pourrait inférer en appliquant des connaissances externes supplémentaires. Cela est particulièrement important si les règles de typage sont le fondement d'une théorie de la preuve: les théorèmes qui reposent sur une théorie des ensembles avec une logique classique et l'axiome de choix peuvent ou non tenir dans une logique constructive, par exemple. L' un des articles fondamentaux dans ce domaine est Eglise de A Formulation de la théorie simple des types (1940)

Peut-être que la manière dont la distinction entre les types et les ensembles est la plus apparente est que la règle la plus fondamentale pour les ensembles, à savoir que deux ensembles sont égaux s'ils ont les mêmes éléments, ne s'applique généralement pas aux types. Voir la réponse d'Andrej Bauer ici et sa réponse à une question connexe pour quelques exemples. Ce deuxième fil a d'autres réponses qui méritent d'être lues.

Dans un calcul typé, dire que les types sont des ensembles, c'est en fait donner une sémantique aux types. Donner à un calcul une sémantique théorique de type n'est pas trivial. Par exemple, supposons que vous définissez un langage avec des fonctions. Quel ensemble est un type de fonction? Les fonctions totales sont déterminées par leur graphique, comme nous l'avons appris dans la théorie des ensembles 101. Mais qu'en est-il des fonctions partielles? Voulez-vous donner à toutes les fonctions non terminales la même sémantique? Vous ne pouvez pas interpréter les types comme des ensembles pour un calcul qui autorise des fonctions récursives tant que vous n'avez pas répondu à cette question. Donner aux langages de programmation ou aux calculs une sémantique dénotationnelle était un problème difficile au début des années 1970. Le papier séminal ici est Vers une sémantique mathématique pour les langages informatiques (1971) parDana Scott et Christopher Strachey . Le wikibook Haskell a une bonne présentation du sujet.

Comme je l'ai écrit ci-dessus, une deuxième partie de la réponse est que même si vous avez réussi à donner aux types une sémantique théorique, la chose à gauche du deux-points n'est pas toujours un élément de l'ensemble. Les valeurs ont des types, mais il en va de même pour d'autres choses, telles que les expressions et les variables . Par exemple, une expression dans un langage de programmation typé a un type même si elle ne se termine pas. Vous pourriez être prêt à conflate integeret $\mathbb{Z}$ , mais (x := 0; while true; do x := x + 1; x)n'est pas un élément de $\mathbb{Z}$ .

Je ne sais pas quand la notation deux-points est apparue pour les types. Il est désormais standard en sémantique et commun dans les langages de programmation, mais ni Russel ni Church ne l'ont utilisé. Algol ne l'a pas utilisé, mais le langage fortement inspiré d'Algol que Pascal a utilisé en 1971. Je soupçonne que ce n'était pas le premier, cependant, parce que de nombreux articles théoriques du début des années 1970 utilisent la notation, mais je ne connais pas de utilisation antérieure. Fait intéressant, c'était peu de temps après l'unification des concepts de types issus de la programmation et de la logique - comme le montre Simon Martini dans Plusieurs types de types dans les langages de programmation , ce que l'on appelait un «type» dans les langages de programmation jusqu'aux années 1960 provenait du vernaculaire. l'utilisation du mot et non de la théorie des types.

La principale raison de préférer la notation deux points $t : T$ à la relation d'appartenance $t \in T$ est que la relation d'appartenance peut être trompeuse car les types ne sont pas (seulement) des collections .

[ Supplémentaire: Je dois noter que la théorie de type historique a été écrite en utilisant $\in$ . La conception du type de Martin-Löf visait à capturer des décors de manière constructive, et déjà Russell et Whitehead utilisaient $\epsilon$ pour le memebrship de la classe. Il serait intéressant de retrouver le moment où $:$ est devenu plus répandu que $\in$ .]

Un type décrit un certain type de construction, c'est-à-dire comment fabriquer des objets avec une certaine structure, comment les utiliser et quelles équations contiennent à leur sujet.

Par exemple , un type de produit $A \times B$ a des règles d'introduction qui expliquent comment faire couples et les règles d'élimination expliquant que nous pouvons projeter le premier et le second composants de tout élément de $A \times B$ . La définition de $A \times B$ ne commence pas par les mots "la collection de tous ..." et elle ne dit nulle part quelque chose comme "tous les éléments de $A \times B$ sont des paires" (mais il résulte de la définition que chaque élément de $A \times B$ est propositionnellementégal à une paire). En contraste, la définition théorique de $X \times Y$ est définie comme "l'ensemble de toutes les paires ordonnées ...".

La notation $t : T$ signifie le fait que $t$ a la structure décrite par $T$ .

Un type $T$ ne doit pas être confondu avec son prolongement , qui est la collection de tous les objets de type $T$ . Un type n'est pas déterminé par son extension, tout comme un groupe n'est pas déterminé par son ensemble de porteuses. De plus, il peut arriver que deux types aient la même extension, mais soient différents, par exemple:

1. Le type de tous les nombres premiers pairs supérieurs à deux: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{iseven}(n) \times (n > 2)$ .
2. Le type de tous les nombres premiers impairs inférieurs à deux: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{isodd}(n) \times (n < 2)$ .

L'extension des deux est vide, mais ce n'est pas le même type.

Il existe d'autres différences entre la théorie des types $:$ et la théorie des ensembles $\in$ . Un objet dans $a$ théorie des ensembles existe indépendamment des ensembles auxquels il appartient, et il peut appartenir à plusieurs ensembles. En revanche, la plupart des théories de type satisfont l' unicité de frappe: si $t : T$ et $t : U$ puis $T \equiv U$ . Ou, pour le dire différemment, une construction théorique de type $t$ a précisément un type $T$ , et en fait il n'y a aucun moyen d'avoir juste un objet $t$ sans son type (déterminé de manière unique).

Une autre différence est que , en théorie , ensemble nous pouvons nier le fait que $a \in A$ par écrit $\lnot (a \in A)$ ou $a \not\in A$ . Ce n'est pas possible en théorie des types, car $t : T$ est un jugement qui peut être dérivé en utilisant les règles de la théorie des types, mais rien dans la théorie des types ne nous permettrait d'affirmer que quelque chose n'a pas été dérivé. Quand un enfant fabrique quelque chose à partir de blocs LEGO, il court fièrement vers ses parents pour leur montrer la construction, mais il ne court jamais vers ses parents pour leur montrer ce qu'ils n'ont pas fait.

Björn,

Il y a probablement une référence antérieure mais pour une chose, les deux points ont été utilisés dans le langage de programmation Pascal: