Sistema de tipos basado en la teoría de conjuntos ingenua

Según tengo entendido, en informática los tipos de datos no se basan en la teoría de conjuntos debido a cosas como la paradoja de Russell, pero como en los lenguajes de programación del mundo real no podemos expresar tipos de datos tan complejos como "conjunto que no se contiene a sí mismo", ¿podemos? ¿Digamos que en la práctica el tipo es un conjunto infinito de sus miembros donde la pertenencia a la instancia se define por el número de características que son intrínsecas a este tipo / conjunto (existencia de ciertas propiedades, métodos)? Si no, ¿cuál sería el contraejemplo?

type-theory set-theory type-systems Nutel
fuente

La paradoja de Russell no tiene nada que ver directamente con eso.

Andrej Bauer

Respuestas:

La razón principal para evitar conjuntos en la semántica de tipos es que un lenguaje de programación típico nos permite definir funciones recursivas arbitrarias. Por lo tanto, cualquiera que sea el significado de un tipo, debe tener la propiedad de punto fijo. El único conjunto con dicha propiedad es el conjunto singleton.

$v$ $\tau$ $\tau$ $v = \Phi(v)$ $\Phi : \tau \to \tau$ $\tau$ $T$ $f : T \to T$ $T$

Por supuesto, también podría darse cuenta de que el culpable es la lógica clásica. Si trabaja con la teoría intuitiva de conjuntos, entonces es consistente asumir que hay muchos conjuntos con propiedades de punto fijo. De hecho, esto se ha utilizado para dar semántica del lenguaje de programación, ver por ejemplo

Alex Simpson, Adecuación computacional para tipos recursivos en modelos de teoría de conjuntos intuicionistas , en Annals of Pure and Applic Logic, 130: 207-275, 2004.

Andrej Bauer
fuente

$\pi$

Dave Clarke
fuente

Hay precursores de Castagna. Hace mucho tiempo, la gente ya usaba la relación de subconjunto para modelar subtipos en modelos PER. Allí, un tipo corresponde a una relación de equivalencia parcial (PER) y el subtipo es solo la inclusión de tales relaciones.

Andrej Bauer

Con algunas excepciones (una que cita Dave Clarke), la semántica de tipos simple de teoría de conjuntos es difícil de usar. La razón es que la abstracción de datos no juega muy bien con la semántica de la teoría de conjuntos.

$\forall \alpha.\; \alpha \to \alpha$ $U$

[[\forall α . α \to α]] = Π X \in U . X \to X

$[\![\forall \alpha.\; \alpha \to \alpha]\!] = \Pi X \in \mathrm{U}.\;X \to X$

$U$ $U$ $X \to X$ $X \in U$ $\alpha$

$\forall \alpha.\; \alpha \to \alpha$

Neel Krishnaswami
fuente

Neel, no creo que esta respuesta tenga sentido. Si la semántica del lenguaje es la semántica estándar de estilo F, entonces un compilador podría hacer la optimización perfectamente, en función del sistema de tipos. Si la semántica es la semántica de la teoría de conjuntos, entonces la optimización sería poco sólida. El modelo que usa para los tipos no entra en él.

Sam Tobin-Hochstadt

Sam, no entiendo tu punto: ¡se lee como si estuvieras completamente de acuerdo conmigo! La semántica de la teoría de conjuntos estándar no puede demostrar que el único habitante de ese tipo es la identidad, por lo que necesita una semántica diferente.

Neel Krishnaswami

@Neel: el problema que describe persiste incluso cuando nos alejamos de los conjuntos. La solución no es cambiar la categoría de conjuntos con otra cosa, sino modelar la parametricidad de manera diferente. A saber, uno tiene que usar la parametricidad relacional , como estoy seguro de que usted sabe. Pero entonces las cosas también funcionan en sets, si no me equivoco. El "único" problema con los conjuntos es la falta de puntos fijos (tanto a nivel de valores recursivos como de tipos recursivos).

Andrej Bauer

¡Ah, creo que entiendo por qué te estoy confundiendo a ti y a Sam! Ciertamente no quiero decir que sea un error usar un modelo ingenuo de teoría de conjuntos, solo que este modelo a menudo da respuestas inútiles, por eso dije "difícil de usar" y no "incorrecto". Por supuesto, puede usar conjuntos para construir un modelo útil (es decir, relacionalmente), pero ya no estamos interpretando los tipos como conjuntos de la manera sugerida en la pregunta. (Además, como saben, con el polimorfismo impredicativo no existe un modelo ingenuo, pero la parametricidad sigue siendo significativa de manera predicativa).

Neel Krishnaswami

Creo que su punto es sobre la correspondencia entre la semántica: una semántica de teoría de conjuntos no es una buena opción para el polimorfismo de estilo del Sistema F, porque tiene habitantes inexpresables. Pero ese no es un punto en contra de la semántica de la teoría de conjuntos, solo una declaración de que nuestra semántica debería estar de acuerdo. Si nuestro lenguaje nos permite expresar las funciones de las que está hablando (como lo hace Typed Racket, por ejemplo), entonces podemos querer la semántica de la teoría de conjuntos.

Sam Tobin-Hochstadt