Teoria das categorias (não) para programação?

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.

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.

As pessoas costumavam usar a TC para descrever os tipos de dados.

1. 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.
2. 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.)
3. 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.