Pedido de referência: Teoria da categoria conforme aplicável a sistemas de tipos

13

Eu continuo ouvindo sobre como é preciso aprender a teoria das categorias para realmente entender a teoria da linguagem de programação. Até agora, aprendi bastante PL sem nunca entrar no campo das categorias. No entanto, achei que era hora de dar o salto para ver o que estava faltando.

Infelizmente, nenhuma das fontes que consigo encontrar parece fazer conexões com sistemas ou programação de tipos. Eles dizem que é uma introdução à teoria das categorias para cientistas da computação, mas depois se desviam para um absurdo abstrato geral (digo isso com carinho) sem dar exemplos ou aplicações práticas.

Acho que minha pergunta é dupla:

  1. A teoria das categorias é essencial para a compreensão dos "conceitos profundos" no PL?
  2. O que é uma fonte que explica a teoria das categorias do ponto de vista de aplicativos práticos para digitar sistemas e programação?

Até agora, o mais longe que cheguei é de uma vaga concepção de functores (que não parecem estar relacionados a functores no ML, tanto quanto eu sei). Estou com medo da abstração que preciso manter em mente para entender as mônadas a partir de uma visão teórica da categoria.

Gardenhead
fonte
2
@Raphael É uma má idéia fazer uma pergunta que consiste em duas perguntas diferentes, apenas vagamente relacionadas entre si. Mas a pergunta 1. não é subjetiva. É antes um pedido de esclarecimento e explicação. Acho que a pergunta 2. foi feita no sentido de que ele está feliz com uma referência a um lugar onde é explicada, em vez de uma explicação real também.
Thomas Klimpel 28/09
2
No futuro, é melhor fazer apenas uma pergunta por postagem. Você pode fazer a pergunta 1 e, dependendo das respostas recebidas, decida se deve fazer a pergunta 2 separadamente. Isso geralmente faz as coisas correrem melhor.
DW
1
@Raphael Como a pergunta um é subjetiva? Pode ser difícil julgar - é isso que você quer dizer? E pode ter como resposta “Depende de que tipo de pessoa você é.” - é isso que você quer dizer? Ainda pode acontecer que seja definitivamente essencial ou definitivamente não essencial, certo? (E as pessoas parecem concordar que isso não é essencial.)
k.stm
1
@ k.stm A forma geral da pergunta me preocupa. Se alguém perguntasse: "A álgebra é essencial para entender os conceitos profundos das linguagens formais?", Sei que pessoas diferentes darão respostas diferentes - com base em suas preferências e gostos. Não espero que seja diferente aqui.
Raphael
1
@ Rafael Ok, eu entendi. Mas acho que são pessoas dando respostas subjetivas a uma pergunta objetiva. (Parece que as pessoas dizendo “Oh, eu estou bebendo cinco xícaras por dia e me sinto ótimo!” Quando perguntado se o café é saudável ou não.)
k.stm

Respostas:

15

A teoria das categorias não é necessária para entender as linguagens de programação, nem mesmo é necessário fazer pesquisas avançadas sobre linguagens de programação. A maioria das pessoas da linguagem de programação não conhece (muito) a teoria das categorias.

Os métodos teóricos de categoria têm sido úteis principalmente em uma pequena parte da pesquisa em linguagem de programação, principalmente na análise de programação funcional, particularmente desde a grande descoberta de Moggi de que alguns efeitos computacionais têm estrutura monádica. Nos anos 90, após o avanço de Moggi, muita pesquisa foi feita para estender os métodos categóricos a outras formas de linguagens de programação. No entanto, até onde sei, não foram encontrados métodos categóricos tão úteis para OO, computação simultânea, paralela e distribuída, computação temporizada ou compiladores. Por esse motivo, as pessoas abandonaram principalmente os métodos categóricos de extensão.

As abordagens categóricas da programação digitada funcionam bem em funções puras. De fato, alguns sistemas simples de digitação são categorias. Isso é descrito em por exemplo

Atualmente, há muito trabalho sobre tipos para processos simultâneos (por exemplo, tipos de sessão) e nada disso é de natureza categórica a partir de setembro de 2016.

