¿Por qué una jerarquía de tipo infinito?

Coq, Agda e Idris tienen una jerarquía de tipos infinita (Tipo 1: Tipo 2: Tipo 3: ...). Pero, ¿por qué no hacerlo como λC, el sistema en el cubo lambda que está más cerca del cálculo de las construcciones, que tiene solo dos tipos, $*$ y , y estas reglas?$◽$

Esto parece más simple. ¿Este sistema tiene limitaciones importantes?

En realidad, el enfoque del CoC es más expresivo: permite una cuantificación impredecible arbitraria. Por ejemplo, el tipo $\forall a.\; a \to a$ puede ser instanciado consigo mismo para obtener $(\forall a.\; a \to a) \to (\forall a.\; a \to a)$ , lo que no es posible con una jerarquía universal.

La razón por la que no se usa ampliamente es porque la cuantificación impredecible es incompatible con la lógica clásica. Si lo tiene, no puede dar un modelo de teoría de tipos en el que los tipos se interpreten como conjuntos de la manera ingenua --- vea el famoso artículo de John Reynolds El polimorfismo no es teórico de conjuntos .

Dado que muchas personas quieren usar la teoría de tipos como una forma de verificar a máquina las pruebas matemáticas ordinarias, generalmente no están entusiasmadas con las características de teoría de tipos que son incompatibles con los fundamentos habituales. De hecho, Coq originalmente apoyó la impredicatividad, pero la han abandonado constantemente.

Complementaré la respuesta de Neel (excelente, como siempre) con un poco más de exposición sobre por qué los niveles se usan en la práctica.

¡La primera limitación importante de CoC es que es trivial! Una observación sorprendente es que no hay ningún tipo para el que pueda probar que tiene más de un elemento, y mucho menos un número infinito de ellos. Agregar solo 2 universos le proporciona los números naturales con infinitos elementos probables y todos los tipos de datos "simples".

La segunda limitación son las reglas de cálculo: CoC solo admite la iteración , es decir, las funciones recusivas no tienen acceso a los términos secundarios de sus argumentos. Por esta razón, es más conveniente agregar tipos inductivos como una construcción primitiva, dando lugar al CIC. Pero ahora surge otro problema: ¡la regla de inducción más natural (llamada eliminación en este contexto) es inconsistente con el Medio Excluido! Estos problemas no aparecen si restringe la regla de inducción a tipos predicativos con universos.

En conclusión, parece que el CoC no tiene ni la expresividad ni la robustez y la consistencia del wrt que le gustaría en un sistema fundamental. Agregar universos resuelve muchos de estos problemas.