Verificação de Tipos

Frank Coelho de Alcantara -2021  

Motivos

Segurança para execução.

Detecção de erros em tempo de compilação.

Metáforas mas expressivas: overload, por exemplo.

Fornecer informações para o otimizador de código.

Identificação de tipos

símbolo meramente ilustrativo, sem valor didático símbolo meramente ilustrativo, sem valor didático

Verificação de Tipos

símbolo meramente ilustrativo, sem valor didático

Tipos, e mais tipos

Definição de Tipos

Um tipo é uma classificação que representa um conjunto específico de dados. Esta classificação define as operações que podem ser realizadas com estes dados.

Definição de Sistema de Tipos

Um conjunto de regras para garantir a aplicação e verificação de tipos em artefatos de uma linguagem de programação.

Anotação de Tipos

Anotação de tipos é útil como documentação, e para a segurança do programa em execução.

Minha Preferência

definição de fortemente e estáticamente tipado.

Inferência

O compilador, ou o interpretador, deduz o tipo de uma estrutura de dados a partir do dados que alocamos nesta estrutura.

Tipos são conjuntos

símbolo meramente ilustrativo, sem valor didático

Por que tipos?

símbolo meramente ilustrativo, sem valor didático

Exemplo de anotação

Exemplo de anotação de várias estruturas de dados diferentes, em escopos diferentes, todas chamadas de i.

Exemplo: "a" + 1

mostra que o javascript concatena inteiros e strings

Propriedades do Sistema de Tipos

Progresso: quando uma expressão está corretamente tipada, ou é um valor, ou uma regra de expansão pode ser aplicada e preservação: se uma expressão está corretamente tipada, sua redução não muda o seu tipo.

Fluxo de Verificação

verificamos primeiro os tipos primitivos, depois os compostos

Matemática, sempre acaba na Matemática.

Enumeração

os tipos enum são estrutura de dados que representam conjuntos.

Tuplas

Tuplas são estruturas de dados que representam um produto cartesiano

Tuplas - Considerações

Em qual ordem colocamos os dados de uma struct na memória

Vetores

Vetores são conjuntos indexados de dados.

União

A união de conjuntos e representada por estruturas de dados como a union do C.

Variant ou Union

No caso de estruturas do tipo union, apenas um dado é disponível a cada uso.

Variant ou Union - Considerações

Cada campo usa o mesmo espaço de memória então o tamanho da union é o tamanho do maior campo definido.

Só Podemos usar um campo de cada vez. Se atribuirmos valores, ainda que corretos, para cada um dos campos em sequencia, apenas a última atribuição terá sentido.

Uma herança dos tempos que a memória era muito cara e reduzida.

Nestes tempos a union era uma forma bem razoável de manter uma metáfora consistente nos seus programas.

Coproduto

O CoProduto do ML é uma união com a origem dos elementos identificada.

Funções

Função é o mapeamento de um domínio em uma imagem

Structs

símbolo meramente ilustrativo, sem valor didático

Structs - Considerações

As structs são representadas como um bloco de memória, grande o suficiente para armazenar todos os campos.

O campos são ordenados de acordo com a a ordem de declaração.

O compilador irá determiner o tamanho total e a posição dos campos em memória. Durante a execução o programa não entende a estrutura da struct.

Ou seja, a struct, como a definimos só existe em forma de artefato de Código e metáfora.

Vantagem das Structs

símbolo meramente ilustrativo, sem valor didático

Sistema de Tipos: Definição.

Em Linguagem Natural

Podemos criar um sistema de tipos usando linguagem natural

Em Linguagem Natural - Exemplo

Uma declaração é bem formatada se:

Sua variável alvo está bem formatada;

Sua expressão fonte está bem formatada, e os tipos declarados da fonte e do alvo coincidem;

Uma condicional é bem formatada se sua expressão de teste for do tipo bool e tanto a opção then quanto a opção else estão bem formatadas.

Definição de tipo

Com a sentença: a expressão $\lambda$ é do tipo $T$, pretendemos mostrar, sem ter que avaliar a expressão que, quando a expressão for avaliada, irá gerar um tipo de dados $\lambda'$ que, sem dúvida, será do tipo $T$.

As seguintes declarações são equivalentes:

  1. $\lambda$ é do tipo $T$
  2. $\lambda$ tem o tipo $T$
  3. $\lambda$ pertence ao tipo $T$
  4. O tipo de $\lambda$ é $T$

Cálculo de Sequentes

O cálculo de Sequentes é uma parte da lógica de primeiro grau que permite a automação do processo de inferência de uma expressão lógica.

Parte de um conjunto condicional de proposições tautológicas, chamada de antecedente, onde cada linha de prova, também é uma tautologia condicional, chamada de sequente.

Estas inferências são expressas na forma: $\Gamma \vdash \Delta$. Onde $\Gamma$ representa um conjunto de fórmulas, ou contexto e $\Delta$ outro conjunto de fórmulas, ou sequente.

Formalmente definiremos um tipo por: $\Gamma \vdash \lambda: T$.

Que leremos dado o contexto $\Gamma$ existe um $\lambda$ do tipo $T$.

Cálculo de Sequentes - Exemplo

Como podemos verificar os tipos nas seguintes declarações em cálculo de sequentes?

$\text{𝑓𝑙𝑜𝑎𝑡 𝑓(𝑓𝑙𝑜𝑎𝑡 𝑥, 𝑓𝑙𝑜𝑎𝑡 𝑦) \{ 𝑟𝑒𝑡𝑢𝑟𝑛 𝑥+𝑦; \}}$

$𝑥 : 𝑓𝑙𝑜𝑎𝑡, 𝑦 : 𝑓𝑙𝑜𝑎𝑡 ⊢ 𝑥+𝑦 : 𝑓𝑙𝑜𝑎𝑡$

$\text{𝑖𝑛𝑡 𝑔(𝑖𝑛𝑡 𝑥, 𝑖𝑛𝑡 𝑦) \{ 𝑟𝑒𝑡𝑢𝑟𝑛 𝑥+𝑦; \}}$

$𝑥 : 𝑖𝑛𝑡, 𝑦 : 𝑖𝑛𝑡 ⊢ 𝑥+𝑦 : 𝑖𝑛𝑡$

Regras de Atribuição

Usamos o cálculo de sequentes para definir as regras de atribuição, verificação e checagem de tipos. Em um formato mais conveniente.

regra de equivalência entre tipos de dois operadores inteiros em uma soma.

Lemos: se 𝐸1 tem tipo int e 𝐸2 tem tipo int então E1+E2 tem tipo int

Cálculo de Sequentes - Exemplo

enunciado do exemplo

Construíndo a AST

AST montada com as regras de produção escritas em cálculo de sequentes