Quelle est la théorie des types dépendants la plus intuitive que j'ai pu apprendre?

Je suis intéressé à obtenir une compréhension vraiment solide sur la dactylographie dépendante. J'ai lu la majeure partie de TaPL et lu (s'il n'est pas complètement assimilé ) "Types dépendants" dans ATTaPL . J'ai également lu et parcouru de nombreux articles sur la dactylographie dépendante.

De nombreuses discussions sur la théorie des types semblent porter sur l'ajout de fonctionnalités incrémentielles aux systèmes de types précédents, et non sur "quelle est la prochaine grande généralisation à partir du système de type X?". Les types dépendants semblent être la prochaine grande généralisation de System F, mais je n'ai pas encore trouvé le langage intuitif, canonique, typé de manière dépendante. Les nombreuses références au calcul de constructions (inductives) me font penser que CoC est ce langage, mais les explications du langage que j'ai vu ne me semblent pas très claires ni intuitives.

Je m'attends / suppose qu'un tel langage aurait des caractéristiques telles que: (et s'il vous plaît laissez-moi savoir si quelque chose en particulier ressort comme confus ou irréaliste)

• Abstraction généralisée (peut avoir des fonctions de n'importe quel domaine de la hiérarchie des types, en d'autres termes, type -> terme, terme -> type '' 'etc.)
• A une hiérarchie infinie de typage (termes: types: types ': types' ': ...)
• Un minimum d'éléments de base. J'imagine que le langage n'affirme qu'un seul élément pour chaque niveau. Par exemple, il pourrait affirmer que ((): Unité: Type: Type ': ...). D'autres éléments sont construits à partir de ces éléments.
• La somme et les types de produits sont dérivables.

Je cherche également une explication de cette langue qui, idéalement, traiterait:

• La relation entre abstraction et quantification dans cette langue. S'ils ne sont pas unifiés, expliquez pourquoi ils ne le sont pas.
• La hiérarchie des types infinis explicitement

Je pose cette question parce que je veux apprendre la théorie des types dépendants, mais aussi parce que je veux élaborer un guide qui, en supposant un peu d’expérience en CS, enseigne l’utilisation et la compréhension des assistants de preuve et des langages typés de manière dépendante.

(Croix posté à Reddit)

Il y a différentes manières d'aborder cela:

1. Théorie des types dépendants . Ce n'est probablement pas le moyen le plus simple de connaître les types dépendants, mais vous pouvez vous reporter aux papiers Calculus of Constructions et leurs variantes, Pure Type Systems et à l'article de Martin Hofmann sur la syntaxe et la sémantique des types dépendants, par exemple.

2. Théorème prouvant . Tout d'abord, jetez un coup d'œil à ma réponse à une question connexe: comment pourrais-je apprendre la théorie sous-jacente de l'assistant de preuves Coq? .

3. Programmation avec types dépendants . En regardant des langues récentes avec des types dépendants tels que Epigram ou Agda ou des langues moins récentes telles que Dependent ML , la rédaction de certains programmes aidera à consolider les idées. Epigram, par exemple, est extrêmement propre. Un autre angle est de voir comment les types dépendants sont implémentés . Une théorie pratique des types dépendants est : Types dépendants sans le sucre. Plusieurs thèses de doctorat sont consacrées à la programmation avec la théorie des types dépendants: celle de Dan Licata , celle de Nils Anders Danielsson , celle d' Ulf Norrel , celle de Susmit Sarkar.$\Pi\Sigma$, entre autres. Et bien sûr, il y a le livre d'Adam Chlipala, donné dans la réponse de Marc Hamann.

Je serais enclin à commencer par la programmation, avant de passer à la démonstration de théorèmes, puis à explorer les questions plus théoriques.

Le calcul - qui est essentiellement le coeur de la FL, à son tour l'approche la plus largement réimplémentée de la logique d'ordre supérieur - est de loin le système le plus simple à dépendre de manière dépendante que l'on puisse apprendre, puisqu'il se limite à l'extension du type système du lambda calcul simplement typé avec des quantificateurs typés de manière dépendante. Les intuitions essentielles pour maîtriser la FL sont donc des intuitions que vous devez maîtriser avec toute théorie avec des types dépendants.$\lambda\pi$

Twelf est un bon système de démonstration de théorèmes basé sur la FL. En parcourant les notes de cours avancées proposées par Frank Pfenning, vous découvrirez une bonne introduction à la théorie et à la pratique de la FL.

Cela dit, ce n’est peut-être pas le meilleur premier système à savoir si vous vous intéressez davantage aux mathématiques constructives qu’aux éléments essentiels de la théorie des types: LF désigne un cadre logique et c’est un système utilisé pour axiomatiser les théories. un système cible directement. La meilleure introduction est probablement l’utilisation d’un système basé sur la théorie des types de Martin-Loef - mentionne Agda, entre autres - est peut-être un meilleur point de départ si tel est votre objectif, car vous pouvez utiliser plus rapidement les types arithmétique et inductif dans un tel contexte. cadre.

Le CdC est probablement la voie à suivre. Il suffit de plonger dans Coq et de suivre un didacticiel intéressant tel que Software Foundations (auquel Pierce of TaPL et ATTaPL participe).

Une fois que vous avez compris les aspects pratiques de la frappe dépendante, retournez aux sources théoriques: elles auront alors beaucoup plus de sens.

Votre liste de fonctionnalités semble fondamentalement correcte, mais voir comment elles se déroulent dans la pratique rapporte mille points de fonctionnalité.

(Un autre tutoriel légèrement plus avancé est la programmation certifiée par Adam Chlipala avec types dépendants )

Je pensais que cet article avait aidé à démystifier le concept au niveau élémentaire: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html

Jetez un coup d’œil sur http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf et sur un système PiSigma plus ancien qui y est mentionné.