¿Cuantificación universal / existencial?

Me cuesta entender el propósito de la cuantificación universal y existencial de los tipos. Estoy jugando con un lenguaje de juguete basado en el cálculo de las construcciones . He estado leyendo sobre Morte y Henk para ayudarme a comprenderlo mejor.

No entiendo por qué el CoC tiene abstracción lambda y forall.

Me parece que lambda subsume en un sistema donde los tipos se pasan manualmente. En otras palabras, que lo siguiente

Podría ser reemplazado con

Si se aplicó por primera vez al tipo que se está utilizando.

¿Qué me estoy perdiendo? ¿Qué artículos, blogs o artículos hay para leer que puedan ayudarme?

Gracias.

Es útil recordar que$\forall$ (o como a veces ves) es un tipo. Se está generalizando → . Así que si bien tiene mucho sentido decir ( λ x : A . M ) N , no tiene sentido decir ( ∀ x : A . M ) N porque ∀ . . . Es solo un tipo. No diría ( A → B ) N porque → no es para computación per-se, está ahí para$\Pi$$\to$$(\lambda x : A. M)\ N$$(\forall x : A. M)\ N$$\forall ...$$(A \to B)\ N$$\to$clasifique los términos lambda que se pueden aplicar de esta manera .

Esto fue algo que también me hizo tropezar, pero así es como se define el cálculo de las construcciones (así como cualquier otro sistema tipeado de forma dependiente).

Los dos programas que escribió tienen intenciones muy diferentes y el primero está mal escrito. No tiene sentido decir porque ∀ requiere tanto sus argumentos por los tipos que significa que si ∀ x : A . B debe estar bien escrito, debemos tener B : ∗ . Sin embargo, λ x . x no es un tipo, que tan sólo puede ser asignado un tipo de forma ∀ x : Una . B , nunca $\forall x : A.\ \lambda x.\ x$$\forall$$\forall x : A. B$$B : *$$\lambda x. x$$\forall x : A. B$$*$. El segundo, por otro lado, es casi (creo que querías devolver no x ) es una función y se le da un tipo usando dos ∀ s.$a$$x$$\forall$

Tenga en cuenta que los tipos existenciales y universales son bastante diferentes. Es lógica constructiva, no lógica clásica y en lógica constructiva y ∃ no están tan relacionados como lo están en la lógica clásica.$\forall$$\exists$

es el tipo de programas que reciben un objeto de tipo A y devuelven un objeto de tipo B ( x ) . Lo importante aquí es que el tipo B ( x ) dependede xy no es el mismo para todas las x . Puede variar dependiendo de quées x . Para una entrada x podríamos generar un número entero. Para otro podríamos generar un número real. Para otro más, podríamos generar una función sobre números reales. Si B ( x $\forall x:A. B(x)$$A$$B(x)$$B(x)$ $x$$x$$x$$x$$B(x)$no varía con , puede utilizar un → B en su lugar, que es el tipo de funciones de A a B .$x$$A\to B$$A$$B$

es laversióndependientede la disyunción (constructiva). Se puede pensar en la disyunción constructiva A ∨ B de dos tipos A y B como la unión disjunta de A y B . ∃ x : A . B ( x ) es la unión de la desunión de una colección de tipos B ( x ) indexada por x : A . El hecho de que el tipo B $\exists x:A. B(x)$$A \lor B$$A$$B$$A$$B$$\exists x:A.B(x)$$B(x)$$x:A$ van varían según el valor de x : A lo convierte en un tipo dependiente. Comparar con el caso en que B no depende de x : A : ∃ x : Una . B . Estamos tomando una copia de la misma B para cada x : Una . Esta es isomorfo a A × B .$B(x)$$x:A$$B$$x:A$$\exists x:A. B$$B$$x:A$$A \times B$

Ahora puede preguntar por qué necesitamos productos dependientes y tipos de suma. Porque nos dan más poder expresivo. Ahora podemos ignorar los tipos por completo y tener una teoría de tipos / programación funcional sin tipo. Pero eso elimina los beneficios de tener tipos en primer lugar, por ejemplo, no sabrá si todos los programas siempre terminarán (normalización fuerte). Ver Cubo Lambda y Tipo dependiente . Creo que una buena manera de entender bien los tipos dependientes es mirar las reglas para introducir y eliminar los tipos dependientes en la teoría de tipos de Martin-Lof .

El punto principal de los tipos dependientes es: queremos permanecer dentro de una buena teoría escrita por varias razones (por ejemplo, evitar errores, prueba automática de terminación, etc.). No queremos ir a algo así como el cálculo lambda sin tipo, donde podemos hacer que la expresión como las que mencionaste sea mucho más poderosa. Podemos decir que los tipos dependientes se inventaron para permitir expresar más cosas sin dejar de estar dentro de una buena teoría de tipos.