As sutilezas da correspondência entre teoria dos tipos e teoria das categorias estão fora do meu conhecimento. No entanto, por minha ingênua compreensão da relação entre as duas disciplinas historicamente convergentes, a segunda substitui inteiramente a primeira. Nesse caso, a linguagem e as descrições formais / gráficas usadas pelos teóricos da categoria substituem as dos teóricos do tipo? E deveriam (por exemplo, em pedagogia e publicação acadêmica)?
Diferentes formalismos podem inspirar novas perspectivas e estabelecer conexões conceituais nuas que, de outra forma, poderiam ser obscuras. No entanto, uma multiplicidade de dialetos provavelmente também limita o tamanho de uma audiência receptiva e, se uma abordagem poliglota for adotada, a duração e a complexidade da exposição serão compostas.
Se a teoria das categorias subsume a teoria dos tipos, as diferenças dialéticas das duas disciplinas devem ser mantidas e, em caso afirmativo, por quê? Por uma questão de valor histórico ou cultural? Reter diferenças diferentes, porém salientes, de ênfase instrucional ou teórica? O que podem ser isso?
fonte
Respostas:
Como você diz que "as sutilezas da correspondência entre teoria dos tipos e teoria das categorias estão fora do seu conhecimento", talvez a melhor maneira de entender a correspondência seja ler exposições não técnicas sobre o assunto. Eu posso recomendar dois:
Steve Awodey, De Conjuntos a Tipos, a Categorias, a Conjuntos , Em: Sommaruga G. (eds) Teorias Fundamentais da Matemática Clássica e Construtiva. The Western Ontario Series in Philosophy of Science, vol. 76. Springer, Dordrecht ( pré-impressão gratuita aqui )
A postagem de blog de Robert Harper, The Holy Trinity , e também veja esses slides .
Suponho que a lição a tirar é que cada abordagem tem algo a oferecer e que elas funcionam melhor juntas, e não tanto se você tentar substituir ou substituir uma pela outra.
fonte
Minha opinião é mais ou menos semelhante à do chi. Vejo a teoria das categorias como (grosso modo) ser a teoria dos tipos, o que é a teoria dos modelos para a lógica. Algumas das consequências disso são: primeiro, cada uma pode existir de forma autônoma. De fato, a teoria dos tipos antecede a teoria das categorias e a criação da teoria das categorias não foi motivada por essas preocupações. Segundo, muitas das distinções da teoria da teoria / teoria dos modelos estão propositalmente tentando desfocar são de interesse primário na teoria / lógica dos tipos.
Como um exemplo muito básico, todas as apresentações dos axiomas de um grupo dão origem à mesma classe de modelos (ou seja, grupos). Do ponto de vista da álgebra universal, uma variedade (no sentido da álgebra universal ou uma categoria algébrica finitária da perspectiva do TC) esquece sua apresentação. Enquanto isso, da perspectiva da lógica equacional, a apresentação é tudo o que existe. Um tópico computacional primário aqui é a unificação E, que opera inteiramente no nível da lógica equacional, isto é, a apresentação.
Isso é típico. Dizemos que o cálculo lambda simplesmente digitado (com produtos) (STLC) é a linguagem interna das categorias fechadas cartesianas, mas na verdade é apenas uma apresentação da linguagem interna e nem mesmo a mais "direta". A Máquina Abstrata Categórica (CAM) é sem dúvida uma representação mais "direta". Mesmo com o STLC, as setas da categoria sintática correspondente sãoβη classes de equivalência de termos lambda! (Mas veja isso .) Então, de alguma forma, descrevemos diretamente a categoria sintática como uma estrutura matemática cujos conjuntos de tarefas coincidem por coincidência comβη classes de equivalência de termos STLC e não têm conteúdo computacional , ou precisamos entender o STLC externo à teoria das categorias, ou precisamos falar em vez de apresentações de categorias fechadas cartesianas que, adotando uma abordagem bastante natural, levarão a algo CAM -gostar. No último caso, a igualdade de flechas se torna algo como um problema de unificação eletrônica. Compreender e simplificar esse processo, além de colocar a fachada mais ergonômica do STLC na frente dele, requer técnicas que são a base da lógica e da teoria dos tipos, mas que não são particularmente naturais na teoria das categorias.
Uma imagem extremamente simplificada que pode dar uma idéia melhor de como a teoria das categorias e a teoria dos tipos se inter-relacionam é a seguinte. Você pode imaginá-los como duas dimensões. As ferramentas, técnicas e notações da teoria dos tipos são voltadas para o movimento vertical entre diferentes apresentações do mesmo objeto, enquanto as ferramentas, técnicas e notações da teoria das categorias são voltadas para o movimento horizontal entre diferentes objetos matemáticos. Você pode até dizer que uma categoria é uma linha vertical inteira e que a teoria da categoria fala em mover uma linha vertical para outra, mas não como os pontos das duas linhas correspondem. Nesta imagem, a teoria da categoria nem é capaz de falar sobre as distinções que a teoria dos tipos está fazendo, mas isso é intencional, porque significa que o mapeamento arbitrariamente complicado de pontos em uma linha vertical para pontos em outra é apenas irrelevante para o que a teoria da categoria se importa e pode ser ignorada.
No meu post de blog, Teoria das categorias, sintaticamente , descrevo uma abordagem que faz a teoria das categorias parecer mais com a teoria dos tipos (e não o contrário). Sem surpresa, o que realmente estou discutindo são apresentações de categorias. Além disso, você pode ver aspectos da normalização entrando em cena, por exemplo, na minha discussão sobre "teorias do produto", mesmo que esse não seja o foco de todo esse post em particular.
fonte