Como ler as regras de digitação?

18

Comecei a ler cada vez mais trabalhos de pesquisa em idiomas. Acho muito interessante e uma boa maneira de aprender mais sobre programação em geral. No entanto, há geralmente vem uma seção onde eu sempre lutar com (Tomemos por exemplo a terceira parte deste ), pois me falta a base teórica em ciência da computação: Regras Tipo.

Existem bons livros ou recursos on-line disponíveis para começar nesta área? A Wikipedia é incrivelmente vaga e realmente não ajuda um iniciante.

suls
fonte
1
Você leu o artigo vinculado sobre regras de inferência ?
Raphael
2
O TAPL de Benjamin Pierce é realmente bom.
Gilles 'SO- stop be evil'

Respostas:

25

Na maioria dos sistemas de tipos, as regras de tipo trabalham juntas para definir julgamentos do formulário:

Γe:τ

Isto indica que no contexto a expressão e tem o tipo τ . Γ é um mapeamento das variáveis ​​livres de e para seus tipos.Γeτ
Γe

Um sistema de tipos consistirá em um conjunto de axiomas e regras (um sistema formal de regras de inferência , como Raphael aponta).

Um axioma é da forma

Γe:τ

Isto indica que o julgamento detém (sempre).Γe:τ

Um exemplo é

x:τx:τ

que afirma que, sob a suposição de que o tipo de variável é τ , a expressão x tem o tipo τ .xτxτ

As regras de inferência pegam fatos que já foram determinados e constroem fatos maiores a partir deles. Por exemplo, a regra de inferência

Γe1:ττΓe2:τΓe1 e2:τ

diz que se eu tiver uma derivação do fato e uma derivação do fato y- e 2 : τΓe1:ττΓe2:τ , então eu posso obter uma derivação do fato . Nesse caso, esta é a regra para digitar o aplicativo de funções.Γe1 e2:τ

Existem duas maneiras de ler esta regra:

  • de cima para baixo - dadas duas expressões (uma função e outra expressão) e algumas restrições em seu tipo, podemos construir outra expressão (a aplicação da função à expressão) com o tipo fornecido.
  • bottom-up - dada uma expressão que é, nesse caso, a aplicação de uma função a alguma expressão, a maneira como ela é digitada é digitando primeiro as duas expressões, garantindo que seus tipos atendam a algumas restrições, a saber, que a primeira é uma tipo de função e que o segundo tenha o tipo de argumento da função.

Algumas regras de inferência também manipulam adicionando novos ingredientes (visualizados de baixo para cima). Aqui está a regra para a atração- λ :Γλ

Γx:τe:τΓλx.e:ττ

As regras de inferência são aplicadas indutivamente com base na sintaxe da expressão que está sendo considerada para formar uma árvore de derivação. Nas folhas da árvore (no topo) haverá axiomas e os galhos serão formados aplicando regras de inferência. No final da árvore está a expressão que você está interessado em digitar.

Por exemplo, uma derivação da digitação da expressão éλf.λx.f x

f:ττ,x:τf:ττf:ττ,x:τx:τf:ττ,x:τf x:τf:ττλx.f x:τλf.λx.f x:τ

Ambos os livros são muito abrangentes, mas começam lentamente, construindo uma base sólida.

Dave Clarke
fonte
8

Há um bonito tutorial on-line interativo sobre cálculo sequencial, que pode ajudar a criar algumas intuições e a sentir como a inferência funciona: um tutorial interativo do cálculo sequencial

aemxdp
fonte
3
Isso é muito legal.
Dave Clarke
1
Impressionante. Eu tenho que encontrar alguma tag wiki para colocar isso.
Raphael
5

Na página da Wikipedia, recomenda-se " Type Systems, Luca Cardelli, ACM Computing Surveys ", que é uma pesquisa de duas páginas que pode ajudá-lo a entender como ler uma regra. De qualquer forma, como ler uma regra é perfeitamente explicado nessa página da Wikipedia (ou melhor ainda na pesquisa de 2 páginas). No entanto, para entender tudo, você precisa entender o que é um sistema de digitação (composto por várias regras), para o qual o artigo da Wikipedia " Sistema de tipos " é um bom começo (e você tem vários livros na seção " Referências ") página se você quiser ir mais longe).

Alejandro DC
fonte