¿Los tipos automáticos hacen que el cálculo de las construcciones inductivas quede obsoleto?

Los tipos propios son una extensión del cálculo de construcciones [1] que permiten que el lenguaje exprese tipos de datos algebraicos codificados a través de la codificación Scott. Scott Encoding proporciona a uno la capacidad de combinar patrones O(1), que es uno de los principales motivadores para la inclusión de definiciones inductivas en CC. Sin embargo, los tipos de uno mismo son una teoría básica mucho más simple y elegante, y aparentemente no son menos poderosos.

¿Los tipos de self, bajo un punto de vista teórico, hacen que CIC quede obsoleto, o todavía hay algún aspecto en el que CIC es favorable en relación con los self tyes?

[1] http://staff.computing.dundee.ac.uk/pengfu/document/talks/mvd-2012.pdf

No soy un experto en este trabajo, pero me parece que el principal problema actual es la falta de pruebas SN, incluso con restricciones. Sin embargo, estas pruebas son notoriamente complicadas, incluso cuando el cálculo es correcto, por lo que le daré un poco de tiempo. El trabajo es ciertamente muy prometedor.

Una cosa a tener en cuenta es que estas restricciones no son realmente triviales de expresar, lo que es una gran parte de la complejidad de la formulación de las familias inductivas en el CIC. El verdadero punto de venta de un enfoque como este sería formular de manera concisa estas condiciones.

Ha sido un problema abierto de larga data tener un lenguaje tipeado de forma dependiente que es

• Consistente / Normalizante
• Puede expresar todas las familias de tipos desde Coq (o incluso Agda)
• Permite una simple expresión de recurrencia sobre estas familias.
• $\Pi,\Sigma,\mu$

$\Pi\Sigma$