Estou lendo sobre a teoria dos tipos dependentes no livro on-line da Teoria dos Tipos de Homotopia . Na seção 1.3 do capítulo Teoria dos tipos , introduz a noção de hierarquia de Universos : , em quevocê0 0: U1 1: U2: ⋯você0 0:você1 1:você2:⋯\mathcal{U}_0 : \mathcal{U}_1 : \mathcal{U}_2 :...
Eu estou trabalhando em uma linguagem baseada em expressão da genealogia ML, então ela naturalmente precisa de inferência de tipo> :) Agora, estou tentando estender uma solução baseada em restrições para o problema de inferir tipos, com base em uma implementação simples no EOPL (Friedman e...
O que é indução-indução ? Os recursos que encontrei são: o livro HoTT , no final do capítulo 5.7. Artigo do nLab um artigo chamado definições indutivo-indutivas este post do blog também menciona tipos indutivos-indutivos As duas primeiras referências são muito breves para mim e as duas últimas...
Na programação de tipo dependente, existem duas maneiras principais de decompor dados e executar recursão: Correspondência de padrões dependentes : as definições de funções são fornecidas como várias cláusulas. A unificação garante que todos os casos omitidos sejam impossíveis e um solucionador...
Desta referência: Estrita positividade A estrita condição de positividade exclui declarações como data Bad : Set where bad : (Bad → Bad) → Bad A B C -- A is in a negative position, B and C are OK Por que A é negativo? Também porque B é permitido? Eu entendo por que C é...
Sou relativamente novo em teoria de tipos e programação dependente. Eu estudei o cálculo de construções (CoC) e outros sistemas de tipo puro. Estou particularmente interessado em usá-lo como uma representação intermediária de preservação de prova para um sistema de compilador. Entendo que os tipos...
Self Types são uma extensão do Cálculo de Construções [1] que permite que o idioma expresse tipos de dados algébricos codificados através da Codificação Scott. A Codificação Scott fornece a capacidade de correspondência de padrões O(1), que é um dos principais motivadores para a inclusão de...
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
O que "em posição positiva" e "em posição negativa" significa no contexto da teoria dos tipos? A única coisa que entendi no post de Bob Harper sobre o tema é que há uma conexão entre polaridade nesse sentido na teoria dos tipos e polaridade na lógica, mas não sei qual é essa...
Estou trabalhando em um pequeno compilador de cálculo lambda que possui um sistema de inferência do tipo Hindley-Milner em funcionamento e agora também oferece suporte a vamos recursivos (não no código vinculado), que eu entendo que deve ser suficiente para torná-lo completo . O problema agora é...
Estou lendo este artigo bem conhecido sobre Universos na teoria dos tipos . No começo, eu esperava algo semelhante ao Setωda Agda, mas acontece que é algo ainda mais geral. Parece generalizar a construção do universo de um tipo indutivo-recursivo simples para um aglutinante (semelhante a e ). A...
Dado que: Uma linguagem com sistemas do tipo muito expressivo (por exemplo, Idris ) também pode ter mecanismos de escape como interfaces de função estrangeira / unsafePerformIO. Existem assistentes de prova que podem ser usados para provar algumas propriedades de um programa escrito em um...
Coq inclui let-expression em sua linguagem principal. Podemos traduzir expressões let para aplicativos como este: let x : t = v in b ~> (\(x:t). b) v Entendo que isso nem sempre funciona porque o valor vnão estaria disponível ao digitar b. No entanto, isso pode ser facilmente corrigido através...
Quero saber até que ponto um sistema de tipos em uma linguagem de programação pode ser benéfico. Por exemplo, eu sei que em uma linguagem de programação de tipo dependente, podemos criar uma Vectorclasse incorporando o tamanho do vetor na assinatura do tipo. É como um exemplo de fato. Também...
Digamos que as listas sejam definidas como List a = Nil | Cons a (List a) Então, em Haskell, List xo maior ou o menos fixo? Estou perguntando porque o lfp deve excluir listas infinitas (mas você pode construí-las em Haskell), enquanto o gfp deve excluir as
Estou procurando um algoritmo de inferência de tipo para uma linguagem que estou desenvolvendo, mas não consegui encontrar uma que atenda às minhas necessidades porque elas geralmente são: à Haskell, com polimorfismo, mas sem sobrecarga ad-hoc à C ++ (automático) no qual você tem sobrecarga...
Eu tenho tentado separar as definições de segurança de tipo e solidez de tipo e estou me divertindo muito. Perguntei recentemente a um professor e, depois de pensar um pouco, ele disse que realmente não havia diferença. No entanto, depois de ler isso , parece que: O Type Safety é uma propriedade...
Na teoria dos tipos, se alguém permite que o tipo seja um membro de si mesmo, isso torna a teoria inconsistente. Eu o entendo por analogia ao paradoxo de Russel na Teoria dos Conjuntos, mas preferiria ver isso na Teoria dos Tipos. Existe um pequeno exemplo do equivalente na teoria dos...
Recentemente, iniciei meus estudos em teoria de tipos / sistemas de tipos e Lambda Calculus. Eu já li sobre o Simple Typed Lambda Calculus no estilo Church and Curry. O último também é conhecido como sistema de atribuição de tipos (TA). Estou pensando nas relações entre TA e Hindley-Milner (HM),...
A teoria do domínio fornece uma incrível teoria da computabilidade na presença de tipos simples. Mas quando o polimorfismo paramétrico é adicionado, não parece haver uma teoria legal que explique o que está acontecendo tão bem quanto a teoria de domínio explica a computação por tipos simples....