Interprétation algébrique du polymorphisme

Question

Si je comprends bien la base interprétation algébrique de types:

Either a b ~ a + b
(a, b) ~ a * b
a -> b ~ b^a
()   ~ 1
Void ~ 0 -- from Data.Void

... et que ces relations sont vrai pour les types de béton, comme Bool, par opposition à des types polymorphes comme a. Je sais aussi comment traduire type de signatures avec des types polymorphes dans leur type de béton représentations par la simple traduction de l'Église de codage selon l'isomorphisme suivant:

(forall r . (a -> r) -> r) ~ a

Donc, si j'ai:

id :: forall a . a -> a

Je sais que cela ne signifie pas id ~ a^a, mais il signifie en réalité:

id :: forall a . (() -> a) -> a
id ~ ()
   ~ 1

De la même façon:

pair :: forall r . (a -> b -> r) -> r
pair ~ ((a, b) -> r) - > r
     ~ (a, b)
     ~ a * b

Ce qui m'amène à ma question. Qu'est-ce que le "algébrique" de l'interprétation de cette règle:

(forall r . (a -> r) -> r) ~ a

Pour chaque type de béton isomorphisme je peux point à un équivalent algébrique de la règle, tels que:

(a, (b, c)) ~ ((a, b), c)
a * (b * c) = (a * b) * c

a -> (b -> c) ~ (a, b) -> c
(c^b)^a = c^(b * a)

Mais je ne comprends pas le algébrique de l'égalité qui est analogue à:

(forall r . (a -> r) -> r) ~ a

Answer 1

C'est le fameux lemme de Yoneda pour le foncteur identité.

Vérifiez ce post pour lisible une introduction, et de toute catégorie de la théorie de manuel pour plus d'.

Brièvement, compte tenu de f :: forall r. (a -> r) -> r vous pouvez appliquer f id pour obtenir un a, et inversement, x :: a vous pouvez prendre ($x) pour obtenir de l' forall r. (a -> r) -> r.

Ces opérations sont mutuellement inverses. La preuve:

Évidemment ($x) id == x. Je vais montrer qu'

($(f id)) == f,

étant donné que les fonctions sont égales quand elles sont égales sur tous les arguments, prenons x :: a -> r et de montrer que

($(f id)) x == f x c'est à dire

x (f id) == f x.

Depuis f est polymorphe, il fonctionne comme une transformation naturelle; c'est la naturalité diagramme pour f:

               f_A
     Hom(A, A)  →  A
(x.)      ↓        ↓ x
     Hom(A, R)  →  R
               f_R

Donc, x . f == f . (x.).

Brancher l'identité, (x . f) id == f x. CQFD

Answer 2

(Réécrit pour plus de clarté)

Il semble y avoir deux parties à votre question. L'un est implicite, et demande à ce que le algébrique interprétation de l' forall est, et l'autre est de demander à propos de la suite/Yoneda transformation, qui sdcvvc la réponse déjà couverte assez bien.

Je vais essayer de répondre à l'algébrique interprétation de l' forall pour vous. Vous mentionnez que A -> B est B^A mais j'aimerais prendre une étape plus loin et d'élargir à B * B * B * ... * B (|A| temps). Bien que nous n'avons exponentiation comme une note répétée de la multiplication comme ça, il n'y a plus flexible de notation, ∏ (en majuscules Pi) représentant arbitraire de produits indexés. Il ya deux composantes à un Pi: la gamme de valeurs que nous voulons multiplier au cours, et l'expression qui nous sont multipliés. Par exemple, au plan de la valeur, vous pourriez exprimer la fonction factorielle en tant que fact i = ∏ [1..i] (λx -> x).

Aller retour dans le monde des types, nous pouvons voir l'opérateur exponentiel dans l' A -> B ~ B^A correspondance comme un Pi: B^A ~ ∏ A (λ_ -> B). Il dit que nous sommes à la définition d'un A-ary produit d' Bs, tels que l' Bs ne peut pas compter sur le particulier A nous avons choisi. Bien sûr, c'est équivalente à une simple élévation à la puissance, mais il nous permet de passer à des cas dans lesquels il y a une dépendance.

Dans le cas le plus général, nous obtenons des types dépendants, comme ce que vous voyez dans Agda ou Coq: dans Agda syntaxe, replicate : Bool -> ((n : Nat) -> Vec Bool n) est une application possible d'un type de Pi, ce qui peut être exprimé de façon plus explicite qu' replicate : Bool -> ∏ Nat (Vec Bool), ou encore en tant que replicate : ∏ Bool (λ_ -> ∏ Nat (Vec Bool)).

Notez que comme vous pouvez le deviner à partir de l'algèbre sous-jacente, vous pouvez fusionner les deux de l' ∏s dans la définition de l' replicate ci-dessus en un seul ∏ allant sur le produit cartésien des domaines: ∏ Bool (\_ -> ∏ Nat (Vec Bool)) est équivalent à ∏ (Bool, Nat) (λ(_, n) -> Vec Bool n) tout comme il le serait à la "valeur". C'est tout simplement uncurrying du point de vue de la théorie des types.

Je comprends votre question a été sur le polymorphisme, donc je vais arrêter d'aller sur des types dépendants, mais ils sont pertinents: forall en Haskell est à peu près équivalent à un ∏ avec un domaine de plus le type (genre) de types, *. En effet, la fonction-comme le comportement de polymorphisme peut être observée directement dans le noyau de GHC, les types comme capitale de lambda (Λ). En tant que tel, un type polymorphe comme forall a. a -> a n'est en fait qu' ∏ * (Λ a -> (a -> a)) (à l'aide de l'Λ notation maintenant que nous faisons la distinction entre les types et les valeurs), qui peut être agrandi à l'infini de produit (Bool -> Bool, Int -> Int, () -> (), (Int -> Bool) -> (Int -> Bool), ...) pour chaque type. L'instanciation de la variable type est tout simplement de la projection sur le bon élément de l' *-ary produit (ou de l'application du type de fonction).

Maintenant, pour le gros morceau que j'ai raté dans ma version originale de cette réponse: parametricity. Parametricity peut être décrit de plusieurs façons différentes, mais aucun de ceux que je connais (l'affichage des types de relations, ou (di)de naturalité dans la catégorie théorie) a vraiment une très algébrique de l'interprétation. Pour nos fins, si, il se résume à quelque chose d'assez simple: vous ne pouvez pas le faire correspondre à un modèle sur *. Je sais que GHC vous permet de le faire au niveau du type avec le type de familles, mais vous ne peut couvrir qu'une infime partie de l' * quand faire ça, donc il y a forcément toujours des points sur lesquels votre type de famille n'est pas défini.

Ce que cela signifie, du point de vue de polymorphisme, c'est que toute fonction de type F nous écrire en ∏ * F doit être constante (c'est à dire, de les ignorer complètement le type dont il est polymorphe plus) ou de passer du type inchangés. Ainsi, ∏ * (Λ _ -> B) est valide parce qu'il ignore son argument, et correspond à l' forall a. B. L'autre cas est quelque chose comme ∏ * (Λ x -> Maybe x), ce qui correspond à forall a. Maybe a, ce qui ne l'ignore pas, le type de l'argument, mais une seule "passe à travers". En tant que tel, ∏ A qui a une pertinence domaine A (comme lors de l' A = *) peuvent être considérées comme plus d'un A-ary indexé intersection (choisir les éléments communs dans toutes les instanciations de l'index), plutôt que d'un produit.

Surtout, au plan de la valeur, les règles de parametricity éviter tout drôle de comportement qui pourrait suggérer les types sont plus grandes qu'elles ne le sont vraiment. Parce que nous n'avons pas typecase, nous ne pouvons pas construire une valeur de type forall a. B qui fait quelque chose de différent, basé sur ce qu' a a été instancié. Ainsi, bien que le type est techniquement une fonction * -> B, il est toujours une fonction constante, et est donc équivalent à une seule valeur de B. À l'aide de l' ∏ interprétation, il est en effet équivalent à une infinie *-ary produit d' Bs, mais ceux - B valeurs doivent toujours être identique, de sorte que le produit infini est effectivement grand comme un seul B.

De même, bien qu' ∏ * (Λ x -> (x -> x)) (un.k.un., forall a. a -> a) est techniquement équivalent à un produit infini de fonctions, aucune de ces fonctions peut inspecter le type, de sorte que tous sont contraints de retourner uniquement leur valeur d'entrée et ne pas faire tout drôle d'affaires comme (+1) : Int -> Int lorsqu'il est instancié à l' Int. Car il y a un seul (en supposant un total de langage) fonction qui ne peut pas inspecter le type de son argument, mais doit renvoyer une valeur du même type, le produit infini est donc tout aussi grand comme une valeur unique.

Maintenant, à propos de votre question directe sur (forall r . (a -> r) -> r) ~ a. Tout d'abord, laissez exprimer votre ~ de l'opérateur de façon plus formelle. C'est vraiment isomorphisme, donc nous avons besoin de deux fonctions de va-et-vient, et un argument qu'ils sont inverses.

data Iso a b = Iso 
  { to   :: a -> b
  , from :: b -> a
  -- proof1 :: forall x. to (from x) == x
  -- proof2 :: forall x. from (to x) == x
  }

et maintenant nous exprimer votre question de départ, en termes plus formels. Votre question revient à construire un terme de la suite (impredicative, afin de GHC a de la difficulté avec elle, mais nous allons survivre) type:

forall a. Iso (forall r. (a -> r) -> r) a

Qui, à l'aide de mon ancienne terminologie, les montants d' ∏ * (Λ a -> Iso (∏ * (Λ r -> ((a -> r) -> r))) a). Une fois de plus, nous avons un produit infini qui ne peut pas inspecter son type d'argument. Par handwaving, nous pouvons affirmer que les seules valeurs possibles compte tenu de la parametricity règles (les deux autres épreuves sont respectés automatiquement) to et from sont ($ id) et flip id.

Si c'est insuffisant, c'est probablement parce que l'interprétation algébrique de forall n'a pas vraiment de rien ajouter à la preuve. C'est vraiment juste un bon vieux type de théorie, mais j'espère que j'ai été en mesure de fournir quelque chose qui se sent un peu moins catégorique que la Yoneda forme de celui-ci. Il est intéressant de noter que nous n'avons pas réellement besoin d'parametricity à écrire proof1 et proof2 - dessus. Parametricity seulement entre l'image lorsque nous voulons affirmer qu' ($ id) et flip id sont nos seules options pour to et from (dont nous ne pouvons pas prouver dans Agda ou Coq, pour cette raison).

Answer 3

Pour (tenter de) répondre à la question (qui est moins intéressant que les réponses à des questions plus générales soulevées), la question est mal formées en raison d'une "erreur de type"

Either ~ (+) 
(,)    ~ (*)
(->) b ~ flip (^)
()   ~ 1
Void ~ 0 

Ces tous les types de cartes de nombres entiers, et le type des constructeurs pour les fonctions sur les produits naturels. Dans un sens, vous avez un foncteur de la catégorie des types de la catégorie de produits naturels. Dans l'autre sens, vous "oubliez" les choses, puisque les types de préserver la structure algébrique alors que les produits naturels de la jeter. I. e. compte tenu de Either () () vous pouvez obtenir un environnement naturel unique, mais étant donné que ce qui est naturel, vous pouvez obtenir de nombreux types.

Mais cela est différent:

(forall r . (a -> r) -> r) ~ a

C'cartes d'un type vers un autre type! Il ne fait pas partie de la ci-dessus foncteur. C'est juste un isomorphisme dans la catégorie des types. Nous allons donc donner qu'un symbole différent, <=>

Maintenant, nous avons

(forall r . (a -> r) -> r) <=> a

Maintenant, vous notez que nous ne pouvons pas envoyer uniquement les types de nats et des flèches à flèches, mais aussi quelques isomorphisms à d'autres isomorphisms:

(a, (b, c)) <=> ((a, b), c) ~ a * (b * c) = (a * b) * c

Mais quelque chose de subtil qui se passe ici. Dans un sens, le dernier isomorphisme sur des paires est vrai parce que l'identité algébrique est vrai. C'est-à-dire que le "isomorphisme" dans celui-ci signifie simplement que les deux types sont équivalents sous l'image de notre foncteur pour les nats.

