¿Existe una jerarquía de expresividad para los sistemas de tipos?

Inspirado por las extensas jerarquías presentes en la teoría de la complejidad, me preguntaba si tales jerarquías también estaban presentes para los sistemas de tipos. Sin embargo, los dos ejemplos que he encontrado hasta ahora son más parecidos a listas de verificación (con características ortogonales) que a jerarquías (con sistemas de tipo sucesivamente más y más expresivos).

Los dos ejemplos que he encontrado son el cubo Lambda y el concepto de polimorfismo con clasificación k . La primera es una lista de verificación con tres opciones, la segunda es una jerarquía real (aunque creo que la clasificación k para valores específicos de k es poco común). Todas las demás características del sistema de tipos que conozco son en su mayoría ortogonales.

Estoy interesado en estos conceptos porque estoy diseñando mi propio lenguaje y tengo mucha curiosidad por cómo se clasifica entre los sistemas de tipos existentes actualmente (mi sistema de tipos es algo poco convencional, hasta donde yo sé).

Me doy cuenta de que el concepto de 'expresividad' puede ser un poco vago, lo que puede explicar por qué los sistemas de tipos me parecen listas de verificación.

Hay varios sentidos de "expresividad" que puede desear para un sistema de tipos.

1. ¿Qué funciones matemáticas puedes expresar en un sistema de tipos particular? Por ejemplo, en el cálculo lambda simplemente escrito, no todas las funciones computables pueden expresarse. Lo mismo ocurre con el Sistema , pero se pueden expresar estrictamente más funciones. Esto no es muy interesante una vez que llega a escribir sistemas para idiomas completos de Turing.$F$

2. ¿Puede el sistema verificar todos los programas escritos en el sistema B ? Esto es básicamente de lo que se trata la primera noción de fuerza de Cody para los STP. Una vez más, Sistema F es más fuerte que el STLC en este orden, ya que cada tipo de programa en STLC Sistema F . Del mismo modo, un sistema con subtipo será más fuerte que un sistema sin él.$A$$B$$F$$F$

3. ¿Existen transformaciones locales (en el sentido del artículo de Felleisen sobre el poder expresivo de los lenguajes de programación ) que permiten que un programa que escribe en el sistema escriba en el sistema B , pero no al revés. $A$$B$

4. ¿Un sistema de tipo garantiza propiedades más fuertes que otro? Por ejemplo, los sistemas de tipo lineal simplemente rechazan más programas, pero eso les permite hacer declaraciones más sólidas sobre los programas que aceptan.

Desafortunadamente, no creo que se haya trabajado en categorizar o formalizar estas nociones, con la excepción del cubo lambda de Barendregt, como comenta @cody.

No estoy seguro de tener una respuesta satisfactoria a su pregunta, pero si considera los Sistemas de tipo puro, que son una generalización de los sistemas que se encuentran en el cubo lambda (se puede encontrar una descripción completa, aunque algo anticuada, en el texto clásico de Barendregt ) entonces hay un par de nociones naturales de jerarquías:

1. $\Gamma\vdash_A\ t\colon T$$\Gamma\vdash_B\ t\colon T$$\Gamma, t$$T$$*\colon *$$(*,*,*)$PTS en el sentido de que hay un morfismo de cualquier otro PTS. Esto puede verse como una medida de la expresividad de un sistema de tipos, donde el PTS final es el sistema más expresivo.

2. $A$$B$$A$$F_\omega$$ECC$$\leftrightarrow$