¿Por qué dos puntos denotan que un valor pertenece a un tipo?

Pierce (2002) introduce la relación de mecanografía en la página 92 ​​escribiendo:

La relación de escritura para expresiones aritméticas, escrita "t: T", se define mediante un conjunto de reglas de inferencia que asignan tipos a términos

y la nota al pie de página dice que el símbolo se usa a menudo en lugar de:. Mi pregunta es simplemente por qué los teóricos de tipos prefieren usar: over ? Si un tipo es un conjunto de valores, entonces tiene mucho sentido escribir , no se necesita una nueva notación.$\in$$\in$$T$$t \in T$

¿Es esto similar a cómo algunos escritores de cs prefieren incluso si piensan que es abuso de notación y deberían escribirse ?$3n^2 = O(n^2)$$3n^2 \in O(n^2)$

Porque lo que está a la derecha del colon no es necesariamente un conjunto y lo que está a la izquierda del colon no es necesariamente un miembro de ese conjunto.

La teoría de tipos comenzó a principios del siglo XX como una aproximación a los fundamentos de las matemáticas. Bertrand Russel descubrió una paradoja en la ingenua teoría de conjuntos, y trabajó en la teoría de tipos como una forma de limitar el poder expresivo de la teoría de conjuntos para evitar esta (y cualquier otra) paradoja. Con los años, Russel y otros han definido muchas teorías de tipos. En algunas teorías de tipos, los tipos son conjuntos con ciertas propiedades, pero en otros, son un tipo diferente de bestia.

En particular, muchas teorías de tipos tienen una formulación sintáctica . Hay reglas que hacen que una cosa tenga un tipo. Cuando las reglas de mecanografía se usan como base para una teoría, es importante distinguir lo que dicen las reglas de mecanografía de lo que se podría inferir aplicando conocimiento externo adicional. Esto es especialmente importante si las reglas de mecanografía son una base para una teoría de prueba: los teoremas basados ​​en la teoría de conjuntos con lógica clásica y el axioma de elección pueden o no mantenerse en una lógica constructiva, por ejemplo. Uno de los trabajos pioneros en este campo es la Iglesia 's Una formulación de la teoría simple de Tipos (1940)

Quizás la forma en que la distinción entre tipos y conjuntos es más evidente es que la regla más básica para los conjuntos, a saber, que dos conjuntos son iguales si tienen los mismos elementos, generalmente no se aplica a los tipos. Vea la respuesta de Andrej Bauer aquí y su respuesta en una pregunta relacionada para algunos ejemplos. Ese segundo hilo tiene otras respuestas que vale la pena leer.

En un cálculo con tipo, decir que los tipos son conjuntos es, de hecho, dar una semántica a los tipos. Darle a un cálculo una semántica de tipo teórico no es trivial. Por ejemplo, suponga que está definiendo un lenguaje con funciones. ¿Qué conjunto es un tipo de función? Las funciones totales están determinadas por su gráfica, como se nos enseña en la teoría de conjuntos 101. Pero ¿qué pasa con las funciones parciales? ¿Desea dar a todas las funciones no terminantes la misma semántica? No puede interpretar los tipos como conjuntos para un cálculo que permite funciones recursivas hasta que haya respondido esa pregunta. Darle a los lenguajes de programación o cálculos una semántica denotacional fue un problema difícil a principios de los años setenta. El artículo fundamental aquí es Hacia una semántica matemática para lenguajes de computadora (1971) porDana Scott y Christopher Strachey . El wikibook de Haskell tiene una buena presentación del tema.

Como escribí anteriormente, una segunda parte de la respuesta es que, incluso si ha logrado darles a los tipos una semántica de conjunto teórico, lo que está a la izquierda del colon no siempre es un elemento del conjunto. Los valores tienen tipos, pero también lo hacen otras cosas, como expresiones y variables . Por ejemplo, una expresión en un lenguaje de programación escrito tiene un tipo incluso si no termina. Es posible que esté dispuesto a confundir integery $\mathbb{Z}$ , pero (x := 0; while true; do x := x + 1; x)no es un elemento de $\mathbb{Z}$ .

