Os tipos de self tornam obsoleto o cálculo das construções indutivas?

Self Types são uma extensão do Cálculo de Construções [1] que permite que o idioma expresse tipos de dados algébricos codificados através da Codificação Scott. A Codificação Scott fornece a capacidade de correspondência de padrões O(1), que é um dos principais motivadores para a inclusão de definições indutivas no CC. No entanto, os Self Types são uma teoria de base muito mais simples e elegante e aparentemente não são menos poderosos.

Os Self Types, sob um ponto de vista teórico, tornam a CIC obsoleta ou ainda existe algum aspecto em que a CIC é favorável em relação aos Self Tyes?

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

Não sou especialista neste trabalho, mas me parece que a principal questão atual é a falta de prova de SN, mesmo com restrições. Porém, essas provas são notoriamente complicadas, mesmo quando o cálculo está correto, então eu daria um pouco de tempo. O trabalho é certamente muito promissor.

Uma coisa a notar é que essas restrições são realmente pouco triviais de expressar, o que é uma grande parte da complexidade da formulação das famílias indutivas na CIC. O verdadeiro ponto de venda de uma abordagem como essa seria formular concisamente essas condições.

Tem sido um problema aberto há muito tempo ter uma linguagem de tipo dependente que é

• Consistente / Normalizador
• Pode expressar todas as famílias de tipos da Coq (ou mesmo da Agda)
• Permite uma simples expressão de recursão sobre essas famílias
• Simples ou possui um pequeno número de construções principais ( ).$\Pi,\Sigma,\mu$

Uma dessas tentativas que conheço é a linguagem Altenkirch & al , que também carece de um estudo metateórico completo (e também não é consistente sem restrições adicionais).$\Pi\Sigma$