Il y a un travail récent de Paul-André Melliès et Noam Zeilberger qui explore cela. En particulier, les articles Functors sont des systèmes de raffinement de type et un théorème de dualité Isbell pour les systèmes de raffinement de type . Il y a aussi une vidéo d'un discours sur le premier.
Je pense qu'il y a beaucoup de confusion autour des types de raffinement parce que les gens pensent que des systèmes particuliers sont représentatifs, ce qui fait que les objectifs et les détails de ces systèmes particuliers sont attribués à l'idée générale. Les systèmes de raffinement de types classent les termes qui existent indépendamment tandis que les types (non raffinés), dépendants ou non, font partie des termes. Cela peut sembler familier et peut-être même un peu contradictoire.
La partie apparemment potentiellement familière et peut-être contradictoire se produit si vous regardez les types à la Curry (extrinsèquement) contre les types à la Church (intrinsèquement). Quand nous pensons aux types à la Curry, nous pensons aux types comme classant des termes non typés qui ont déjà un sens. Dans les types à la Church, les seuls termes qui existent sont des termes bien typés, c'est-à-dire que les contraintes de type font partie de notre syntaxe. Donc, ce que je dis, c'est qu'un système de type Curry est en fait un système de raffinement de type raffinant des termes non typés, alors qu'un système de type Church n'est pas un système de raffinement de type. Cela signifie que, par exemple, nous pouvons considérer le calcul lambda simplement typé comme un système de raffinement de type ou comme un système de type sans raffinement.
Bien sûr, personne ne dit que nos termes doivent être des termes non typés. Nous pourrions tout aussi bien appliquer un système de raffinement de type aux termes typés, et, historiquement, c'est le contexte dans lequel les types de raffinement (de ce nom) sont apparus. Cependant, les applications au typage logiciel illustrent quelque chose de plus proche de la situation décrite ci-dessus.
Jusqu'à présent, je n'ai rien dit sur les types dépendants. La raison en est qu'il s'agit d'une préoccupation complètement orthogonale. Je dirais que les systèmes de type dépendants archétypaux sont généralement présentés dans un style d'église, et ne sont donc pas des systèmes de raffinement de type, mais NuPRL (basé sur la théorie de type informatique , une variante de la théorie de type dépendante la plus archétypale, la théorie de type Martin-Löf) est manifestement un système de raffinement de type comme je l'ai décrit. Les termes dans NuPRL peuvent même ne pas avoir de types! Certes, le fait que "PRL" signifie "Program Refinement Logic" pourrait aussi être un indice. D'un autre côté, Refinement Types for ML décrit un système de type de raffinement, peut-être l'origine du terme, qui n'est en aucun cas un système de type dépendant.
Quant aux triplets Hoare, ils sont un système de raffinement de type. Ils sont en fait utilisés comme exemple d'un système de raffinement de type dans le premier article. Cependant, la théorie des types de Hoare donne quelque chose qui peut être considéré comme un système de type sans raffinement pour une langue ayant des triplets de Hoare.
Pour avoir une réponse sur la «puissance» de différents systèmes, vous devez spécifier un (des) type (s) de système (s) dépendant (s) particulier (s) et un (des) type (s) de type (s) de raffinement particulier (s). Le terme "système de type dépendant" couvre une très large classe de systèmes de type et "systèmes de raffinement de type" est encore plus large. Même alors, les termes ne s'excluent pas mutuellement, il ne s'agirait donc pas d'une comparaison entre les "systèmes de type dépendants" et les "systèmes de type de raffinement". Cependant, si par "système de type dépendant" vous pensez à quelque chose comme Coq , et pour "système de type de raffinement" quelque chose comme Liquid Typesalors c'est plutôt unilatéral. Coq est généralement considéré comme suffisamment puissant pour gérer pratiquement toutes les mathématiques dans la pratique; vous pouvez littéralement implémenter et prouver la validité d'un solveur SMT dans Coq, puis l'utiliser; et un analogue très proche du type de sous-ensemble peut être formulé. (NuPRL a littéralement des types de sous-ensembles.) De l'autre côté, les solveurs SMT sont généralement limités à des théories décidables où Coq n'a pas une telle limitation; et de nombreux systèmes comme Liquid Types ont un langage limité et non extensible pour spécifier les prédicats. (Bien sûr, par "système de type dépendant", vous pourriez signifier ML dépendant , et par "système de raffinement de type" NuPRL [qui est également un système de type dépendant] qui serait unilatéral dans l'autre sens.)
