Pas de modèles théoriques naïfs de calcul lambda polymorphe?

Dans l'article de Philip Wadler sur les théorèmes gratuits, il déclare dans la section 2 sur la paramétrie que

il n'y a pas de modèles naïfs de théorie des ensembles du calcul lambda polymorphe

Dans le modèle naïf de la théorie des ensembles, les types sont des ensembles et les fonctions sont des fonctions de la théorie des ensembles, ce qui semble raisonnable. Alors pourquoi dit-il qu'il n'y a pas de modèles naïfs de théorie des ensembles du calcul lambda polymorphe?

functional-programming MK
la source

OK, je suis juste tombé sur ce papier: hal.inria.fr/inria-00076261/document . Je vais devoir passer au travers.

Cet article de Reynolds est en effet le bon article à lire! En omettant beaucoup de détails, cela se résume à: considérer data T = K ((T -> Bool) -> Bool). Ensuite, Tet ((T->Bool)->Bool)sont isomorphes. S'ils ont un modèle d'ensemble où ->désigne l'espace de fonction (en tant qu'ensemble), ce dernier a une cardinalité plus élevée, il ne peut donc pas être isomorphe à T. Ainsi, dans un modèle, nous devons interpréter ->différemment - par exemple comme l'espace des fonctions continues .

chi

J'ai répondu trop rapidement et répondu à la mauvaise question. Désolé pour ça. La raison pour laquelle le calcul lambda polymorphe n'a pas de modèle dans la théorie des ensembles naïfs est apparemment plutôt différente de celle du calcul lambda non typé.

Réponses:

$\Pi_{S\in\mathrm{Set}}S$ $\times$ $\rightarrow$

$\bf 2$ $T=\Pi_X(X\rightarrow {\bf 2})\rightarrow{\bf 2}$ $(T\rightarrow {\bf 2})\rightarrow {\bf 2}$ $\rightarrow$

Notez qu'un autre article, par Andrew Pitts, Polymorphism is Set Theoretic, Constructively , renverse quelque peu cette conclusion en montrant que la contradiction ci-dessus n'est possible que dans la théorie classique des ensembles, et qu'il existe plusieurs théories constructives des ensembles dans lesquels le polymorphisme peut être interprété avec les interprétations habituelles des espaces de fonctions et des produits. Plus particulièrement, ces «grands produits» existent dans les Topos efficaces, la plus complète des introductions étant donnée par Phoa .

cody
la source