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.
fonte
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.
fonte
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 )
fonte
Achei que este artigo ajudou a desmistificar o conceito em um nível elementar: http://golem.ph.utexas.edu/category/2010/03/in_praise_of_dependent_types.html
fonte
Veja http://www2.tcs.ifi.lmu.de/~abel/talkDTP2011.pdf e um sistema PiSigma mais antigo mencionado lá.
fonte