Types dépendants vs types de raffinement

Quelqu'un pourrait-il expliquer la différence entre les types dépendants et les types de raffinement? Si je comprends bien, un type de raffinement contient toutes les valeurs d’un type satisfaisant un prédicat. Existe-t-il une caractéristique des types dépendants qui les distingue?

Si cela peut aider, je suis tombé sur les types raffinés via le projet Liquid Haskell et les types dépendants via Coq et Agda. Cela dit, je cherche une explication sur la différence entre les théories.

Les principales différences concernent deux dimensions: la théorie sous-jacente et la manière dont elles peuvent être utilisées. Permet de nous concentrer sur ce dernier.

En tant qu'utilisateur, la "logique" des spécifications dans LiquidHaskell et les systèmes de type raffinement se limitent généralement aux fragments décidables, de sorte que la vérification (et l'inférence) sont complètement automatiques, ce qui signifie que vous ne devez pas utiliser de "termes de preuve" du type dont ils ont besoin. paramètre dépendant. Cela conduit à une automatisation importante. Par exemple, comparez le type d'insertion dans LH:

http://ucsd-progsys.github.io/lh-workshop/04-case-study-insertsort.html#/ordered-lists

vs à Idris

https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr

Cependant, l'automatisation a un prix. On ne peut pas utiliser des fonctions arbitraires comme spécifications dans un monde totalement dépendant, ce qui limite la classe de propriétés que l'on peut écrire.

Ainsi, l'un des objectifs des systèmes de raffinement est d' élargir la classe de ce qui peut être spécifié, tandis que celui des systèmes totalement dépendants est d' automatiser ce qui peut être prouvé. Peut-être y a-t-il un heureux lieu de rencontre où nous pouvons obtenir le meilleur des deux mondes!

Les types de raffinement sont simplement des types usuels avec prédicats. C'est-à-dire, étant donné que est un type habituel et que est un prédicat sur$T$$P$$T$

Autant que je sache, dans Liquid Haskell, ils autorisent également certains types de fonctions dépendants , à savoir les types [1]. Notez que les types totalement dépendants (comme les types sigma) ne sont pas autorisés.$\{x:T_1 \to T_2 \mid P\}$

Le système Liquid Type, décrit dans [1], est décidable et Liquid Haskell utilise des solveurs SMT. Cependant, Liquid Haskell requiert également des termes de preuve (ou des valeurs, comme celles-ci sont appelées dans un langage typé de manière non dépendante): si vous vous assoyez pour écrire un programme Liquid Haskell, vous écrivez vos propres fonctions, pas seulement les types.

[1] http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf

Les types dépendants sont des types qui dépendent des valeurs de quelque manière que ce soit. Un exemple classique est "le type de vecteurs de longueur n", où nest une valeur. Les types de raffinement, comme vous le dites dans la question, consistent en toutes les valeurs d'un type donné qui satisfont un prédicat donné. Par exemple, le type de nombres positifs. Ces concepts ne sont pas particulièrement liés (à ma connaissance). Bien sûr, vous pouvez aussi raisonnablement avoir des types d'affinement dépendants, tels que "type de tous les nombres supérieurs à n".