Qu’est ce que la prédicativité?

J’ai une assez bonne intuition sur les types que Haskell interdit comme “imprédicatifs”: à savoir ceux où un forall apparaît dans un argument d’un constructeur de type autre que -> . Mais quelle est la prédication? Qu’est-ce qui le rend important? Comment se rapporte-t-il au mot “prédicat”?

Permettez-moi d’append un point concernant le problème de «l’étymologie», puisque l’autre réponse de @DanielWagner couvre une grande partie du terrain technique.

Un prédicat sur quelque chose comme a est a -> Bool . Maintenant, une logique de prédicat est une logique qui peut en quelque sorte expliquer les prédicats – donc si nous avons un prédicat P et que nous pouvons en parler, pour un a donné, P(a) , maintenant dans une “logique de prédicat” (comme premier -ordre logique) on peut aussi dire ∀a. P(a) ∀a. P(a) . Nous pouvons donc quantifier les variables et discuter du comportement des prédicats sur de telles choses.

Maintenant, à notre tour, nous disons qu’une instruction est prédicative si toutes les choses auxquelles un prédicat est appliqué sont introduites avant . Donc, les déclarations sont “basées sur” les choses qui existent déjà. À son tour, une déclaration est imprédicative si elle peut en quelque sorte se référer à elle-même par ses “bootstraps”.

Donc, dans le cas, par exemple, de l’ id ci-dessus, nous trouvons que nous pouvons donner un type à id sorte qu’il prenne quelque chose du type d’ id dans quelque chose d’autre du type d’ id . Donc, maintenant, nous pouvons donner à une fonction un type où une variable quantifiée (introduite par forall a. ) Peut “se développer” pour être du même type que celle de la fonction entière elle-même!

Par conséquent, l’imprédication introduit une possibilité d’une certaine “référence de soi”. Mais attendez, vous pourriez dire, une telle chose ne mènerait-elle pas à la contradiction? La réponse est: “bien, parfois.” En particulier, “System F” qui est le lambda calcul polymorphe et le “core” essentiel du langage “core” de GHC permet une forme d’imprédicativité qui a néanmoins deux niveaux: le niveau de valeur et le niveau de type autorisé. quantifier sur lui-même. Dans cette stratification à deux niveaux, nous pouvons avoir une imprévisibilité et non une contradiction / un paradoxe.

Notez cependant que cette astuce est très délicate et facile à bousculer par l’ajout de fonctionnalités supplémentaires, comme l’indique cette collection d’articles d’Oleg: http://okmij.org/ftp/Haskell/impredicativity-bites.html

La question centrale de ces systèmes de type est la suivante: “Pouvez-vous substituer un type polymorphe à une variable de type?”. Les systèmes de type prédicatif sont la cantine scolaire «absurde», «ABSOLUMENT NON», alors que les systèmes de type imprédicatif sont votre copain insouciant qui pense que cela semble être une idée amusante et qu’est-ce qui pourrait mal tourner?

Maintenant, Haskell embrouille un peu la discussion car elle pense que le polymorphism devrait être utile mais invisible. Donc pour le rest de ce post, je vais écrire dans un dialecte de Haskell où les utilisations de forall ne sont pas seulement autorisées mais requirejses. De cette façon, nous pouvons distinguer le type a , qui est un type monomorphe qui tire sa valeur d’un environnement de typage que nous pouvons définir plus tard, et le type forall a. a forall a. a , qui est l’un des types polymorphes les plus difficiles à habiter. Nous allons également permettre à tout le monde d’aller pratiquement n’importe où dans un type – comme nous le verrons, GHC restreint sa syntaxe de type en tant que mécanisme “échec rapide” plutôt qu’en tant que condition technique.

Supposons que nous ayons dit au compilateur id :: forall a. a -> a id :: forall a. a -> a . Pouvons-nous demander plus tard à utiliser id comme s’il y avait du type (forall b. b) -> (forall b. b) ? Les systèmes de type imprédicatif sont d’accord avec cela, car nous pouvons instancier le quantificateur dans le type de l’ id pour tout forall b. b forall b. b , et remplacez tout forall b. b forall b. b pour a partout dans le résultat. Les systèmes de type prédicatif sont un peu plus méfiants à cet égard: seuls les types monomorphes sont autorisés. Donc, si nous avions un b particulier, nous pourrions écrire id :: b -> b .

Il y a une histoire similaire à propos de [] :: forall a. [a] [] :: forall a. [a] et (:) :: forall a. a -> [a] -> [a] (:) :: forall a. a -> [a] -> [a] . Alors que votre copain insouciant peut être d’accord avec [] :: [forall b. b] [] :: [forall b. b] et (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] (:) :: (forall b. b) -> [forall b. b] -> [forall b. b] , l’école maternelle prédicative n’est pas tellement. En fait, comme vous pouvez le voir sur les deux seuls constructeurs de listes, il est impossible de produire des listes contenant des valeurs polymorphes sans instancier la variable de type dans leurs constructeurs à une valeur polymorphe. Donc, bien que le type [forall b. b] [forall b. b] est autorisé dans notre dialecte de Haskell, ce n’est pas vraiment raisonnable – il n’y a pas de termes de ce type. Cela motive la décision de GHC de se plaindre si vous pensez même à un tel type – c’est la manière du compilateur de vous dire “ne vous embêtez pas”. *

Eh bien, qu’est-ce qui rend la maîtresse de l’école si ssortingcte? Comme d’habitude, la réponse est de garder la vérification de type et l’inférence de type possible. L’inférence de type pour les types imprédicatifs est exacte. La vérification de type semble être possible , mais c’est compliqué et personne ne veut le maintenir.

D’un autre côté, certains pourraient objecter que GHC est parfaitement satisfait de certains types qui semblent nécessiter une imprédication:

 > :set -Rank2Types > :t id :: (forall b. b) -> (forall b. b) {- no complaint, but very chatty -} 

Il s’avère que certaines versions légèrement restreintes de l’imprédicativité ne sont pas trop mauvaises: en particulier, les types de rang supérieur de vérification de type (qui permettent aux variables de type d’être remplacées par des types polymorphes quand ils ne sont que des arguments à (->) ) sont relativement simples. . Vous perdez l’inférence de type au-dessus du rang 2, et les types principaux au-dessus du rang 1, mais les types de rangs supérieurs sont parfois ce que le médecin a ordonné.

Ne sais pas sur l’étymologie du mot, cependant!

* Vous pourriez vous demander si vous pouvez faire quelque chose comme ceci:

 data FooTy a where FooTm :: FooTy (forall a. a) 

Vous obtiendrez alors un terme ( FooTm ) dont le type a quelque chose de polymorphe en tant qu’argument de quelque chose d’autre que (->) (à savoir, FooTy ), vous n’avez pas à traverser la maitresse pour le faire, et donc la croyance “appliquer utiliser des types non (->) vers des types polymorphes n’est pas utile car vous ne pouvez pas les créer “serait invalidé. GHC ne vous laisse pas écrire FooTy , et je dois admettre que je ne suis pas sûr qu’il y ait une raison de principe pour la ressortingction ou non.

(Mise à jour rapide quelques années plus tard: il y a une bonne raison de principe selon laquelle FooTm n’est toujours pas correcte. À savoir, les GADT implémentent des égalités de type, donc le type étendu de FooTm est en fait FooTm :: forall a. (a ~ forall b. b) => FooTy a . Donc, pour utiliser réellement FooTm , il faudrait en effet instancier une variable de type polymorphe, merci à Stephanie Weirich de m’avoir signalé cela.)

J’aimerais faire un commentaire sur la question de l’étymologie, car la réponse de @ sclv n’est pas tout à fait correcte (étymologiquement, pas conceptuellement).

Retourner dans le temps, à l’époque de Russell, où tout est mis en théorie, y compris la logique. Une des notions logiques de l’importance particulière est le «principe de compréhension»; c’est-à-dire, étant donné un prédicat logique φ:A→2 nous aimerions avoir un principe pour déterminer l’ensemble de tous les éléments satisfaisant ce prédicat, écrit sous la forme ” {x | φ(x) } ” ou une variante. Le point essentiel à retenir est que les “ensembles” et les “prédicats” sont considérés comme des choses fondamentalement différentes: les prédicats sont des correspondances entre des objects et des valeurs de vérité, et les ensembles sont des objects. Ainsi, par exemple, nous pouvons autoriser la quantification des ensembles mais pas la quantification des prédicats.

Maintenant, Russell était plutôt préoccupé par son paradoxe éponyme et cherchait un moyen de s’en débarrasser. Les corrections sont nombreuses, mais l’intérêt ici est de restreindre le principe de compréhension. Mais d’abord, la définition formelle du principe: ∃S.∀xS x ↔︎ φ(x) ; c’est-à-dire que pour notre φ particulier, il existe un object (c’est-à-dire un ensemble) S tel que pour chaque object (aussi un ensemble, mais considéré comme un élément) x , nous avons S x x∈S “, bien que les logiciens du temps aient donné” “un sens différent de la simple juxtaposition) est vrai juste au cas où φ(x) est vrai. Si nous prenons le principe exactement comme écrit, nous nous retrouvons avec une théorie imprédicative. Cependant, nous pouvons imposer des ressortingctions sur ce que nous sums autorisés à comprendre. (Par exemple, si nous disons que φ ne doit contenir aucun quantificateur de second ordre.) Ainsi, pour toute ressortingction R , si un ensemble S est déterminé (généré par compréhension) par un prédicat R , alors nous disons que S est ” R -prédicatif”. Si chaque ensemble dans notre langue est R -prédicatif alors nous disons que notre langue est ” R -prédicative”. Et puis, comme c’est souvent le cas avec les préfixes composés d’un trait d’union, le préfixe est supprimé et laissé implicite, d’où les langages “prédicatifs”. Et, naturellement, les langues qui ne sont pas prédicatives sont “imprédicatives”.

C’est l’étymologie de l’ancienne école. Depuis ces jours-là, les conditions ont pris leur envol. Les façons dont nous utilisons “prédicatif” et “imprédicatif” aujourd’hui sont très différentes, car les choses qui nous préoccupent ont changé. Donc, il peut parfois être un peu difficile de voir à quel point notre usage moderne est lié à ce genre de choses. Honnêtement, je ne pense pas que connaître l’étymologie aide vraiment à comprendre en quoi consistent réellement les mots (de nos jours).