São proposições de tipos? (Quais são os tipos exatamente?)

25

Eu tenho lido muito sobre sistemas de tipos e coisas desse tipo e entendo por que eles foram introduzidos (para resolver o paradoxo de Russel). Eu também entendo aproximadamente sua relevância prática em linguagens de programação e sistemas de prova. No entanto, não estou totalmente confiante de que minha noção intuitiva do que é um tipo esteja correta.

Minha pergunta é: é válido afirmar que tipos são proposições?

Em outras palavras, a afirmação "n é um número natural" corresponde à afirmação "n tem o tipo 'número natural'", significando que todas as regras algébricas que envolvem números naturais são válidas para n. (Ou seja, dito de outra maneira, regras algébricas são declarações. Essas declarações que são verdadeiras para números naturais também são verdadeiras para n.)

Então, isso significa que um objeto matemático pode ter mais de um tipo?

Além disso, eu sei que conjuntos não são equivalentes a tipos porque você não pode ter um conjunto de todos os conjuntos. Eu poderia afirmar que, se um conjunto é um objeto matemático semelhante a um número ou uma função , um tipo é um tipo de objeto meta-matemático e, pela mesma lógica, um tipo é um objeto meta-meta-matemático? (no sentido de que cada "meta" indica um nível mais alto de abstração ...)

Isso tem algum tipo de link para a teoria das categorias?

Rehno Lindeque
fonte
5
Uma questão intimamente relacionados: Provas / Programas e Proposições / Tipos
Marc Hamann
1
Outra discussão relacionada: Classificação de Lambda Cálculos
Marc Hamann
Encontrei outro artigo interessante aqui scientopia.org/blogs/goodmath/2009/11/17/…
Rehno Lindeque 04/04
1
Em certo sentido, isso se resume a uma questão de ontologia. O que é um conjunto, uma proposição etc. Além disso, muitas pessoas pensam nos tipos como conjuntos também. Se alguém quiser ser mais preciso, pode distinguir entre tipos pequenos (que são conjuntos) e tipos de universo. Para um bom ler que as preocupações de algumas dessas coisas eu recomendo Martin-LOFS papel clássico "Intuitionistic Tipo Theory"
Tobias Raski
1
Alguém deve escrever uma resposta do ponto de vista da Teoria do Tipo de Homotopia.
9116 Robin Green

Respostas:

20

O papel principal dos tipos é dividir os objetos de interesse em diferentes universos, em vez de considerar tudo o que existe em um universo. Originalmente, os tipos foram criados para evitar paradoxos, mas como você sabe, eles têm muitas outras aplicações. Os tipos permitem classificar ou estratificar objetos (consulte a entrada do blog ).

Alguns trabalham com o slogan de que proposições são tipos , então sua intuição certamente lhe serve bem, embora existam trabalhos como Propositions as [Types] de Steve Awodey e Andrej Bauer que argumentam o contrário, ou seja, que cada tipo tem uma proposição associada. A distinção é feita porque os tipos têm conteúdo computacional, enquanto as proposições não.

Um objeto pode ter mais de um tipo devido a subtipagem e por coerção de tipo .

Os tipos geralmente são organizados em uma hierarquia, na qual os tipos desempenham o papel do tipo de tipos, mas eu não diria que os tipos são meta-matemáticos. Tudo está acontecendo no mesmo nível - esse é especialmente o caso quando se lida com tipos dependentes .

Existe uma ligação muito forte entre tipos e teoria de categorias. De fato, Bob Harper (citando Lambek) diz que Lógicas, Idiomas (onde os tipos residem) e Categorias formam uma trindade sagrada . Citação:

Esses três aspectos dão origem a três seitas de adoração: Lógica, que dá primazia a provas e proposições; Idiomas, que primam programas e tipos; Categorias, que dá primazia aos mapeamentos e estruturas.

Você deve olhar para a correspondência de Curry-Howard para ver o link entre a lógica e as linguagens de programação (tipos são proposições) e as categorias fechadas cartesianas , para ver a relação entre a relação com a teoria das categorias.

Dave Clarke
fonte
Obrigado, o primeiro link foi especialmente útil! Nele, Mark informa que existe uma "relação total <" sobre os tipos. Então, isso significa que todas as "proposições" de um tipo também devem incluir todas as "proposições" nos tipos abaixo deles? Eu esperava que ele seria pelo menos uma "relação parcial <" tipos mais ....
Rehno Lindeque
1
Enquanto eu o li, há uma ordem total sobre os átomos, o que existia apenas para garantir que haja um número infinito de átomos.
Dave Clarke
Oh, vejo que fiquei confuso entre o "Axioma da Compreensão" e o "Axioma do Infinito" ... Um tipo 'nat' (o tipo de todos os números naturais) seria um "tipo de nível 0 infinito"?
Rehno Lindeque 04/04
3
A "trindade sagrada" é realmente devida a Lambek. Cf. a discussão da teoria dos tipos em Lambek e Scott (1986). Ouvi dizer que em McGill se fala da correspondência de Curry-Howard-Lambek.
Charles Stewart
@ Charles: Eu concordo que Lambek é sub-creditado por sua contribuição maciça, mesmo que, ironicamente, estivesse lendo o livro de Lambek e Scott que me convenceu de que a "trindade sagrada" é falsa: se quebra na presença de potenciais -terminação.
Marc Hamann