Quantificação universal / existencial?

Estou lutando para entender o objetivo da quantificação universal e existencial de tipos. Estou brincando de escrever uma linguagem de brinquedo baseada no cálculo de construções . Eu tenho lido sobre Morte e Henk para me ajudar a entender melhor.

Não entendo por que o CoC tem abstração lambda e forall.

Parece-me que o lambda subsume tudo em um sistema em que os tipos são passados ​​manualmente. Em outras palavras, que as seguintes

Pode ser substituído por

Se foi aplicado primeiro ao tipo que está sendo usado.

o que estou perdendo? Que artigos, blogs ou artigos existem para ler que possam me ajudar?

Obrigado.

É bom lembrar que (ou$\forall$$\Pi$ como você vê às vezes) é um tipo. Está generalizando . Então, enquanto ele faz todo o sentido para dizer ( λ x : Um . M ) N , não faz sentido dizer ( ∀ x : Um . M ) N porque ∀ . . . é apenas um tipo. Você não diria ( A → B ) N becaues → não é para computação per-se, ele está lá para$\to$$(\lambda x : A. M)\ N$$(\forall x : A. M)\ N$$\forall ...$$(A \to B)\ N$$\to$classifique termos lambda que podem ser aplicados assim .

Isso foi algo que também me fez tropeçar, mas é assim que o cálculo das construções (assim como qualquer outro sistema tipicamente dependente é definido).

Os dois programas que você escreveu têm intenções muito diferentes e o primeiro está incorreto. Não faz sentido dizer porque ∀ requer que ambos os seus argumentos por tipos que significa que se ∀ x : A . B deve ser bem digitado, devemos ter B : ∗ . No entanto, λ x . x não é um tipo, só pode nunca ser atribuído um tipo de forma ∀ x : A . B , nunca $\forall x : A.\ \lambda x.\ x$$\forall$$\forall x : A. B$$B : *$$\lambda x. x$$\forall x : A. B$$*$. A segunda, por outro lado é quase (eu acho que você quis retornar não x ) é uma função e é dado um tipo usando dois ∀ s.$a$$x$$\forall$

Lembre-se de que tipos existenciais e universais são bastante diferentes. É lógica construtiva, não lógica clássica, e na lógica construtiva e ∃ não são tão relacionadas quanto na lógica clássica.$\forall$$\exists$

é o tipo de programa que recebe um objeto do tipo A e retorna um objeto do tipo B ( x ) . O importante aqui é que o tipo B ( x ) dependede x e não é o mesmo para todos os x . Pode variar dependendo do que x é. Para uma entrada x, podemos gerar um número inteiro. Para outro, podemos gerar um número real. Para mais uma, poderíamos gerar uma função sobre números reais. Se B ( x $\forall x:A. B(x)$$A$$B(x)$$B(x)$ $x$$x$$x$$x$$B(x)$não varia com , em seguida, você pode usar A → B no lugar que é o tipo de funções de A para B .$x$$A\to B$$A$$B$

é aversãodependenteda disjunção (construtiva). Você pode pensar em disjunção construtiva A ∨ B $\exists x:A. B(x)$$A \lor B$ de dois tipos e B como a união disjunta de A e B . ∃ x : A . B ( x ) é a união disjunta de uma coleção de tipos B ( x ) indexados por x : A . O fato de o tipo B $A$$B$$A$$B$$\exists x:A.B(x)$$B(x)$$x:A$ van varia de acordo com o valor de x : A o torna um tipo dependente. Compare com o caso em que B não depende de x : A : ∃ x : A . B . Estamos levando uma cópia do mesmo B para cada x : A . Esta é isomorphic a A × B .$B(x)$$x:A$$B$$x:A$$\exists x:A. B$$B$$x:A$$A \times B$

Agora você pode perguntar por que precisamos de tipos de produtos e somas dependentes ? Porque eles nos dão um poder mais expressivo. Agora podemos ignorar completamente os tipos e ter teoria de tipos / programação funcional sem tipo. Mas isso remove os benefícios de ter tipos em primeiro lugar, por exemplo, você não saberá se todos os programas sempre serão encerrados (forte normalização). Consulte Cubo Lambda e tipo de dependente . Penso que uma boa maneira de entender bem os tipos dependentes é examinar as regras para introduzir e eliminar os tipos dependentes na teoria dos tipos de Martin-Lof .

O ponto principal dos tipos dependentes é: queremos permanecer dentro de uma boa teoria de tipos por vários motivos (por exemplo, evitando bugs, prova automática de terminação etc.). Não queremos ir para algo como cálculo lambda sem tipo, onde podemos tornar a expressão como as que você declarou e coisas muito mais poderosas. Podemos dizer que os tipos dependentes foram inventados para permitir expressar mais coisas enquanto ainda permaneciam dentro de uma boa teoria de tipos.