Tipagem Estática e Dinâmica

A tipagem estática verifica os tipos antes da execução de um programa, enquanto a tipagem dinâmica os verifica durante a execução; a tipagem gradual busca combinar as duas em uma única linguagem.

Definition

A tipagem estática verifica as restrições de tipo em tempo de compilação para que programas bem tipados sejam aceitos antes da execução; a tipagem dinâmica adia as verificações de tipo para o tempo de execução, levantando erros quando operações são aplicadas a valores de tipo inadequado.

Scope

Este tópico abrange o espectro de quando e como a verificação de tipo ocorre: verificação estática que rejeita programas mal tipados em tempo de compilação, verificação dinâmica que detecta erros de tipo em tempo de execução, e tipagem gradual ou opcional que permite a coexistência das duas. Aborda as garantias, flexibilidade e implicações de desempenho de cada uma, juntamente com a solidez da disciplina de verificação de tipo.

Core questions

• Que classes de erro a verificação estática previne que a verificação dinâmica não pode prevenir antecipadamente?
• Que flexibilidade a tipagem dinâmica oferece, e a que custo?
• Como a tipagem gradual pode misturar de forma sólida código tipado e não tipado?
• Como a solidez de uma disciplina de tipo estático é estabelecida?

Key theories

Tipagem gradual

Siek e Taha definiram um sistema de tipos que permite que partes de um programa sejam estaticamente tipadas e outras dinamicamente tipadas, com uma relação de consistência governando a interação segura na fronteira.

Solidez do tipo estático

O método de progresso e preservação de Wright e Felleisen mostra que um sistema de tipo estático sólido garante que programas bem tipados nunca atinjam estados travados, formalizando a segurança da verificação estática.

Clinical relevance

A escolha estática versus dinâmica molda o fluxo de trabalho do desenvolvedor, as ferramentas e a confiabilidade. Sistemas de tipagem gradual e opcional, como aqueles sobrepostos a linguagens dinâmicas, permitem que as equipes adicionem garantias estáticas incrementalmente a grandes bases de código existentes.

History

As primeiras linguagens dividiram-se em linhagens estaticamente tipadas (Algol, Pascal, ML) e dinamicamente tipadas (Lisp, Smalltalk). À medida que as linguagens dinâmicas se tornaram populares pela produtividade, os pesquisadores buscaram conciliar as abordagens; a tipagem gradual de Siek e Taha em 2006 e o trabalho contemporâneo sobre tipos opcionais levaram a sistemas gradualmente tipados amplamente utilizados, construídos sobre linguagens dinâmicas.

Debates

Custo e solidez da tipagem gradual

Pesquisadores debatem se a tipagem gradual sólida pode evitar custos proibitivos de verificação em tempo de execução nas fronteiras tipadas/não tipadas, e se a tipagem 'opcional' não sólida é uma troca prática melhor.

Key figures

• Benjamin Pierce
• Jeremy Siek
• Walid Taha
• Matthias Felleisen

Seminal works

• pierce2002
• siek2006
• wright1994

Frequently asked questions

A tipagem estática é sempre melhor que a tipagem dinâmica?

Nenhuma é universalmente melhor; a tipagem estática detecta mais erros precocemente e auxilia as ferramentas, enquanto a tipagem dinâmica oferece flexibilidade e prototipagem mais rápida, então a escolha certa depende das necessidades de confiabilidade e agilidade do projeto.

O que é tipagem gradual?

A tipagem gradual permite que um único programa misture porções estaticamente e dinamicamente tipadas, inserindo verificações em tempo de execução nas fronteiras para que o código tipado mantenha suas garantias enquanto o código não tipado permanece flexível.