Tipos universales y existenciales

Estoy tratando de entender los conceptos de tipos universales y existenciales, pero en todas partes veo intuiciones lógicas u operativas (o implementaciones) (por ejemplo, el libro TAPL de B. Pierce), que, bueno ... es bueno , pero me gustaría ver las definiciones (donde las vemos como conjuntos), y de ellas, derivaciones de algunas leyes, así como justificaciones para nuestras intuiciones.

Entonces, como no puedo encontrar esas definiciones, decidí hacerlo yo mismo y creo que pueden ser razonables:

∃ x . T d e f : = ⋃ S - t y p e T [ x : = S

$$\forall x.T \overset{def}{:=} \bigcap_{S - type} T[x := S]$$ $$\exists x.T \overset{def}{:=} \bigcup_{S - type} T[x := S]$$

Pero, en el libro TAPL mencionado anteriormente, se nos da esta definición (aunque yo lo llamaría una identidad)

$$\exists x.T \overset{def}{:=} \forall y. (\forall x. T \rightarrow y) \rightarrow y \quad (*)$$

Tengo dos problemas con esto:

1. En el LHS de esperaría que x fuera la única variable libre de T (porque ¿cómo ver un tipo "aún no construido" con algunas variables libres colgando en él?), Pero en el RHS parece que y puede tener algún impacto en T , por lo que es mejor que sea una variable libre en T . Por lo tanto, LHS no puede ser igual a RHS porque los conjuntos de variables libres de T difieren en ambos lados, ¿verdad?$(*)$$x$$T$$y$$T$$T$$T$
2. Incluso sin tener en cuenta la preocupación en el punto 1. - Traté de reescribir RHS usando mis definiciones y ver si puedo obtener mi definición de tipo existencial pero me quedé: $$RHS = \bigcap_{S} (\forall x.T \rightarrow y)[y := S] \rightarrow S = \bigcap_{S} \left(\bigcap_{R} T[x := R, y := S] \rightarrow S\right) \rightarrow S$$

Ni siquiera se parece remotamente a mi definición. ¿Es posible simplificar la fórmula a la que llegué? Intuitivamente, debido a que hay tipos de funciones, probablemente nunca será igual a mi definición. Pero si no son iguales, ¿son al menos 'isomórficos' en algún sentido? Si no, ¿qué "salió mal"?

La teoría de conjuntos te está haciendo daño aquí y cuanto antes te liberes de ella, mejor será para tu comprensión de la informática.

Olvídate de las intersecciones y uniones. La gente tiene la idea de que y ∃ son como ⋂ y ⋃ , que es el tipo de cosas que la escuela polaca estaba haciendo hace mucho tiempo con álgebras booleanas, pero realmente no es el camino a seguir (definitivamente no en informática).$\forall$$\exists$$\bigcap$$\bigcup$

Te gustaría verlos como conjuntos. Ok, pero luego tenemos que ignorar los problemas de tamaño y pretender que hay un conjunto de todos los conjuntos. (Es posible solucionar los problemas de tamaño pasando a una categoría diferente). El tipo es realmente como el producto cartesiano ∀ X . T : = ∏ S : S e t T [ X ↦ S ] . Es decir, un elemento de ∀ X . T es una función f de conjuntos a conjuntos: para cada conjunto S da un elemento$\forall x . T$

$$\forall X . T \mathrel{{:}{=}} \prod_{S : \mathsf{Set}} T[X \mapsto S].$$ $\forall X . T$ $f$$S$ de tipo T [ x ↦ S ] . Por ejemplo, un elemento de ∀ X . ( X → X ) → ( X → X ) es una función f que toma un conjunto S y proporciona una función de tipo ( S → S ) → ( S → S ) . Estas son algunas de esas funciones: f 0 ( S ) ( g ) $f(S)$$T[x \mapsto S]$$\forall X. (X \to X) \to (X \to X)$$f$$S$$(S \to S) \to (S \to S)$ Así que obtenemos uno para cada número natural, y es difícil pensar en otros ejemplos. (Ejercicio: google "Codificación de la iglesia de números naturales".) $$\begin{align*} f_0(S)(g)(x) &\mathrel{{:}{=}} x \\ f_1(S)(g)(x) &\mathrel{{:}{=}} g(x) \\ f_2(S)(g)(x) &\mathrel{{:}{=}} g(g(x)) \\ f_3(S)(g)(x) &\mathrel{{:}{=}} g(g(g(x))) \end{align*}$$

$\exists$$\forall$

$$\exists X . T \mathrel{{:}{=}} \forall Y . (\forall X . (T \to Y)) \to Y$$ $Y$$T$$\exists X . T$ $$\exists X . T \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S].$$ $\exists X . T$ $(S, a)$$S$$a$$T[X \mapsto S]$$\exists X . (X \times X \to X)$$(S, m)$$S$$m : S \times S \to S$

$\exists$$\forall$$\exists X. T$$\forall Y . (\forall X . (T \to Y)) \to Y$$Y$

$$A \mathrel{{:}{=}} \coprod_{S : \mathsf{Set}} T[X \mapsto S]$$ $$B \mathrel{{:}{=}} \prod_{R : \mathsf{Set}} \left(\prod_{S : \mathsf{Set}} (T[X \mapsto S] \to R) \right) \to R.$$ $\lambda$$f : A \to B$ $$f(S,a)(R)(h) \mathrel{{:}{=}} h(S)(a)$$ $g : B \to A$ $$g(\phi) \mathrel{{:}{=}} \phi(A)(\lambda S . \lambda a . (S, a)).$$ $\lambda S . \lambda a . (S, a)$$S \mapsto a \mapsto (S, a)$$f$$g$ $$g(f(S,a)) = f(S,a)(A)(\lambda S' . \lambda a' . (S', a')) = (\lambda S' . \lambda a' . (S', a')(S)(a) = (S, a).$$ $$f(g(\phi))(R)(h) = h(\pi_1(g(\phi))(\pi_2(g(\phi))).$$ $g(\phi)$$\phi(A)(\lambda S . \lambda a . (S, a))$

$\exists$$\forall$

$$\exists x . \phi(x)$$ $$\forall{P : \mathsf{Prop}} . (\forall x . (\phi(x) \Rightarrow P)) \Rightarrow P,$$ $P$$P$$\phi$

$Y$ $Y$$Y$$T$$\exists T$

$$((\forall x. T\rightarrow U_0)\rightarrow U_0)\wedge((\forall x. T\rightarrow U_1)\rightarrow U_1)\wedge\ldots$$ $U_i$$U$ $$\exists x.T \rightarrow ((\forall x. T\rightarrow U)\rightarrow U)$$

En palabras:

$x$$T(x)$$U$ $x$$T(x)$$U$

$U$$x$

$U$

$\bigcap_S A(S)$$A(\varnothing)$

$$\left(\bigcap_R \left(T[x:=R]\rightarrow \varnothing\right)\right)\rightarrow\varnothing$$

$R$$T[x:=R]\rightarrow \varnothing$$T[x:=R]$

Sugiero no renunciar a la intuición operativa. La operativa es primaria, toda la semántica se deriva y no son más que técnicas de prueba para la semántica operativa. Las ideas clave son las siguientes.

$P$$x$ $P$$x$$x$$\lambda$

• $\lambda x.x.$
• $\lambda (x,y,z). (z,x, y)$
• $\lambda x.(x,x)$
• $\lambda x.7$

$P$$x$ $P$$x$$x$$P$$x$$x$

$\lambda$