Depois de aprender Haskell e outras linguagens FP não puras, decidi ler sobre a teoria das categorias. Depois de obter um bom entendimento da teoria das categorias, comecei a pensar em como os conceitos da teoria das categorias podem ser usados ​​para pensar em criar programas, mas não importa o quanto tentei, parece que esse não é o caminho a seguir.
Depois de passar muitas tentativas frustradas de relacionar a teoria das categorias ao projeto de programas , cheguei à conclusão de que:
A teoria das categorias é útil ao projetar uma linguagem de programação .
A teoria das categorias não é algo que você usa ao criar programas (mesmo quando usa uma linguagem que foi projetada com base nos princípios das categorias). Por exemplo: Ao programar em Haskell, você utilizará tipos, tipos de construtor, funções, funções de ordem superior etc. para projetar seu programa, não conceitos de teoria de categorias.
Em resumo, temos o sistema de camada abaixo (a ordem é baixa para alta):
Teoria da categoria -> Linguagem de programação -> Programa
Em uma camada específica, você usa os conceitos da camada subjacente imediata .
Este entendimento está correto? Caso contrário, e você acredita que, ao projetar programas , podemos usar diretamente os conceitos da teoria das categorias, consulte alguns artigos ou postagens de blog onde está sendo demonstrado.
NOTA: Ao projetar programas, quero dizer projetar programas com base em diferentes conceitos, como simultaneidade, paralelismo, reativo, passagem de mensagens etc.
Você considera as mônadas como parte da linguagem ou programas de programação? Setas; flechas?
Isso me parece uma questão filosófica, pelo menos em parte. Não sei se há uma única resposta correta. Um adepto da teoria das categorias aplicará a intuição adquirida durante a programação, outro favorecerá diferentes modos de pensar.
A maioria dos programas sendo escritos usa linguagens de programação não inspiradas na teoria das categorias. Até onde eu sei, o programador médio não está ciente da teoria das categorias e, portanto, a maioria dos programas (incluindo o sistema operacional e o navegador) não é inspirada em matemática superior.
@YuvalFilmus: A minha pergunta é voltado para linguagens de programação funcional
Veja também esta pergunta para algumas aplicações CS de monoids
Bem, isso depende do tipo de programa que você está tentando criar.
Se você está criando um programa de contabilidade para a loja de chocolates de sua tia, duvido muito que a teoria das categorias seja de grande utilidade.
Mas há, é claro, situações em que a teoria das categorias é extremamente útil no design de programas (com o que também quero dizer estruturas de dados, bibliotecas e assim por diante). Tais situações ocorrem principalmente quando os programas envolvidos são de natureza matemática.
Se você deseja escrever programas que computam números reais exatos e outras estruturas que ocorrem na análise matemática, a primeira pergunta a ser respondida é o que significa implementar corretamente um objeto matemático complicado (como uma função diferenciável, uma variedade, etc.) ) Aqui, ajuda muito conhecer algumas teorias e lógica de categorias, porque elas oferecem uma maneira sistemática de traduzir definições de estruturas matemáticas para especificações e implementações das estruturas de dados correspondentes. A palavra da moda que você deve procurar é a teoria da realização . Mas este é apenas um exemplo.
A melhor maneira de ver como a teoria das categorias é útil é olhar para programas escritos por pessoas que conhecem muita teoria das categorias (e matemática em geral). Um exemplo óbvio disso é Martín Escardó e seus funcionais impossíveis, por exemplo:
M. Escardó e P. Oliva: que jogos seqüenciais, o teorema de Tychonoff e a mudança de dupla negação têm em comum a programação funcional 2010, matematicamente estruturada, ACM Press. (com arquivos Haskell e Agda complementares )
Você pode reclamar que isso não é apenas teoria de categorias, mas também lógica e topologia. Tais queixas seriam severamente equivocadas. A melhor teoria das categorias é sempre misturada com outras coisas.
Por fim, eu desaconselharia a tirar grandes conclusões sobre a natureza das coisas com base em um pouco de leitura auto-atribuída.
Esse é exatamente o meu ponto. Se estou projetando um software de contabilidade, o sistema de tipos será minha linguagem para o design. Se eu estiver projetando um software matemático, usarei o sistema de tipos para representar os conceitos da teoria das categorias. O que basicamente indica que a teoria dos tipos OU sistemas de tipos são abstrações mais gerais do que a teoria das categorias.
Essa é uma afirmação ridícula. Acho que você talvez deva aprender um pouco mais antes de fazer declarações abrangentes como essa. Talvez você pode começar com existentialtype.wordpress.com/2011/03/27/the-holy-trinity
Eu não sou pesquisador, doutorado, cientista, matemático ou teórico de categorias; portanto, não fique chateado com minhas afirmações, elas não serão publicadas em periódicos científicos ou papéis de pesquisa. Eu sou apenas um programador que está tentando entender o outro lado da moeda. A propósito, obrigado pelo link.
Percebo isso, e é exatamente por isso que estou sugerindo que você seja cuidadoso ao tirar conclusões como você: você simplesmente não possui as informações necessárias para tirar essas conclusões. E é também por isso que te refiro a um post de Bob Harpher em vez de, digamos, a um livro técnico sobre a relação entre teoria de tipos e teoria de categorias. Estou tentando ajudar, mas esperaria, em troca, um pouco mais de sua reserva quando se trata de tirar grandes conclusões sobre a natureza de todo um ramo da matemática.
— 22313 Andrej Bauer
Por exemplo, você declarou que "a teoria dos tipos é uma abstração mais geral que a teoria das categorias". Este é um exemplo de declaração que você deve saber para não fazer com base em pouco conhecimento. Eu trabalho profissionalmente nessa área e até eu seria muito cuidadoso em fazer essa conclusão, ou a oposta.
As pessoas costumavam usar a TC para descrever os tipos de dados.
O tipo de dados foi definido por uma categoria específica cujos objetos são seqüências finitas de tipos (linguagem de especificação) e cujas setas eram projeções ou composições das operações do tipo de dados. Por exemplo, o objeto é o domínio e é o codomain da operação de envio de pilhas. Isso fornece sintaxe, mas você ainda não tem noção de semântica.
Uma álgebra, ou seja, uma instância do tipo, é um functor da teoria ao Ens, a categoria de conjuntos (pequenos). (Usamos "pequeno" para evitar o paradoxo de Russell, mas isso não importa muito.)
Acontece que as propriedades de fechamento das categorias correspondem a famílias de teorias lógicas. Por exemplo, se a categoria de teoria for fechada em produtos, o tipo de dados poderá ser axiomatizado por equações. Se a categoria da teoria for fechada com retrocessos, o tipo de dados poderá ser axiomatizado pelas sentenças de Horn.
Não tenho certeza se alguém presta mais atenção nisso. Eu pensaria que isso , e os links lá, explicariam mais detalhadamente.