Aplicações diárias da teoria dos tipos

10

Quero entender a teoria dos tipos, mas primeiro preciso saber como aplicá-la. Poderia haver mais aplicações não óbvias da teoria dos tipos, além dos sistemas de tipos na programação? Poderia haver outras aplicações, digamos, em perfis de personalidade e afins?

type-theory applied-theory Tamad Lang
fonte
2
Por que algo precisa ter aplicativos fora do que foi inventado?
Raphael
3
Fundamentos da matemática? As pessoas também usaram a teoria dos tipos para formalizar coisas como teoria do domínio sintético, topologia etc. Há também o trabalho de Chris Martens sobre o uso de ferramentas teóricas dos tipos para modelar a narrativa narrativa. Link da dissertação
Daniel Gratzer
11
Você poderia esclarecer as contagens como um aplicativo?
Jake #
4
Não estou convencido de sua premissa. Suponha que alguém tenha dito: "Quero entender a engenharia automotiva, mas primeiro preciso saber para que posso usar um carro. Poderia haver mais aplicações não óbvias de carros além do transporte?" Eles recebem respostas dizendo que algumas pessoas dormem em seus carros, e Ansel Adams usou o dele como plataforma para tirar fotos . Bem, isso é ótimo, mas não ajuda ninguém a entender engenharia e é provável que leve nosso aluno hipotético a projetar carros com assentos reclináveis ​​e suspensão muito rígida.
David Richerby
3
O fato é que grande parte da ciência da computação teórica (incluindo as coisas em que trabalho) é praticamente inútil, embora matematicamente bonita. Infelizmente você tem que escolher os lados.
Yuval Filmus

Respostas:

10

Você pode estar interessado no trabalho sobre o Ceptre , resultado da pesquisa de doutorado de Chris Martens , que usa a teoria dos tipos para contar histórias interativas. A seguir, é apresentado o resumo da tese :

A narrativa interativa une idéias computacionais profundas com a rica história da humanidade de histórias e brincadeiras, fornecendo um contexto importante para a construção de ferramentas e linguagens. Ao mesmo tempo, linguagens formais de especificação oferecem uma paleta de técnicas de representação e inferência normalmente reservadas para a análise de linguagens de programação e sistemas dedutivos complexos. Esta tese conecta problemas no domínio interativo de narrativa a soluções em especificação formal.

Especificamente, examinamos a narrativa de um ponto de vista estrutural e observamos que caminhos narrativos alternativos desempenham um papel complementar às linhas do tempo de interação simultânea. A lógica linear fornece as ferramentas representacionais necessárias para investigar essa estrutura e, estendendo a correspondência às provas e à construção de provas, encontramos um conjunto de possibilidades computacionais. Apresentamos três esforços para realizar essas possibilidades: (1) o uso da programação lógica linear para gerar narrativas; (2) uma nova linguagem de programação para a criação de narrativas interativas, jogos e simulações; e (3) técnicas para declarar e provar as propriedades do programa em nível de design.

Concluímos que a programação lógica linear, enriquecida com uma extensão mínima de sua semântica lógica, permite uma ampla variedade de idiomas de programação e codificações de domínio. Como evidência, fornecemos cinco estudos de caso, incluindo simulação social, jogos de aventura baseados em combate e jogos de tabuleiro. Para apoiar o raciocínio sobre a correção do design, apresentamos técnicas para declarar e provar invariantes de programas, bem como uma prova de decidibilidade para verificar automaticamente esses invariantes em busca de um grande fragmento da linguagem.

Essas descobertas mostram que a lógica linear é uma linguagem de representação proveitosa para servir de base para modelar e executar mundos interativos e convidam investigações futuras sobre o uso de metodologias teóricas da prova para sistemas criativos.