Dito isto, nunca se pode saber muita matemática, e conhecer a teoria das categorias é útil. Portanto, é uma questão de custo / benefício. Se você gosta de matemática, se talvez você tenha um pouco de experiência em álgebra (por exemplo, qual é o grupo livre em um conjunto, anel livre etc.), aprender a teoria das categorias será fácil, e se você planeja fazer um trabalho inspirado em programação funcional, conhecer categorias será útil.

Finalmente, a teoria das categorias é uma bela matemática e vale a pena estudar simplesmente porque é muito elegante.


Veja a contribuição de Uday Reddy nesta discussão para uma visão diferente.

Martin Berger
fonte
"No entanto, até onde sei, métodos categóricos não foram tão úteis para ..." Esse é exatamente o meu problema. A semântica operacional pode descrever com precisão todos esses conceitos, então não senti que estava perdendo. Eu amo matemática, mas infelizmente minha formação em álgebra abstrata está faltando. Eu só entendo o básico básico das estruturas algébricas comuns. Isso tornou a teoria das categorias compreensiva especialmente complicada.
gardenhead
2
@ Gardenhead Então talvez o CT não seja tão útil para você. Se você quiser ler muitos artigos no espaço "Programação Funcional", incluindo trabalhos sobre tipos, muitos deles usarão a linguagem do CT.
Martin Berger
É esta uma duplicata?
Raphael
2
Além disso, sugiro o livro cs.unibo.it/~asperti/PAPERS/book.pdf "Categorias, tipos e estruturas", que aparentemente está esgotado, mas esse é um link para um pdf de um dos páginas dos autores, então eu acho que é legítimo.
precisa saber é o seguinte
6

Aprender a teoria das categorias é um enorme investimento de tempo, e a questão de saber se vale a pena é muito válida. Eu ainda lutam com isso também , e eu já sei por que eu deveria aprender. Eu escrevi:

Eu gostava da linguagem assembly quando comecei a programar, e a teoria dos conjuntos se parece com a linguagem assembly. A teoria das categorias é uma alternativa para contornar todos os preconceitos arraigados sobre a lógica e a teoria dos modelos incorporados à teoria convencional dos conjuntos de ZFC.

A idéia aqui é usar categorias em vez de conjuntos ou "bits não especificados" como uma possível semântica para uma dada teoria de tipos ou linguagem de programação. Por que alguém deveria querer fazer isso? Considere a dualidade entre uma ação e uma observação. Observações diferentes (ou pelo menos sua ordem no tempo) não interferem entre si (fora da mecânica quântica), mas isso não é necessariamente verdade para ações diferentes. Os preconceitos arraigados sobre a lógica incorporada na teoria dos conjuntos dificultam a modelagem de ações, em comparação com a modelagem de observações.


Não estou convencido de que realmente exista uma correspondência perfeita entre teoria das categorias e teoria dos tipos, como reivindicado aqui :

Por uma dualidade sintaxe-semântica, pode-se ver a teoria dos tipos como uma linguagem sintática formal ou cálculo para a teoria das categorias e, inversamente, pode-se pensar na teoria das categorias como fornecedora de semântica para a teoria dos tipos.

É verdade que a teoria das categorias pode fornecer semântica para a teoria dos tipos (o que pode ser realmente útil), mas duvido que a teoria dos tipos realmente forneça uma linguagem sintática formal suficientemente poderosa para expressar todos os cálculos feitos na teoria das categorias.


Na prática, a utilidade da teoria das categorias pode surgir sugerindo perguntas e analogias úteis. Mas a teoria das categorias também pode sugerir atividades e perguntas que acabam sendo apenas uma distração (perda de tempo) das questões realmente importantes. E você certamente pode aprender lógica e teoria dos tipos sem se preocupar com a teoria das categorias.

Thomas Klimpel
fonte
Obrigado por seus pensamentos. Suas razões para aprender a teoria das categorias parecem ser diferentes das minhas; seus interesses resultam de uma perspectiva puramente matemática, enquanto eu gostaria de ampliar minha compreensão dos tipos. Ainda assim, é bom saber que outras pessoas me consideram uma categoria difícil de abordar e aplicar
#