Qual é a teoria do tipo dependente mais intuitiva que eu poderia aprender?

46

Estou interessado em obter uma compreensão realmente sólida da digitação dependente. Eu li a maior parte do TaPL e li (se não totalmente absorvido) 'Tipos Dependentes' no ATTaPL . Também li e vasculhei vários artigos sobre digitação dependente.

Muitas discussões da teoria dos tipos parecem se concentrar em adicionar recursos incrementais aos sistemas de tipos anteriores, e não "qual é a próxima grande generalização do sistema de tipos X?". Os tipos dependentes parecem ser a próxima grande generalização do Sistema F, mas ainda não encontrei a linguagem intuitiva e canônica do tipo dependente. As muitas referências ao cálculo de construções (indutivas) me fazem pensar que o CoC é essa linguagem, mas as explicações da linguagem que eu vi não me parecem muito claras ou intuitivas.

Espero / acho que esse idioma terá recursos como: (e informe-me se algo em particular parecer confuso ou irreal)

  • Abstração generalizada (pode ter funções de qualquer domínio na hierarquia de tipos para outro, tipo -> termo, termo-> tipo '' 'etc.)
  • Possui uma hierarquia infinita de digitação (terms: types: types ': types' ': ...)
  • Um número mínimo de elementos básicos. Imagino que a linguagem apenas afirme um único elemento para cada nível. Por exemplo, pode afirmar que ((): Unidade: Tipo: Tipo ': ...). Outros elementos são criados a partir desses elementos.
  • Os tipos de soma e produto são deriváveis.

Também estou procurando uma explicação dessa linguagem que idealmente discuta:

  • A relação entre abstração e quantificação nessa linguagem. Se eles não estão unificados, explique por que eles não estão unificados.
  • A hierarquia de tipos infinitos explicitamente

Estou fazendo essa pergunta porque quero aprender a teoria dos tipos dependentes, mas também porque quero montar um guia que, assumindo um pouco de experiência em CS, ensine o uso e como entender assistentes de prova e linguagens de tipo dependente.

(Cruz postada no Reddit)

John Salvatier
fonte

Respostas:

35

Existem algumas maneiras diferentes de abordar isso:

  1. Teoria do tipo dependente . Provavelmente, essa não é a maneira mais fácil de aprender sobre tipos dependentes, mas você pode examinar os documentos sobre Cálculo de Construções e suas variantes, Pure Type Systems, e o artigo de Martin Hofmann sobre Sintaxe e Semântica de Tipos Dependentes, por exemplo.

  2. Prova do teorema . Primeiramente, dê uma olhada na minha resposta a uma pergunta relacionada: como eu aprenderia a teoria subjacente do assistente de prova Coq? .

  3. Programação com tipos dependentes . Examinar idiomas recentes com tipos dependentes, como Epigram ou Agda, ou idiomas menos recentes, como Dependent ML e escrever alguns programas, ajudará a solidificar as idéias. Epigram, por exemplo, é extremamente limpo em design. Outro ângulo é ver como os tipos dependentes são implementados . Uma teoria prática de tipos dependentes é : Tipos dependentes sem o açúcar. Várias teses de doutorado são dedicadas à programação com a teoria dos tipos dependentes: Dan Licata , Nils Anders Danielsson , Ulf Norrel , Susmit Sarkar,ΠΣ, entre outros. E, claro, há o livro de Adam Chlipala, dado na resposta de Marc Hamann.

Eu estaria inclinado a começar com a programação, antes de passar a usar a prova de teoremas e começar a explorar as questões mais teóricas.

Dave Clarke
fonte
Posso encontrar trabalhos para o Epigram, mas não consigo encontrar um download real para o Epigram, apenas o ainda inacabado Epigram 2. Alguma idéia?
John Salvatier
1
Você encontrou: e-pig.org/darcs/Pig09/web ? Epigram está disponível na parte inferior da página.
Dave Clarke
3
O Epigram 1 é essencialmente inalterado desde há algum tempo AFAIK - o autor usa o Agda hoje em dia (enquanto trabalhava no Epigram 2 ao lado).
Blaisorblade 26/03
Em 2019, acho que o Epigram 2 nunca vai acontecer - mas há Idris (e Idris 2!) Agora.
xrq
14

λπ

O Twelf é um bom sistema de prova de teoremas baseado em LF. Examinar as notas avançadas do curso oferecidas por Frank Pfenning é uma boa introdução à teoria e prática da LF.

Dito isto, talvez não seja o melhor primeiro sistema para aprender se o seu interesse é em matemática construtiva, e não nos fundamentos da teoria dos tipos: LF significa estrutura lógica e é um sistema usado para axiomatizar teorias, e não é tão frequentemente trabalhado como um sistema de destino diretamente. Usar um sistema baseado na teoria de tipos de Martin-Loef é provavelmente a melhor introdução - Dave menciona a Agda, entre outros - talvez seja um melhor ponto de partida se esse for o seu objetivo, pois você pode começar com tipos aritméticos e indutivos mais rapidamente. estrutura.

Charles Stewart
fonte
10

O CoC é provavelmente o caminho a percorrer. Basta mergulhar na Coq e trabalhar com um bom tutorial como o Software Foundations (no qual Pierce do TaPL e ATTaPL está envolvido).

Depois de entender os aspectos práticos da digitação dependente, volte às fontes teóricas: elas farão muito mais sentido.

Sua lista de recursos parece basicamente correta, mas ver como eles funcionam na prática vale mais que mil pontos de recursos.

(Outro tutorial um pouco mais avançado é a programação certificada de Adam Chlipala com tipos dependentes )

Marc Hamann
fonte
"intuitivo" é talvez o ponto de discórdia aqui: há muito mais intuições no CoC / CIC do que apenas digitação dependente. É um bom objetivo final - na minha opinião, a escolha é realmente entre Coq e Twelf - mas talvez não seja o melhor primeiro passo para "obter uma compreensão realmente sólida da digitação dependente".
Charles Stewart
@ Charles: Seu ponto de vista está correto. Eu ainda acho que, do ponto de vista prático, é uma boa aposta. Embora um entendimento completo do CoC / CIC possa ser uma tarefa mais complexa, o Coq (mais a existência de bons tutoriais de nível básico para ele) facilita o foco em aprender apenas os aspectos de programação ou apenas os aspectos básicos do assistente de prova (como ditam seus interesses) mesmo antes de entender todas as complexidades. Eu acho que isso se qualifica como "intuitivo" para alguém que não vem de uma base teórica.
Marc Hamann