Que ne peut pas faire Idris en abandonnant la complétude de Turing?

Je sais qu'Idris a des types dépendants mais n'est pas complet. Que peut-il ne pas faire en abandonnant la complétude de Turing, et est-ce lié à avoir des types dépendants?

Je suppose que cette question est assez spécifique, mais je ne connais pas énormément les types dépendants et les systèmes de types associés.

Idris est Turing complet! Il vérifie la totalité (terminaison lors de la programmation avec données, productivité lors de la programmation avec codata) mais n'exige pas que tout soit total.

Fait intéressant, disposer de données et de codata suffit à modéliser la complétude de Turing, car vous pouvez écrire une monade pour des fonctions partielles. Je l’ai fait il ya des années dans Coq - c’est probablement le cas actuellement, mais ici, c’est néanmoins: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v .

Vous avez besoin d’une seule évasion pour exécuter de telles choses, mais Idris vous permet de le faire.

Idris ne réduira pas les fonctions partielles au niveau du type, afin de maintenir la vérification du type décidable. En outre, seuls les programmes totaux peuvent raisonnablement être considérés comme des preuves.

Premièrement, je suppose que vous avez déjà entendu parler de la thèse de Church-Turing, selon laquelle tout ce que nous appelons le «calcul» peut être fait avec une machine de Turing (ou l’un des nombreux modèles équivalents). Ainsi, un langage complet de Turing est un langage dans lequel tout calcul peut être exprimé. Inversement, un langage incomplet de Turing est un langage dans lequel certains calculs ne peuvent être exprimés.

Ok, ce n'était pas très instructif. Laissez-moi vous donner un exemple. Il y a une chose que vous ne pouvez pas faire dans un langage Turing-incomplet: vous ne pouvez pas écrire un simulateur de machine de Turing (sinon, vous pourriez encoder n'importe quel calcul sur la machine de Turing simulée).

Ok, ce encore n'a pas été très instructif. La vraie question est: quel programme utile ne peut pas être écrit dans un langage incomplet? Eh bien, personne n’a proposé de définition de «programme utile» incluant tous les programmes écrits par quelqu'un dans un but utile, sans compter tous les calculs de la machine de Turing. Donc, concevoir un langage incomplet de Turing dans lequel vous pouvez écrire tous les programmes utiles reste un objectif de recherche à très long terme.

Maintenant, il existe plusieurs types très différents de langages Turing-incomplets, et ils diffèrent par ce qu'ils ne peuvent pas faire. Toutefois, il existe un thème commun: les langages Turing-complete doivent inclure un moyen de terminer conditionnellement ou de continuer à fonctionner pendant une durée qui n'est pas limitée par la taille du programme, et un moyen pour le programme d'utiliser une quantité de mémoire qui dépend de l'entrée . Concrètement, les langages de programmation les plus impératifs fournissent ces capacités via des boucles while et une allocation dynamique de la mémoire, respectivement. La plupart des langages de programmation fonctionnels fournissent ces capacités via la récursivité et l’imbrication de la structure de données.

Idris est fortement inspiré par Agda . Agda est un langage conçu pour prouver des théorèmes . Maintenant , prouvant théorèmes et les programmes en cours d' exécution sont très étroitement liés , de sorte que vous pouvez écrire des programmes en Agda comme vous prouvez un théorème. Intuitivement, une preuve du théorème «A implique B» est une fonction qui prend une preuve du théorème A comme argument et renvoie une preuve du théorème B.

Puisque le but du système est de prouver des théorèmes, vous ne pouvez pas laisser le programmeur écrire des fonctions arbitraires. Imaginez que le langage vous permette d’écrire une fonction récursive qui s’appelle tout simplement:

oops : A -> B
oops x = oops x

Vous ne pouvez pas laisser l’existence d’une telle fonction vous convaincre que A implique B, sinon vous seriez en mesure de prouver quoi que ce soit et pas seulement de vrais théorèmes! Ainsi, Agda (et des démonstrateurs de théorèmes similaires) interdisent la récursion arbitraire. Lorsque vous écrivez une fonction récursive, vous devez prouver qu'elle se termine toujours , de sorte que chaque fois que vous l'exécutez sur une preuve du théorème A, vous savez qu'elle construira une preuve du théorème B.

La limite pratique immédiate d'Agda est qu'il est impossible d'écrire des fonctions récursives arbitraires. Étant donné que le système doit pouvoir rejeter toutes les fonctions non terminantes, l'indécidabilité du problème bloquant (ou plus généralement du théorème de Rice ) garantit qu'il existe également des fonctions terminales qui sont également rejetées. Une difficulté pratique supplémentaire est que vous devez aider le système à prouver que votre fonction prend fin.

Il existe de nombreuses recherches en cours pour rendre les systèmes de preuve plus similaires à un langage de programmation sans compromettre leur garantie que si vous avez une fonction de A à B, c'est aussi bon que la preuve mathématique que A implique B. Elargir le système pour en accepter plus la terminaison des fonctions est l’un des sujets de recherche. Les autres directions d'extension comprennent la gestion de problèmes tels que les entrées / sorties et la simultanéité dans le «monde réel». Un autre défi consiste à rendre ces systèmes accessibles aux simples mortels (ou peut-être à convaincre les simples mortels de leur accessibilité).

Je ne connais pas Idris. C'est une réponse aux défis que je viens de mentionner. D'après ce que j'ai compris d'un simple coup d'œil à la pré - impression de 2013 , Idris est un logiciel complet, mais comprend un vérificateur de totalité. Le vérificateur de totalité vérifie que chaque fonction annotée avec le mot-clé se totaltermine. Le fragment de langue qui ne contient que des programmes Idris où chaque fonction est totale a un pouvoir expressif similaire à Arda (probablement pas une correspondance exacte en raison de différences dans la théorie des types, mais suffisamment proche pour que vous ne le remarquiez pas, à moins d’essayer délibérément).

Pour d'autres exemples de langages qui ne sont pas complets de Turing de différentes manières, voir Quelles sont les limitations pratiques d'un langage complet tel que le Coq? (dont cette réponse est dans une large mesure prise).