Des propriétés telles que l'utilisation de la mémoire d'une fonction peuvent-elles être exprimées dans un langage typé de manière dépendante?

Supposons que l'on veuille raisonner sur les propriétés du code au-delà de choses comme la totalité et la pureté fonctionnelle - on se soucie également de la consommation de mémoire ou de la complexité algorithmique d'une fonction. Cela peut-il être fait à l'aide de systèmes de typage et d'effets dépendants?

Oui il peut. Bien que conceptuellement ce ne soit pas si difficile, cela n'a pas été beaucoup étudié. Un aspect du domaine est la sémantique des coûts comme la recherche effectuée par Guy Blelloch .

Dans la veine de la vidéo mentionnée par Anton, le travail de Daniellson sur l' analyse de la complexité temporelle semi-formelle légère pour les structures de données purement fonctionnelles . Cela utilise en effet une monade pour supporter un coût par opération. Une monade similaire, au niveau sémantique, est utilisée dans la sémantique des coûts de dénotation pour les langages fonctionnels avec des types inductifs . Voici un article de 2016 faisant quelque chose de similaire dans Coq, A Coq Library For Internal Verification of Running-Times .

Les gens de NuPRL sont également intéressés depuis longtemps à faire des choses comme ça. In Expressing Computational Complexity in Contstructive Type Theory , ce qui revient à calculer sur une sémantique opérationnelle structurée. Là où cela devient un peu plus intéressant, c'est que vous pouvez refléter la sémantique du langage dans le langage. L'exemple de la dernière section, section 12, de la théorie du type computationnel naïf illustre et discute ce genre de chose.