No sé cuándo surgió la notación de colon para los tipos. Ahora es estándar en semántica y común en lenguajes de programación, pero ni Russel ni Church lo usaron. Algol no lo usó, pero el lenguaje fuertemente inspirado en Algol que Pascal hizo en 1971. Sin embargo, sospecho que no fue el primero, porque muchos documentos teóricos de principios de la década de 1970 usan la notación, pero no sé de un uso anterior Curiosamente, esto fue poco después de que los conceptos de tipos de programación y de lógica se unificaron, como lo demuestra Simon Martini en Varios tipos de tipos en lenguajes de programación , lo que se llamó un "tipo" en lenguajes de programación hasta la década de 1960 provino de la lengua vernácula uso de la palabra y no de la teoría de tipos.

La razón principal para preferir la notación de dos puntos $t : T$ a la relación de membresía $t \in T$ es que la relación de membresía puede ser engañosa porque los tipos no son (solo) colecciones .

[ Complementario: Debo señalar que históricamente la teoría de tipos se escribió usando $\in$ . La concepción del tipo de Martin-Löf estaba destinada a capturar conjuntos de manera constructiva, y Russell y Whitehead ya usaban $\epsilon$ para la membresía de la clase. Sería interesante rastrear el momento en que $:$ hizo más frecuente que $\in$ .]

Un tipo describe un cierto tipo de construcción, es decir, cómo hacer objetos con una determinada estructura, cómo usarlos y qué ecuaciones tienen sobre ellos.

Por ejemplo, un tipo de producto $A \times B$ tiene reglas de introducción que explican cómo hacer pares ordenados, y reglas de eliminación explicando que podemos proyectar el primer y el segundo componente de cualquier elemento de $A \times B$ . La definición de $A \times B$ no no comienza con las palabras "la colección de todos ..." y tampoco dice en ninguna parte nada por el estilo "todos los elementos de $A \times B$ son pares" (pero que sigue de la definición que cada elemento de $A \times B$ es proposicionalmenteigual a un par). En contraste, la definición teórica de conjuntos de $X \times Y$ se establece como "el conjunto de todos los pares ordenados ...".

La notación $t : T$ significa el hecho de que $t$ tiene la estructura descrita por $T$ .

Un tipo $T$ no se debe confundirse con su extensión , que es la colección de todos los objetos de tipo $T$ . Un tipo no está determinado por su extensión, al igual que un grupo no está determinado por su conjunto de portadores. Además, puede suceder que dos tipos tengan la misma extensión, pero son diferentes, por ejemplo:

1. El tipo de todos los primos pares mayores que dos: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{iseven}(n) \times (n > 2)$ .
2. El tipo de todos los números primos impares menores que dos: $\Sigma (n : \mathbb{N}) . \mathtt{isprime}(n) \times \mathtt{isodd}(n) \times (n < 2)$ .

La extensión de ambos está vacía, pero no son del mismo tipo.

Existen otras diferencias entre el tipo teórico $:$ y el conjunto teórico $\in$ . Un objeto $a$ en la teoría de conjuntos existe independientemente de a qué conjuntos pertenece, y puede pertenecer a varios conjuntos. En contraste, la mayoría de las teorías de tipo satisfacen singularidad de escribir: si $t : T$ y $t : U$ entonces $T \equiv U$ . O para decirlo de otra manera, una construcción teórica de tipo $t$ tiene precisamente un tipo $T$ , y de hecho no hay forma de tener solo un objeto $t$ sin su tipo (determinado de forma única).

Otra diferencia es que en la teoría de conjuntos podemos negar el hecho de que $a \in A$ por la escritura $\lnot (a \in A)$ o $a \not\in A$ . Esto no es posible en la teoría de tipos, porque $t : T$ es un juicio que puede derivarse usando las reglas de la teoría de tipos, pero no hay nada en la teoría de tipos que nos permita afirmar que algo no se ha derivado. Cuando un niño hace algo con bloques LEGO, corren orgullosamente hacia sus padres para mostrarles la construcción, pero nunca corren hacia sus padres para mostrarles lo que no hicieron.

Björn

Probablemente haya una referencia anterior, pero por un lado, los dos puntos se usaron en el lenguaje de programación Pascal: