Système de types basé sur la théorie naïve des ensembles

Si je comprends bien, en informatique, les types de données ne sont pas basés sur la théorie des ensembles à cause de choses comme le paradoxe de Russell, mais comme dans les langages de programmation du monde réel, nous ne pouvons pas exprimer des types de données aussi complexes que "ensemble qui ne se contient pas", pouvons-nous dire qu'en pratique, le type est un ensemble infini de ses membres où l'appartenance à une instance est définie par un nombre de caractéristiques intrinsèques à ce type / ensemble (existence de certaines propriétés, méthodes)? Si non, quel serait le contre-exemple?

La principale raison pour éviter les ensembles dans la sémantique des types est qu'un langage de programmation typique nous permet de définir des fonctions récursives arbitraires. Par conséquent, quelle que soit la signification d'un type, il doit avoir la propriété virgule fixe. Le seul ensemble avec une telle propriété est l'ensemble singleton.

Pour être plus précis, une valeur définie de manière récursive de Type (où typiquement est un type de fonction) est définie par une équation de point fixe où peut être n'importe quel programme. Si est interprété comme l'ensemble alors nous nous attendrions à ce que chaque ait un point fixe. Mais le seul ensemble avec cette propriété est le singleton.τ τ v = Φ ( v ) Φ : τ → τ τ T f : T → T $v$$\tau$$\tau$$v = \Phi(v)$$\Phi : \tau \to \tau$$\tau$$T$$f : T \to T$$T$

Bien sûr, vous pourriez également réaliser que le coupable est la logique classique. Si vous travaillez avec la théorie des ensembles intuitionniste, il est cohérent de supposer qu'il existe de nombreux ensembles avec une propriété à point fixe. En fait, cela a été utilisé pour donner la sémantique du langage de programmation, voir par exemple

Alex Simpson, Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory , In Annals of Pure and Applied Logic, 130: 207-275, 2004.

Le sous - typage sémantique est basé sur une interprétation théorique sous-jacente des types, où le sous-typage est un sous-ensemble. Le travail original , je crois, est de Castagna dans le contexte du langage de traitement XML CDuce. Les types correspondent à des ensembles de documents XML. Les idées ont depuis été réappliquées au -calculus et aux objets et classes de calcul .$\pi$

À quelques exceptions près (dont Dave Clarke cite), la sémantique simple des types théoriques des ensembles est difficile à utiliser. La raison en est que l'abstraction des données ne joue pas très bien avec la sémantique de la théorie des ensembles.

Le problème de base est plus facilement visible dans un langage totalement purement fonctionnel avec des types polymorphes, et considérons le type polymorphe . En sémantique ensembliste naïve des types, nous interpréter l'espace fonctionnel que l' espace de fonction ensembliste, puis interpréter le quantificateur universel en tant que produit sur une (petite) univers des ensembles . C'est,$\forall \alpha.\; \alpha \to \alpha$$U$

Toutefois, notez que cette interprétation des types inclut des fonctions qui font quelque chose de différent à chaque élément de - nous pouvons branche sur pour donner une autre fonction dans pour chaque . En revanche, le type polymorphe ne contient que la fonction d'identité, car les seules opérations que le langage de programmation vous permettra d'effectuer au type celles qui fonctionnent à tous les types.U X → X X ∈ U $U$$U$$X \to X$$X \in U$$\alpha$

Cette sémantique ne peut donc (par exemple) justifier aucune optimisation basée sur le fait que l'identité est le seul habitant de .$\forall \alpha.\; \alpha \to \alpha$