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.

logic reference-request terminology type-theory 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'

25

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

Γ ⊢ e : τ

$\Gamma\vdash e:\tau$

Isto indica que no contexto a expressão tem o tipo . é um mapeamento das variáveis livres de para seus tipos. $\Gamma$ $e$ $\tau$
$\Gamma$ $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

\frac{}{Γ ⊢ e : τ}

$\dfrac{}{\Gamma \vdash e:\tau}$

Isto indica que o julgamento detém (sempre). $\Gamma \vdash e:\tau$

Um exemplo é

\frac{}{x : τ ⊢ x : τ}

$\dfrac{}{x:\tau\vdash x:\tau}$

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

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

\frac{Γ ⊢ e_{1} : τ \to τ^{'} Γ ⊢ e_{2} : τ}{Γ ⊢ e_{1} e_{2} : τ^{'}}

$\dfrac{\Gamma\vdash e_1:\tau\to\tau' \quad \Gamma\vdash e_2:\tau}{\Gamma\vdash e_1\ e_2:\tau'}$

diz que se eu tiver uma derivação do fato e uma derivação do fato $\Gamma\vdash e_1:\tau\to\tau'$ $\Gamma\vdash e_2:\tau$ , então eu posso obter uma derivação do fato . Nesse caso, esta é a regra para digitar o aplicativo de funções. $\Gamma\vdash e_1\ e_2:\tau'$

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- : $\Gamma$ $\lambda$

\frac{Γ x : τ ⊢ e : τ^{'}}{Γ ⊢ λ x . e : τ \to τ^{'}}

$\dfrac{\Gamma x:\tau\vdash e:\tau'}{\Gamma\vdash \lambda x.e:\tau\to \tau'}$

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 é $\lambda f.\lambda x.f\ x$

\frac{\frac{}{f : τ \to τ^{'}, x : τ ⊢ f : τ \to τ^{'}} \frac{}{f : τ \to τ^{'}, x : τ ⊢ x : τ}}{\frac{f : τ \to τ^{'}, x : τ ⊢ f x : τ^{'}}{\frac{f : τ \to τ^{'} ⊢ λ x . f x : τ^{'}}{⊢ λ f . λ x . f x : τ^{'}}}}

$\dfrac{\dfrac{}{f:\tau\to\tau',x:\tau\vdash f:\tau\to\tau'} \qquad \dfrac{}{f:\tau\to\tau',x:\tau\vdash x:\tau}} {\dfrac{f:\tau\to\tau',x:\tau\vdash f\ x:\tau'}{ \dfrac{f:\tau\to\tau'\vdash \lambda x.f\ x:\tau'}{\vdash \lambda f.\lambda x.f\ x:\tau'}}}$

Tipos e linguagens de programação por Benjamin Pierce
Fundamentos práticos para linguagens de programação por Robert Harper

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

Como ler as regras de digitação?

Respostas: