Pourquoi le type d'identifiant ne peut-il pas être spécialisé dans (pour tous a. A -> a) -> (pour tous b. B -> b)?

Question

Prendre l'humble fonction identité en Haskell,

id :: forall a. a -> a

Étant donné que Haskell censé prendre en charge impredicative polymorphisme, il semble raisonnable que je devrais être en mesure de "restreindre" id pour le type (forall a. a -> a) -> (forall b. b -> b) par type d'attribution. Mais cela ne fonctionne pas:

Prelude> id :: (forall a. a -> a) -> (forall b. b -> b)

<interactive>:1:1:
    Couldn't match expected type `b -> b'
                with actual type `forall a. a -> a'
    Expected type: (forall a. a -> a) -> b -> b
      Actual type: (forall a. a -> a) -> forall a. a -> a
    In the expression: id :: (forall a. a -> a) -> (forall b. b -> b)
    In an equation for `it':
        it = id :: (forall a. a -> a) -> (forall b. b -> b)

Il est bien sûr possible de définir une nouvelle forme restreinte de l'identité, fonction souhaitée signature:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId x = x

Cependant à définir en fonction de la générale id ne fonctionne pas:

restrictedId :: (forall a. a -> a) -> (forall b. b -> b)
restrictedId = id -- Similar error to above

Alors que ce passe ici? Il semble que cela pourrait être lié à des difficultés avec impredicativity, mais l'activation -XImpredicativeTypes ne fait aucune différence.

Answer 1

pourquoi est-il attendre d'un type d' (forall a. a -> a) -> b -> b

Je crois que le type forall b.(forall a. a -> a) -> b -> b est équivalente à la vous a donné. C'est juste une représentation canonique, où sont les forall est décalé, autant pour la gauche que possible.

Et la raison pourquoi il ne fonctionne pas, c'est que le type est en fait plus polymorphes que le type de id :: forall c. c -> c, qui exige que l'argument et les types de retour égal. Mais le pourtout un dans votre type effectivement interdit à un être unifié avec n'importe quel autre type.

Answer 2

Vous avez absolument raison qu' forall b. (forall a. a -> a) -> b -> b n'est pas équivalent à (forall a. a -> a) -> (forall b. b -> b).

Sauf annoté sinon, les variables de type sont quantifiés à l'ultrapériphériques niveau. Donc, (a -> a) -> b -> b est une abréviation de" (forall a. (forall b. (a -> a) -> b -> b)). Dans le Système F, où le type d'abstraction et d'application sont explicites, c'est ce qui décrit un terme comme f = Λa. Λb. λx:(a -> a). λy:b. x y. Juste pour être clair, pour quiconque n'est pas familier avec la notation, Λ est un lambda qui prend un type comme paramètre, contrairement à λ qui prend un terme en tant que paramètre.

L'appelant d' f première fournit un paramètre de type a, puis fournit un paramètre de type b, puis fournit deux valeurs x et y , qui adhèrent à la choisi types. La chose importante à noter est le visiteur choisit a et b. Si l'appelant peut effectuer une application comme f String Int length par exemple pour la production d'un terme String -> Int.

À l'aide de -XRankNTypes vous pouvez annoter un terme explicite de placer le quantificateur universel, il n'a pas à être à la limite extérieure de niveau. Votre restrictedId terme avec le type (forall a. a -> a) -> (forall b. b -> b) pourrait être à peu près illustré dans le Système F g = λx:(forall a. a -> a). if (x Int 0, x Char 'd') > (0, 'e') then x else id. Remarquez comment g, le destinataire de l'appel, peut s'appliquer x deux 0 et 'e' par instanciation avec un premier type.

Mais dans ce cas, l'appelant ne peut pas choisir le type de paramètre comme il l'a fait avant avec f. Notez que les applications x Int et x Char à l'intérieur de la lambda. Cela oblige l'appelant de fournir une fonction polymorphe, de sorte qu'un terme comme g length n'est pas valide car length ne s'applique pas à l' Int ou Char.

Une autre façon de penser, est dessin les types d' f et g comme un arbre. L'arbre en f a un quantificateur universel à la racine de tout l'arbre pour g a une flèche comme la racine. Pour se rendre à la flèche en f, l'appelant instancie les deux quantificateurs. Avec g, c'est déjà un type de flèche et que l'appelant ne peut pas contrôler l'instanciation. Cela oblige l'appelant de fournir un polymorphe argument.

Enfin, s'il vous plaît pardonnez mon artificiel exemples. Gabriel Scherer décrit quelques-uns plus d'utilisations pratiques de rang supérieur à partir de polymorphisme dans Modérément utilisations Pratiques du Système F sur ML. Vous pouvez aussi consulter les chapitres 23 et 30 de TAPL ou de lait écrémé de la documentation du compilateur extensions pour trouver plus de détails ou mieux des exemples pratiques de rang supérieur à partir de polymorphisme.

Answer 3

Je ne suis pas un expert sur impredictive types, de sorte que c'est à la fois une réponse potentielle et essayer d'apprendre quelque chose de commentaires.

Il n'est pas judicieux de se spécialiser

\/ a . a -> a                       (1)

pour

(\/ a . a -> a) -> (\/ b . b -> b)  (2)

et je ne pense pas que impredictive types de sont une raison pour l'autoriser. Les quantificateurs pour effet de rendre les types représentés par la gauche et la droite de (2) inequivalent jeux en général. Pourtant, l' a -> a (1) implique de droite et de gauche sont l'équivalent des ensembles.

E. g. vous pouvez concrétiser (2) à (int -> int) -> (string -> string). Mais par n'importe quel système je sais que ce n'est pas un type représenté par (1).

Le message d'erreur ressemble à des résultats d'une tentative par la Haskel type inferencer d'unifier le type d' id

\/ a . a -> a

avec le type que vous avez donné

\/ c . (c -> c) -> \/ d . (d -> d)

Ici, je suis uniqifying quantifiés variables pour plus de clarté.

Le travail du type inferencer est de trouver un plus général d'affectation pour a, c, et d qui entraîne les deux expressions syntaxiquement égaux. Il constate finalement qu'il est nécessaire d'unifier c et d. Depuis qu'ils sont quantifiées séparément, il est dans une impasse et se ferme.

Vous êtes peut-être en posant la question, parce que le type de base inferencer -- avec un nom (c -> c) -> (d -> d) -- voudrais juste charrue avant et mettre en c == d. Le type résultant serait

(c -> c) -> (c -> c)

qui est juste un raccourci pour

\/c . (c -> c) -> (c -> c)

C'est sensiblement le moins le plus général (le type de théorie de la moindre limite supérieure) de l'expression pour le type d' x = x où x est contraint d'être une fonction avec le même nom de domaine et co-domaine.

Le type de "restricedId" donnée est dans un réel sens trop général. Bien qu'il ne peut jamais conduire à un runtime type d'erreur, il existe de nombreux types décrits par l'expression que vous avez donné comme susmentionnés (int -> int) -> (string -> string) - qu'il est impossible du point de vue opérationnel, même si votre type permettrait.