gasche
fonte
11
Isso soa como um uso da lógica linear, em vez da teoria dos tipos em si .
David Richerby
6
A lógica linear é um tópico fundamental da teoria dos tipos. Este trabalho faz parte da teoria dos tipos como uma disciplina (algumas pessoas descrevem seu trabalho como "teoria das provas" quando é igualmente relevante para a teoria dos tipos, embora os nomes não sejam equivalentes, já que outros trabalhos na "teoria das provas" seriam considerados como mais específico à teoria da prova do que central à teoria do tipo).
Gasche
9

Tem havido usos interessantes da teoria dos tipos na linguística. Veja, por exemplo, as obras linguísticas de Chung-chieh Shan ou Christian Rétoré .

A seguir, é apresentada a descrição do livro de Rétoré sobre gramáticas categoriais:

Este livro é uma introdução contemporânea e abrangente às gramáticas categoriais da tradição lógica iniciada pelo trabalho de Lambek. Ele orienta estudantes e pesquisadores através dos resultados fundamentais no campo, fornecendo provas modernas de muitos teoremas clássicos, bem como avanços recentes originais. Numerosos exemplos e exercícios ilustram as motivações e aplicações desses resultados do ponto de vista linguístico, computacional e lógico. O cálculo de Lambek e suas variantes, e as gramáticas correspondentes, estão no centro dessas notas de aula. Um capítulo é dedicado a uma característica essencial dessas gramáticas categoriais: sua interface sintaxe-semântica muito elegante. Além disso, adaptamos redes de prova de lógica linear a esses cálculos, pois eles fornecem algoritmos de análise eficientes, como exemplificado no analisador Grail.

A citação a seguir está na introdução do capítulo do livro sobre Efeitos colaterais linguísticos de Shan :

Este artigo relaciona casos de aparente não composicionalidade em linguagens naturais com aqueles em linguagens de programação. Tem a forma de uma ampulheta: começo no §1 com uma abordagem da interface sintaxe-semântica que nos ajuda a construir teorias semânticas composicionais. Essa abordagem é traçar uma analogia entre efeitos colaterais computacionais em linguagens de programação e o que chamo de analogia efeitos colaterais linguísticos em linguagens naturais.

Essa conexão pode beneficiar cientistas da computação e lingüistas, mas eu me concentro aqui na última direção da transferência de tecnologia. As continuações têm sido úteis no tratamento de efeitos colaterais computacionais. No §2, introduzo uma nova metalinguagem para continuações na semântica.

A metalinguagem que apresento é útil para analisar linguagens de programação e linguagens naturais. Por intuição, analiso o primeiro uso no §3 e depois aponto as virtudes desse tratamento no §4.

Passando para a linguagem natural no §5, descrevo em detalhes como essa perspectiva ajudou Chris Barker e eu estudamos encadernação e cruzamento, bem como perguntas e superioridade. Também usei continuações para estudar o escopo quantificador e por tempo indeterminado, particularmente no chinês mandarim, mas só há espaço aqui para esboçar esses desenvolvimentos adicionais, no §6.

gasche
fonte
9

Por causa da correspondência de Curry-Howard , os tipos podem ser interpretados como proposições e proposições como tipos.

Como resultado disso, a teoria de tipos é aplicável a literalmente qualquer campo que use lógica formal para suas provas. Isso pode ser verificação de circuitos, análise real, lógica simbólica, geometria etc.

Por exemplo, algumas ferramentas automáticas de verificação de provas funcionam usando esse princípio: elas verificam a validade da prova, verificando um termo específico em algum sistema de tipos. O verificador de prova LF é baseado nessa abordagem, assim como o HOL Light . Como um exemplo de aplicativo, o código de transporte de prova usou o LF para verificar as provas de segurança da memória do código não confiável. O benefício de usar esse tipo de verificador de provas é que a implementação pode ser muito simples e, portanto, podemos obter alta garantia de que a implementação está correta. Veja, por exemplo, o seguinte documento:

Damas fundamentais com pequenas testemunhas . Dinghao Wu, Andrew W. Appel, Aaron Stump. PPDP 2003.

jmite
fonte
Isso pode ajudar: math.ucr.edu/home/baez/rosetta.pdf
Pseudônimo
Eu não acho que isso responda à pergunta. E as aplicações reais?
Yuval Filmus
@YuvalFilmus Definir "real"?
David Richerby
11
Você sabe se alguém usou a teoria dos tipos para provar algo novo sobre verificação de circuitos, análises reais, lógica simbólica ou geometria? Ou estamos apenas falando de casos em que alguém usa 20 páginas da teoria dos tipos para provar algo que leva três linhas em um livro elementar?
David Richerby
@ David O que esta resposta é que, em princípio, você pode usar a teoria dos tipos para provar coisas. Além disso, em princípio, podemos usar autômatos celulares para provar coisas, já que a Regra 110 é Turing-completa. Eu acho que a primeira declaração é tão sem sentido quanto a segunda.
Yuval Filmus
7

Um artigo interessante que explica aplicações de tipos dependentes é o The Power of Pi , que mostra como o Agda pode ser usado para resolver problemas interessantes.

Outro bom exemplo é o uso de tipos dependentes para o controle de recursos. Um bom exemplo é a API de gerenciamento de arquivos do Effects of Idris . Por exemplo, a função para ler uma linha de um arquivo tem o seguinte tipo

readLine  : { [FILE_IO (OpenFile Read)] } Eff String

que especifica que essa função é aplicável apenas se houver um arquivo aberto. A lista entre chaves indica quais efeitos estão disponíveis. Nesse caso, temos que essa função requer o efeito de ter um arquivo aberto para leitura.

Mais informações sobre a biblioteca Effect podem ser encontradas aqui .

Mais um aplicativo é o uso de tipos dependentes de simultaneidade, conforme relatado no artigo a seguir pelo criador do Idris.

Rodrigo Ribeiro
fonte
11
Mais exemplos adicionados.
Rodrigo Ribeiro
3

Como mencionado na resposta de jmite, a lógica de ordem superior / teoria dos tipos na verificação de circuitos / hardware / eletrônica existe há décadas e agora é tão rotineira que nem sequer percebeu / considerou uma "aplicação" após um esforço de transferência aparentemente importante em década de 1990, embora ainda seja uma área ativa de pesquisa. também existe muita aplicação da Coq e sua lógica de tipo, em particular na verificação de circuitos / hardware / eletrônica, desde a lógica de gate de baixo nível até estruturas de nível / ordem / subsistemas de nível muito mais alto. aqui estão algumas referências principais

vzn
fonte
11
Para ser justo, no entanto, a maioria das verificações reais de hardware em escala industrial foi feita usando a verificação de modelo, uma tecnologia de verificação geralmente não relacionada à teoria de tipos (embora pontes tenham sido desenhadas recentemente). A teoria dos tipos foi usada para criar linguagens de descrição de hardware (não muito buscadas nas linguagens de programação), e a maioria das linguagens fornecidas está nessa categoria, e alguns dos assistentes de prova projetados para verificação de hardware (principalmente a HOL original, mas não os PVS mais utilizados) são transposições de Curry-Howard da teoria dos tipos.
Gasche
se você tiver um conhecimento mais profundo da verificação de hardware, seria interessante ouvir mais detalhes no bate-papo sobre ciência da computação, mas pense / suspeite de linhas estreitas / distintas / generalizações não são fáceis de desenhar nessa área, por exemplo, entre verificação de modelo e teoria de tipos. pode ser necessária uma análise histórica muito sutil para descobrir / reunir de maneira abrangente as conexões entre dois campos diferentes com objetivos diferentes e, às vezes, está fora das capacidades dos especialistas em ambos os campos individualmente ... os árbitros em geral mostram fortes conexões que poderiam ser analisadas mais adiante. ..
vzn 1/11/2015