Les types sont-ils des propositions? (Quels sont exactement les types?)

25

J'ai beaucoup lu sur les systèmes de types et autres et je comprends à peu près pourquoi ils ont été introduits (afin de résoudre le paradoxe de Russel). Je comprends également à peu près leur pertinence pratique dans les langages de programmation et les systèmes de preuve. Cependant, je ne suis pas entièrement convaincu que ma notion intuitive de ce qu'est un type est correcte.

Ma question est, est-il valable de prétendre que les types sont des propositions?

En d'autres termes, la déclaration «n est un nombre naturel» correspond à la déclaration «n a le type« nombre naturel »», ce qui signifie que toutes les règles algébriques qui impliquent des nombres naturels sont valables pour n. (Autrement dit, les règles algébriques sont des déclarations. Ces déclarations qui sont vraies pour les nombres naturels le sont également pour n.)

Cela signifie-t-il alors qu'un objet mathématique peut avoir plusieurs types?

De plus, je sais que les ensembles ne sont pas équivalents aux types car vous ne pouvez pas avoir un ensemble de tous les ensembles. Puis-je prétendre que si un ensemble est un objet mathématique similaire à un nombre ou à une fonction , un type est une sorte d'objet méta-mathématique et par la même logique un genre est un objet méta-méta-mathématique? (dans le sens où chaque "méta" indique un niveau d'abstraction plus élevé ...)

Cela a-t-il un lien avec la théorie des catégories?

Rehno Lindeque
la source
5
Une question étroitement liée: preuves / programmes et propositions / types
Marc Hamann
1
Une autre discussion connexe: Classification des Lambda Calculi
Marc Hamann
Trouvé un autre bel article ici scientopia.org/blogs/goodmath/2009/11/17/…
Rehno Lindeque
1
Dans un certain sens, cela se résume à une question d'ontologie. Qu'est-ce qu'un ensemble, une proposition, etc. De plus, il y a beaucoup de gens qui pensent aussi aux types comme des ensembles. Si l'on veut être plus précis, on peut distinguer entre les petits types (qui sont des ensembles) et les types d'univers. Pour une bonne lecture qui concerne certaines de ces choses, je recommande le papier classique de Martin-Löfs "Théorie des types intuitionistes"
Tobias Raski
1
Quelqu'un devrait écrire une réponse du point de vue de la théorie des types d'homotopie.
Robin Green

Réponses:

20

Le rôle clé des types est de partitionner les objets d'intérêt en différents univers, plutôt que de considérer tout ce qui existe dans un univers. À l'origine, les types ont été conçus pour éviter les paradoxes, mais comme vous le savez, ils ont de nombreuses autres applications. Les types permettent de classer ou de stratifier des objets (voir l' article de blog ).

Certains fonctionnent avec le slogan que les propositions sont des types , donc votre intuition vous sert certainement bien, bien qu'il existe des travaux tels que des propositions comme [Types] de Steve Awodey et Andrej Bauer qui soutiennent le contraire, à savoir que chaque type a une proposition associée. La distinction est faite parce que les types ont un contenu informatique, contrairement aux propositions.

Un objet peut avoir plusieurs types en raison du sous - typage et des contraintes de type .

Les types sont généralement organisés dans une hiérarchie, où les types jouent le rôle du type de types, mais je n'irais pas jusqu'à dire que les types sont méta-mathématiques. Tout se passe au même niveau - c'est particulièrement le cas lorsqu'il s'agit de types dépendants .

Il existe un lien très fort entre les types et la théorie des catégories. En effet, Bob Harper (citant Lambek) dit que les logiques, les langues (où résident les types) et les catégories forment une sainte trinité . Citant:

Ces trois aspects donnent naissance à trois sectes d'adoration: la logique, qui donne la primauté aux preuves et aux propositions; Langues, qui donne la primauté aux programmes et aux types; Catégories, qui donne la primauté aux mappages et aux structures.

Vous devriez regarder la correspondance Curry-Howard pour voir le lien entre la logique et les langages de programmation (les types sont des propositions) et les catégories fermées cartésiennes , pour voir la relation entre la relation avec la théorie des catégories.

Dave Clarke
la source
Merci le premier lien a été particulièrement utile! Mark y informe qu'il existe une "relation totale <" sur les types. Cela signifie-t-il donc que toutes les "propositions" d'un type doivent également inclure toutes les "propositions" dans les types en dessous? Je m'attendais à ce que ce soit au moins une "relation partielle <" sur les types ....
Rehno Lindeque
1
Comme je l'ai lu, il y a un ordre total sur les atomes, qui était en place simplement pour s'assurer qu'il y a un nombre infini d'atomes.
Dave Clarke
Oh je vois que je me suis confondu entre l '"Axiome de compréhension" et l' "Axiome de l'infini" ... Un type 'nat' (le type de tous les nombres naturels) serait-il un "type de niveau 0 infini"?
Rehno Lindeque
3
La "sainte trinité" est vraiment due à Lambek. Cf. la discussion de la théorie des types dans Lambek & Scott (1986). J'ai entendu dire qu'à McGill, on parlait de la correspondance Curry-Howard-Lambek.
Charles Stewart
@Charles: Je conviens que Lambek est sous-crédité pour sa contribution massive, même si, ironiquement, c'est la lecture du livre de Lambek et Scott qui m'a convaincu que la "sainte trinité" est bidon: elle s'effondre en présence de potentiels non -Résiliation.
Marc Hamann