L'ancien isomorphisme nous avons besoin de prouver directement, qui est l'endroit où nous commençons à obtenir de la question sous-jacente-est, compte tenu de notre foncteur pour les nats, qu'est - forall r. carte? Mais la réponse est qu' forall r. n'est ni un type, ni de flèche entre les types.

En introduisant pourtout, nous avons déménagé loin de premiers types d'ordre. Il n'y a pas de raison de s'attendre à ce que toutes les doit tenir dans notre ci-dessus Foncteur, et en effet, il n'est pas.

Donc, nous pouvons explorer, comme d'autres, au-dessus, pourquoi l'isomorphisme détient (qui est lui-même très intéressant) -- mais, pour ce faire, nous avons abandonné le algébriques de base de la question. Une question qui peut être répondu, je pense, est, compte tenu de la catégorie de l'ordre supérieur des types et des constructeurs comme des flèches entre eux, quel est - il significatif Foncteur?

Edit: Alors maintenant, j'ai une autre approche qui montre pourquoi l'ajout de polymorphisme rend les choses aller de noix. Nous commençons par poser une simple question -- est-ce une donnée de type polymorphe avoir zéro ou plus de zéro habitants? C'est le type d'habitation problème, et des vents jusqu'à être, via Curry-Howard, un problème dans modifiés realizability, puisque c'est la même chose que de demander si une formule dans une logique qui est réalisable dans un modèle de calcul. Maintenant que cette page explique, c'est decidable dans le lambda calcul simplement typé, mais est PSPACE-complet. Mais une fois que nous passons à quelque chose de plus compliqué, par l'ajout de polymorphisme par exemple et le Système F, alors il va à indécidable!

Donc, si nous ne pouvons pas décider si un type arbitraire est habitée à tous, nous a clairement ne peut pas décider de la façon dont de nombreux habitants il a!

Answer 4

C'est une question intéressante. Je n'ai pas de réponse, mais c'était trop long pour un commentaire.

La signature de type (forall r. (a -> r) -> r) peut être exprimée comme moi qui le dit

Pour tout type r que vous vous souciez de nom, si vous me donnez une fonction qui prend en a , et produit un r, alors je vais vous donner en retour, un r.

Maintenant, ce qui a fonctionne pour tout type r, mais il peut être un spécifique de type a. Donc, la façon pour moi de tirer de cette astuce est d'avoir un a assis autour de quelque part, que je nourris à la fonction (qui produit un r pour moi) et puis j'ai la main qui r de nouveau à vous.

Mais si j'ai un a assis autour de moi, je pourrais vous le donner:

Si vous me donnez un 1, je vais vous donner un a.

ce qui correspond à la signature de type 1 -> a ou tout simplement a. Par cet argument informel, nous avons

(forall r. (a -> r) -> r) ~ a

La prochaine étape serait de générer le correspondant expression algébrique, mais je ne suis pas clair sur la façon dont le algébrique des quantités d'interagir avec la quantification universelle. On peut avoir besoin d'attendre d'un expert!

Answer 5

Quelques liens vers les nLab:

• Quantificateur universel, correspond dépendant du produit.

• Quantificateur existentiel, correspond dépendant de la somme (en fonction de la coproduct).

---

Ainsi, dans les paramètres de la catégorie de la théorie:

Type               | Modeled¹ as               | In category
-------------------+---------------------------+-------------
Unit               | Terminal object           | CCC
Bottom             | Initial object            |
Record             | Product                   |
Union              | Sum (coproduct)           |
Function           | Exponential               |
-------------------+---------------------------+-------------
Dependent product² | Right adjoint to pullback | LCCC
Dependent sum      | Left adjoint to pullback  |

1) dans la catégorie appropriée ─ CCC total et non polymorphes sous-ensemble de Haskell (lien), CPO pour les non-total traits de Haskell (lien), LCCC pour dépendante tapé langues.

2) forall de quantification est un cas spécial de l'dépendant du produit:

∀(x :: *). y[x] ~ ∏(x : Set)y[x]

où Set est l' univers de tous les petits types.