Qual é a "pergunta" que a teoria da linguagem de programação está tentando responder?

10

Estou interessado em vários tópicos como Lógica Combinatória, Cálculo Lambda, Programação Funcional há algum tempo e os tenho estudado. No entanto, diferentemente da "Teoria da computação", que se esforça para responder à questão da "computabilidade", isto é, coisas que podem / não podem ser computadas com várias restrições, estou lutando para encontrar o análogo para "Teoria da programação"

A Wikipedia descreve como:

A teoria da linguagem de programação (PLT) é um ramo da ciência da computação que lida com o design, implementação, análise, caracterização e classificação de linguagens de programação e seus recursos individuais.

É como dizer "tudo" que não é realmente específico.

A progressão comum dos tópicos é geralmente assim:

Lógica combinada> Cálculo lambda> Teoria de tipos Martin Lof> Cálculo lambda digitado> (Algo acontece aqui)> Linguagens de programação desenvolvidas - que têm muito pouca conexão com CL /λ

Eu posso ver a "matemática" subjacente envolvida com CL / e provas interessantes que surgem como resultado, incluindo o teorema de Church-Rosser, e isso é interessante. No entanto, estou lutando para entender o "objetivo final" de todo esse empreendimento? Qual é o Santo Graal da PLT, se você preferir? Por enquanto, parece apenas estar coçando uma coceira intelectual, mas não posso realmente atravessar a ponte da pesquisa / teoria para algo prático.λ

Nota: Eu o levanto até usar o -calc para provas de indecidibilidade. Mas além de sua aplicabilidade à "computabilidade", simplesmente não entendo e estou tendo dificuldades para entender a necessidade de pesquisa em PLT a partir desse ponto de vista restrito. Existem livros existentes, referências que possam esclarecer o "quadro geral" do PLT?λ

Doutorado
fonte
11
Você está totalmente ignorando faixas inteiras de PLT em sua "progressão comum". Por alguma razão, sua visão parece estar distorcida pelo -calculus e pela teoria dos tipos. Vamos dar uma olhada nos artigos aceitos pelo POPL 2019 : programação aleatória simultânea, programação probabilística, montagem verificável, efeitos algébricos, redes neurais de certificação, modelos de memória fraca de PL e hardware, programação quântica, etc. Muitas coisas que não são "apenas" teoria dos tipos ", você não diria? λ
21319 Andrej Bauer
Você está 100% correto. Por isso, chamei meu "POV estreito". Eu estou familiarizado com os "outros tópicos" apenas lendo aqui e verificando os procedimentos do SIGPLAN / POPL. Ainda não encontrei uma "referência / livro holístico" que ofereça uma visão geral abrangente do PLT, que inclua os tópicos mencionados. O bit da teoria dos tipos é apenas do "meu" POV de (criando?) Linguagens de programação. Você teria algumas dicas que poderiam fornecer introduções de alto nível para as várias áreas do PLT para obter uma visão geral geral? Estou curioso para saber quais "modelos" subjacentes eles usam e como? todo lugar? λ
PhD
2
@PhD Não há apresentações de alto nível para as várias áreas da PLT que você deseja, c'est la vie ! Talvez um dia isso mude. Mas não prenda a respiração. O campo está evoluindo rapidamente e se diferenciando em subcampos. Outros modelos simples populares incluem -calculus, semântica operacional estrutural, cálculos imperativos simples (como a linguagem WHILE) e muitos outros. Muitas vezes, inventa-se um cálculo de brinquedo para se adequar ao domínio de aplicação. π
22819 Martin Berger

Respostas:

13

O objetivo geral do PLT é tornar a engenharia de software industrial (em um sentido geral) mais barata (também em um sentido geral), otimizando a ferramenta mais importante (linguagens de programação) e o ecossistema de ferramentas associado.

