Status quo da teoria da categoria e das mônadas na pesquisa teórica em ciência da computação?

Background . Sou um estudante de bacharel interessado em pesquisas relacionadas à teoria das categorias, mônadas e Haskell, e quero encontrar um tópico para a tese de bacharel nessa área.

Eu olhei para o jornal

Eugenio Moggi , “ Noções de Computação e Mônadas ”, 1991,

e ainda não entendo muito disso. Provavelmente vou precisar de algum tempo para entendê-lo completamente. Mas, antes de dedicar mais tempo ao estudo, quero entender melhor o campo e seu potencial de pesquisa. Recentemente, conversei com um professor meu sobre ele e ele me disse que as mônadas estavam na moda na comunidade de pesquisa nos anos 90, mas hoje em dia elas estão fora de moda.

Portanto , agora estou procurando trabalhos recentes relacionados a mônadas e estou me perguntando:

Em que áreas da ciência da computação teórica atualmente são feitas pesquisas relacionadas à teoria das categorias e às mônadas?
Que tipo de pesquisa foi construída ou proposta no trabalho de E. Moggi sobre mônadas na teoria da programação? Houve alguma pesquisa de acompanhamento ou em andamento relacionada ao seu trabalho?

reference-request pl.programming-languages big-picture ct.category-theory monad k.stm
fonte

Antes de respondermos a essa pergunta: não é de nível de pesquisa, é? Pode ser mais adequado para cs.stackexchange.com.

21315 Andrej Bauer #

@AndrejBauer Minha tese de bacharel não será de nível de pesquisa, mas minha pergunta aborda a pesquisa atual ou pelo menos a pesquisa realizada na última década.

k.stm

@AndrejBauer Eu discordo. O site irmão é principalmente para perguntas de trabalhos de casa, enquanto aqui é necessária uma opinião de um especialista.

Yuval Filmus

@ Kaveh Essa foi a edição drástica que você acabou de fazer. Você melhorou alguns pontos, mas agora não é mais a pergunta que eu estava fazendo. Quando tiver tempo amanhã, reverteremos algumas de suas alterações. Por exemplo, é importante para mim ter o histórico lá. Diga-me quais alterações você acha que são necessárias e por que, para que eu saiba o que não reverter.

k.stm

@Yuval, acho que muitas pessoas na Ciência da Computação discordariam totalmente do seu comentário de que é principalmente para trabalhos de casa e que especialistas não estão presentes na Ciência da Computação . Nesse caso, Andrej respondeu a mais de 100 perguntas sobre ciência da computação .

Kaveh

Respostas:

Houve uma série de desenvolvimentos no que diz respeito ao uso de mônadas na teoria da computação desde o trabalho de Eugenio Moggi. Não sou capaz de fornecer uma conta abrangente, mas aqui estão alguns pontos que estou familiarizado, outros podem concordar com suas respostas.

Exemplos específicos de mônadas

Você não precisa estudar teoria super-geral o tempo todo. Existem exemplos de mônadas muito interessantes e suficientemente complicadas para preencher uma tese de graduação inteira.

Gosto muito do blog de Dan Piponi, onde ele dá exemplos surpreendentes de como as mônadas podem ser usadas para misturar programação funcional e matemática. Procure seu trabalho sobre nós e trança através de mônadas, por exemplo.

Outro exemplo específico de mondas que vale a pena estudar foi dado por Martin Escardo e Paulo Oliva no contexto de funcionais de seleção, veja Funções de Seleção, Recursão de Barras e Indução Reversa , ou talvez para se interessar primeiro leia What Sequential Games, the Tychonoff Theorem and the O deslocamento de dupla negação tem em comum (arquivos Haskell e Agda associados aqui ).

Formação matemática

As mônadas são originárias da teoria das categorias e são muito mais antigas que Eugenio Moggi. Você pode estudar a teoria dos antecedentes se tiver uma inclinação matemática. Por exemplo, você pode atacar o teorema da monadicidade de Beck . Um cientista da computação teórico nunca pode saber muita matemática.

Variações sobre um tema

Você pode olhar para algo que não é estritamente mônadas.

Por exemplo, os idiomas de Connor McBride e Ross Paterson : a programação aplicativa com efeitos mostra como é possível generalizar as mônadas para algo que é praticamente relevante e perspicaz.

Ou você pode ver como as comonadas são usadas para modelar efeitos computacionais. Alguém deve sugerir algumas referências para este tópico, mas um bom começo pode ser os slides de David Overtone .

Teoria modal do tipo

Na teoria dos tipos de homotopia, bem como na teoria dos tipos em geral, as mônadas aparecem na forma da teoria modal dos tipos . Recentemente, a teoria do tipo modal foi considerada na teoria do tipo de homotopia porque os operadores de truncamento são exemplos de operadores modais. E existe a teoria coesa do tipo de homotopia, na qual os operadores modais (que são mônadas) desempenham um papel essencial.

Efeitos algébricos e manipuladores

[Aviso: soprando parcialmente minha própria buzina aqui.]

Há um tempo atrás, Gordon Plotkin e John Power observaram que muitos efeitos computacionais não são apenas mônadas, mas mônadas especiais decorrentes de teorias algébricas. Isso levou a um tratamento totalmente novo dos efeitos computacionais conhecidos como efeitos algébricos . Mais tarde, Gordon Plotkin e Matija Pretnar introduziram manipuladores e, juntamente com efeitos algébricos, formam uma teoria muito agradável de efeitos computacionais. Uma vantagem dessa abordagem é que as teorias algébricas podem ser facilmente combinadas, enquanto as mônadas não.

Você pode estudar como exatamente os efeitos algébricos se relacionam com as mônadas. Você pode ver como as pessoas implementaram efeitos e manipuladores algébricos, digamos na linguagem Eff ou em Haskell como uma biblioteca . Esta é uma pesquisa mais ou menos atual.

Andrej Bauer
fonte

Oi, obrigado por essa resposta! Eu cliquei no seu site sobre Eff, e parece que o link para Uma introdução a efeitos e manipuladores algébricos está desatualizado, ou seja, o arquivo eff-lang.org/handlers-tutorial.pdfestá ausente.

k.stm

Pedi a Matija para consertar o link. Enquanto isso, você pode acessar arxiv.org/abs/1203.1539 .

Andrej Bauer

Eu já sou. A propósito, você pode dar uma breve visão geral da teoria de background que preciso estudar para entender seu artigo? Conheço alguma teoria das categorias, cálculo lambda não tipado e alguma teoria elementar da computação e teoria elementar da programação (sei o que são semânticas denotacionais), mas não muito mais até agora. Por exemplo, já posso dizer na seção 3 do seu artigo que preciso examinar as regras de digitação (talvez, talvez, o cálculo lambda digitado). Desculpe se estou sendo agressivo aqui.

k.stm

Você deve saber um pouco sobre álgebra universal e / ou a teoria das teorias algébricas de Lavwere. Se você não conhece as regras de digitação, pode estudar um livro geral sobre linguagens de programação, como o TAPL de Benjamin Pierce ou os fundamentos Práticos de linguagens de programação de Bob Harper .

Andrej Bauer

Este artigo apresenta alguns trabalhos recentes importantes usando mônadas.

NietzscheanAI
fonte

Oi, obrigado pela sua resposta. Eu apreciaria um pouco de contexto, isto é, se você puder poupar tempo para dar alguns detalhes. (Na verdade, o papel tem boa introdução sobre o seu conteúdo, mas eu ainda gostaria de ver algum contexto para os seus arredores, como se há trabalhos relacionados e tal.)

k.stm