Les auto-types rendent-ils le calcul des constructions inductives obsolète?

Les Self Types sont une extension du Calcul des constructions [1] qui permettent au langage d'exprimer des types de données algébriques encodés par le Scott Encoding. Le Scott Encoding offre une possibilité de correspondance de motifs O(1), qui est l'un des principaux facteurs de motivation pour l'inclusion de définitions inductives sur CC. Pourtant, les Self Types sont une théorie de base beaucoup plus simple et élégante, et ne sont apparemment pas moins puissants.

Les Self Types, d'un point de vue théorique, rendent-ils le CIC obsolète, ou y a-t-il encore un aspect sur lequel CIC est favorable par rapport aux Self Tyes?

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

Je ne suis pas un expert dans ce travail, mais il me semble que le problème majeur actuel est le manque de preuve SN, même avec des restrictions. Ces preuves sont notoirement délicates cependant, même lorsque le calcul est correct, donc je lui donnerais un peu de temps. Le travail est certainement très prometteur.

Une chose à noter est que ces restrictions sont en fait assez non triviales à exprimer, ce qui est une grande partie de la complexité de la formulation des familles inductives dans le CIC. Le véritable argument de vente d'une telle approche serait de formuler de manière concise ces conditions.

Cela a été un problème ouvert de longue date d'avoir une langue typée dépendante qui est

• Cohérent / Normalisant
• Peut exprimer toutes les familles de types de Coq (ou même Agda)
• Permet une expression simple de la récursivité sur ces familles
• Simple ou a un petit nombre de constructions de base ( ).$\Pi,\Sigma,\mu$

Une de ces tentatives que je connaisse est le langage Altenkirch & al , qui manque également d'une étude méta-théorique complète (et n'est pas cohérent sans autres restrictions).$\Pi\Sigma$