Algumas razões pelas quais a matemática está envolvida:

  • Os PLs são altamente não triviais e não está claro se eles fazem a coisa certa sem provas. A matemática fornece um modelo simplificado de linguagens de programação reais. Esse modelo nos permite estudar linguagens de programação reais em uma configuração muito simplificada, removendo (espero) a maioria dos problemas que já estão no nível do modelo. Atualmente, linguagens de programação reais são matematicamente intratáveis. Em outras palavras: lambda-calculus é a mosca da fruta, a E. Coli, a vaca esférica da PLT.

  • O PLT carece de métodos empíricos adequados, o que seria bom / melhor, portanto a matemática é feita como um substituto.

  • A matemática é linda e profunda.

  • A matemática fornece uma metodologia de pesquisa simples, testada e testada, importante para ajudar os alunos de doutorado a se formarem. Normalmente, algumas variantes de, por exemplo: Investigue o recurso PL XYZ adicionando-o ao cálculo lambda. Adicione tipos simples para XYZ e comprove a solidez do tipo. Adicione genéricos para XYZ e comprove a solidez do tipo. Prove um teorema da parametridade para genéricos XYZ. Adicione tipos dependentes para XYZ e comprove a solidez do tipo. Desenvolva uma inferência de tipo parcial para tipos dependentes de XYZ. Adicione tipos graduais para XYZ e comprove a solidez do tipo. Adicione contratos para XYZ. Cada um deles é um papel. Você pode parar se o seu aluno de doutorado ou pós-doutorado ficar sem tempo. Cada uma das opções acima é interessante e fornecerá informações sobre genéricos, parametridade, inferência de tipo etc. Esse pipeline é um ótimomaneira de navegar pelas águas difíceis de todas as linguagens de programação possíveis. Uma segunda maneira de aprender é implementar linguagens em um compilador, mas isso é menos tratável para um indivíduo.

Se PLT é necessário é uma pergunta interessante. A maioria dos programadores parece achar que não. Eles estão errados: a maioria das linguagens desenvolvidas por programadores sem experiência em PLT (por exemplo, Javascript, PHP) começa terrível e comete todos os erros que os teóricos da PL aprenderam há muito tempo a evitar. Se um PL desenvolvido por um amador atinge o mainstream, os teóricos do PL precisam de uma década ou mais para consertar as falhas óbvias (por exemplo, reformando um sistema de tipagem estática, consulte Typescript). Deixe-me resumir esta situação:

 Every successful programming language ends up being ML! Either because 
 it was designed by a PL theorist as ML from the start, or because a 
 decade of painful evolution removes all the obvious flaws, leaving ML. ;-)

Além disso: Esse estado de coisas é inteiramente culpa do PLT, porque, como a maioria deles não possui experiência em programação industrial, realmente não sabe quais são os problemas dos engenheiros de software que trabalham. Em particular, por razões sociológicas, a maioria dos teóricos da PL pensa que a programação funcional pura em linguagens como a Agda é a solução para todos os problemas, o que não resiste ao escrutínio.

Martin Berger
fonte
11
@ MartinBerger: O CompCert conta como um exemplo de capacidade de lidar com uma linguagem de programação do mundo real "teoricamente"? Caso contrário, quão alto você está definindo a fasquia, porque o CompCert é bastante impressionante.
21319 Andrej Bauer
2
@MartinBerger: Por favor, considere enfraquecer "a maioria dos teóricos da PL pensa que a programação funcional pura em linguagens como a Agda é a solução para todos os problemas", porque esse é apenas o seu discurso e desabafo. Para iniciantes, mesmo se você olhar para os tópicos que estão presentes no ICFP e no POPL, a maioria é sobre linguagens de programação impuras .
21319 Andrej Bauer
5
@ PhD: há muito mais no PLT do que a teoria dos tipos. É apenas que a teoria dos tipos é a primeira coisa que você percebe porque é uma das principais ferramentas do PLT.
21319 Andrej Bauer
11
@AndrejBauer CompCert, CakeML etc são impressionantes, mas estão distantes de compiladores amplamente usados ​​como LLVM, GCC etc. Além disso, os compiladores, ao contrário de qualquer software do mundo real, possuem uma especificação (tipo de) que você simplesmente não faz na engenharia de software industrial normal. Sem mencionar que grande parte do trabalho inicial de Xavier no CompCert consistia em precisar a especificação.
Martin Berger
2
@PhD Em relação a "" radicalmente mais produtivo "do que> não PLT C / C ++, Java, C #", lembre-se de que se você observar essas linguagens, mais especificamente, sua evolução ao longo do tempo, quase tudo o que adquiriram ao longo do tempo tempo, por exemplo, lambdas, mônadas (LINQ), correspondência de padrões, inferência de tipo parcial vem do PLT. A equipe de C # possui PhDs em PLT. Na verdade, eles tentaram me contratar em algum momento. A entrevista de emprego me estava tentando convencer Anders Heijlsberg que C # precisa de genéricos, que ele não gostava na época ...
Martin Berger