A Teoria da categoria é útil para aprender programação funcional?

Estou aprendendo Haskell e sou fascinado pelo idioma. No entanto, eu não tenho matemática séria ou formação em CS. Mas sou um programador de software experiente.

Quero aprender a teoria das categorias para me tornar melhor em Haskell.

Quais tópicos da teoria das categorias devo aprender para fornecer uma boa base para o entendimento de Haskell?

Em uma resposta anterior no site de Teoria da Computação , eu disse que a teoria das categorias é o "fundamento" da teoria dos tipos. Aqui, eu gostaria de dizer algo mais forte. A teoria das categorias é uma teoria dos tipos . Por outro lado, a teoria dos tipos é a teoria das categorias . Deixe-me expandir esses pontos.

A teoria das categorias é a teoria dos tipos

Em qualquer linguagem formal digitada, e até mesmo em matemática normais usando a notação informal, acabamos de declarar funções com tipos . Por escrito, está implícita a idéia de que A e B são algumas coisas chamadas "tipos" ef é uma "função" de um tipo para outro. A teoria das categorias é a teoria algébrica de tais "tipos" e "funções". (Oficialmente, a teoria da categoria os chama de "objetos" e "morfismos", para evitar pisar nos dedos da teoria dos conjuntos dos tradicionalistas, mas cada vez mais vejo teóricos da categoria jogando tanta cautela ao vento e usando os termos mais intuitivos: "type "e" função ". Mas,$f : A \to B$$A$$B$$f$

Todos nós fomos educados sobre a teoria dos conjuntos desde o ensino médio. Então, estamos acostumados a pensar em tipos como e B como conjuntos e funções como f como mapeamentos teóricos de conjuntos. Se você nunca pensou neles dessa maneira, está em boa forma. Você escapou da lavagem cerebral com teoria dos conjuntos. A teoria das categorias diz que existem muitos tipos de tipos e muitos tipos de funções. Portanto, a ideia de tipos como conjuntos é limitadora. Em vez disso, a teoria das categorias axiomatiza tipos e funções de maneira algébrica. Basicamente, é isso que a teoria das categorias é. Uma teoria dos tipos e funções. Fica bastante sofisticado, envolvendo altos níveis de abstração. Mas, se você puder aprender, adquirirá uma compreensão profunda dos tipos e funções.$A$$B$$f$

Teoria dos tipos é teoria das categorias

Por "teoria dos tipos", refiro-me a qualquer tipo de linguagem formal digitada, baseada em regras rígidas de formação de termos que garantem que tudo seja verificado. Acontece que, sempre que trabalhamos em tal linguagem, estamos trabalhando em uma estrutura teórica da categoria. Mesmo se usarmos notações da teoria dos conjuntos e pensarmos teoricamente, ainda assim escreveremos coisas que fazem sentido categoricamente. Esse é um fato surpreendente .

Historicamente, Dana Scott pode ter sido a primeira a perceber isso. Ele trabalhou na produção de modelos semânticos de linguagens de programação com base no cálculo lambda digitado (e não tipado). Os modelos tradicionais de teoria dos conjuntos eram inadequados para esse propósito, porque as linguagens de programação envolvem recursão irrestrita, à qual falta a teoria dos conjuntos. Scott inventou uma série de modelos semânticos que capturaram fenômenos de programação e chegou à conclusão de que digitar o cálculo lambda representava exatamente uma classe de categorias denominadas categorias fechadas cartesianas . Existem muitas categorias fechadas cartesianas que não são "teóricas dos conjuntos". Mas o cálculo lambda digitado se aplica a todos eles igualmente. Scott escreveu um belo ensaio chamado " Relacionando teorias do cálculo lambda""explicando o que está acontecendo, partes das quais parecem estar disponíveis na Web. O artigo original foi publicado em um volume chamado" To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism ", Academic Press, 1980. Berry and Curien chegou à mesma conclusão, provavelmente de forma independente: eles definiram uma máquina abstrata categórica (CAM) para usar essas idéias na implementação de linguagens funcionais, e a linguagem implementada foi chamada "CAML", que é a estrutura subjacente do F # da Microsoft .

$\times$$\to$$List$exatamente para formalizar o conceito de funções polimórficas. Eles os chamavam de "transformações naturais", "naturais" porque são os únicos que você pode escrever de maneira correta usando variáveis ​​de tipo. Assim, pode-se dizer que a teoria das categorias foi inventada precisamente para formalizar linguagens de programação polimórficas, mesmo antes da criação das linguagens de programação!

Um tradicionalista da teoria dos conjuntos não tem conhecimento dos functores e transformações naturais que estão ocorrendo sob a superfície quando ele usa notações da teoria dos conjuntos. Mas, enquanto ele estiver usando fielmente o sistema de tipos, ele estará realmente fazendo construções categóricas sem estar ciente delas.

Tudo dito e feito, a teoria das categorias é a teoria matemática por excelência de tipos e funções. Portanto, todos os programadores podem se beneficiar ao aprender um pouco da teoria das categorias, especialmente programadores funcionais. Infelizmente, não parece haver nenhum livro de texto sobre a teoria das categorias direcionado especificamente aos programadores. Os livros da "teoria das categorias para ciência da computação" geralmente são direcionados a estudantes / pesquisadores teóricos da ciência da computação. O livro de Benjamin Pierce, teoria básica das categorias para cientistas da computação, é talvez o mais legível deles.

No entanto, existem muitos recursos na web, direcionados a programadores. A página da Haskellwiki pode ser um bom ponto de partida. Na Midlands Graduate School , temos palestras sobre teoria das categorias (entre outras). O curso de Graham Hutton foi atrelado a um curso "iniciante", e o meu foi atrelado a um curso "avançado". Mas ambos cobrem essencialmente o mesmo conteúdo, indo a profundidades diferentes. A Universidade de Chalmers tem uma boa página de recursos sobre livros e notas de aula de todo o mundo. O entusiasta blog de "sigfpe" também fornece muitas boas intuições do ponto de vista de um programador.

Os tópicos básicos que você gostaria de aprender são:

• definição de categorias e alguns exemplos de categorias
• functores e exemplos deles
• transformações naturais e exemplos delas
• definições de produtos, coprodutos e expoentes (espaços funcionais), objetos iniciais e terminais.
• adjuntos
• categorias mônadas, álgebras e kleisli

Minhas anotações de palestras na Midlands Graduate School abordam todos esses tópicos, exceto o último (mônadas). Atualmente, existem muitos outros recursos disponíveis para mônadas. Portanto, isso não é uma grande perda.

Quanto mais matemática você souber, mais fácil seria aprender a teoria das categorias. Como a teoria das categorias é uma teoria geral das estruturas matemáticas, é útil conhecer alguns exemplos para avaliar o significado das definições. (Quando aprendi a teoria das categorias, tive que criar meus próprios exemplos usando meu conhecimento da semântica da linguagem de programação, porque os livros-texto padrão só tinham exemplos matemáticos, dos quais eu não sabia nada.) Então veio o brilhante livro de Lambek e Scott chamaram " Introdução à lógica categórica"que relacionou a teoria das categorias aos sistemas de tipos (o que eles chamam de" lógica "). Agora é possível entender a teoria das categorias apenas relacionando-a aos sistemas de tipos, mesmo sem conhecer muitos exemplos. Muitos dos recursos mencionados acima usam isso abordagem para explicar a teoria das categorias.

Vou tentar mantê-lo curto e doce. Existe uma correspondência informal entre os programas Haskell e certas classes de categorias, que podem ser formalizadas com algum trabalho. Essa correspondência é conhecida como correspondência de Curry-Howard-Lambek e relaciona-se:

1. Tipos de haskell com objetos da categoria
2. $A\rightarrow B$ $f\colon A\rightarrow B$
3. Tipos de dados algébricos com objetos iniciais
4. Digite construtores com functors
5. etc

A lista continua, mas um ponto crucial é que você pode definir coisas como mônadas e álgebras na teoria das categorias e criar noções que são úteis para os matemáticos, mas também difundidas na prática da programação Haskell.

Não tenho certeza de qual livro recomendar, pois não encontrei um livro introdutório completamente satisfatório sobre categorias para cientistas da computação. Você pode experimentar categorias, tipos e estruturas de Asperti e Longo. A idéia é aprender definições básicas até complementos e, em seguida, talvez tente ler alguns dos excelentes blogs disponíveis para tentar entender esses conceitos.

Repetindo o conselho da @Jed, recomendo que você faça sua declaração

I want to learn category theory so I can become better at Haskell.

de cabeça para baixo: aprenda Haskell, desenvolvendo sua intuição de programação. Quando você é um guru de PF, pode ser mais fácil entender a teoria das categorias (se você ainda se importa).

A teoria das categorias é simples para alguém com ampla educação matemática (grupos, anéis, módulos, espaços vetoriais, topologia etc.). Sem esse pano de fundo, a teoria das categorias é quase impenetrável. A beleza da teoria das categorias é que ela unifica muitas coisas aparentemente não relacionadas (por exemplo, adjuntos à esquerda de functores esquecidos incluem grupos livres, álgebras envolventes universais, compactações Stone-Cech, abelianizações de grupos, ...) e, assim, reduz a complexidade. Mas se você não estiver familiarizado com os vários exemplos que a teoria das categorias unifica, a teoria das categorias é apenas uma camada adicional de complexidade que dificulta sua vida.

Na minha experiência, o aprendizado é mais fácil com base nas coisas que já se sabe. Como desenvolvedor de software, você sabe muito sobre programação, e a programação Haskell não é tão diferente de outras programações, então minha recomendação é abordar Haskell de um ponto de vista pragmático da programação, ignorando a teoria das categorias. A parte da teoria das categorias que existe em Haskell, por exemplo, algum suporte para mônadas, é muito mais fácil para um programador entender sem desviar-se da teoria das categorias. Afinal, as mônadas são meramente composição generalizada (e você já usou mônadas em sua prática de programação - embora sem saber o que você fez), e Haskell não suporta realmente mônadas de verdade, pois não impõe as leis monádicas.

Uma resposta curta: não [mas isso é apenas uma opinião]

Não vá à Teoria da Categoria ou a qualquer outro domínio teórico para se tornar bom em Haskell. Aprenda técnicas de programação funcional, como recursão da cauda, ​​mapa, redução e outras. Leia o máximo de código possível. Implemente o máximo de idéias possível. Se você tiver problemas, leia e leia.

Se você deseja uma boa referência teórica para aprender Haskell e outros paradigmas de programação funcional, consulte: Uma introdução à programação funcional através do cálculo Lambda, Greg Michaelson (disponível on-line). ... Existem outros livros semelhantes.

Aqui está um post (longo) do blog, que fornece motivação sobre como as idéias da teoria da categoria são relevantes para a programação prática: http://cdsmith.wordpress.com/2012/04/18/why-do-monads-matter/

A teoria das categorias é um ramo da matemática muito sofisticado e, ao dominá-lo, unificará a maioria de seus aprendizados anteriores, tornando-os instâncias dos mesmos objetos abstratos. Portanto, é muito útil e muito intuitivo. Mas é vasto e amplo, e você se encontrará com muitos conceitos novos que nem sequer sabem qual é adequado para suas necessidades e qual deve ser ignorado. Portanto, sua abordagem proposital precisa de escolha entre conceitos; caso contrário, dominá-la inevitavelmente precisa de muito tempo e não é realmente um domínio de auto-estudo.

A propósito, sugiro um ponto de partida muito bom para o seu propósito de estar aqui .