Sistema de tipo - Type system

Em linguagens de programação , um sistema de tipos é um sistema lógico que compreende um conjunto de regras que atribui uma propriedade chamada tipo às várias construções de um programa de computador , como variáveis , expressões , funções ou módulos . Esses tipos formalizam e reforçam as categorias implícitas que o programador usa para tipos de dados algébricos , estruturas de dados ou outros componentes (por exemplo, "string", "array de float", "função retornando booleano"). O objetivo principal de um sistema de tipos é reduzir as possibilidades de bugs em programas de computador, definindo interfaces entre diferentes partes de um programa de computador e, em seguida, verificar se as partes foram conectadas de maneira consistente. Essa verificação pode acontecer estaticamente (em tempo de compilação ), dinamicamente (em tempo de execução ) ou como uma combinação de ambos. Os sistemas de tipos também têm outras finalidades, como expressar regras de negócios, permitir certas otimizações do compilador , permitir o envio múltiplo , fornecer uma forma de documentação, etc.

Um sistema de tipos associa um tipo a cada valor calculado e, examinando o fluxo desses valores, tenta garantir ou provar que nenhum erro de tipo pode ocorrer. O sistema de tipo dado em questão determina o que constitui um erro de tipo, mas em geral, o objetivo é evitar que operações que esperam um certo tipo de valor sejam usadas com valores para os quais aquela operação não faz sentido (erros de validade). Os sistemas de tipos são frequentemente especificados como parte de linguagens de programação e integrados em interpretadores e compiladores, embora o sistema de tipos de uma linguagem possa ser estendido por ferramentas opcionais que realizam verificações adicionais usando a sintaxe e gramática de tipo original da linguagem.

Visão geral de uso

Um exemplo de um sistema de tipo simples é o da linguagem C . As partes de um programa C são as definições de funções . Uma função é chamada por outra função. A interface de uma função indica o nome da função e uma lista de parâmetros que são passados ​​para o código da função. O código de uma função de chamada declara o nome da função chamada, junto com os nomes das variáveis ​​que contêm valores para passar para ela. Durante a execução, os valores são colocados no armazenamento temporário e, em seguida, a execução salta para o código da função invocada. O código da função invocada acessa os valores e faz uso deles. Se as instruções dentro da função forem escritas com a suposição de receber um valor inteiro , mas o código de chamada passou um valor de ponto flutuante , o resultado errado será calculado pela função invocada. O compilador C verifica os tipos de argumentos passados ​​para uma função quando ela é chamada em relação aos tipos de parâmetros declarados na definição da função. Se os tipos não corresponderem, o compilador lançará um erro de tempo de compilação.

Um compilador também pode usar o tipo estático de um valor para otimizar o armazenamento de que precisa e a escolha de algoritmos para operações no valor. Em muitos compiladores C, o tipo de dados float , por exemplo, é representado em 32 bits , de acordo com a especificação IEEE para números de ponto flutuante de precisão simples . Assim, eles usarão operações de microprocessador específicas de ponto flutuante nesses valores (adição, multiplicação de ponto flutuante, etc.).

A profundidade das restrições de tipo e a maneira de sua avaliação afetam a digitação do idioma. Uma linguagem de programação pode ainda associar uma operação com várias resoluções para cada tipo, no caso de polimorfismo de tipo . A teoria dos tipos é o estudo dos sistemas de tipos. Os tipos concretos de algumas linguagens de programação, como inteiros e strings, dependem de questões práticas de arquitetura de computador, implementação de compilador e design de linguagem.

Fundamentos

Formalmente, a teoria dos tipos estuda os sistemas de tipos. Uma linguagem de programação deve ter a oportunidade de verificar o tipo usando o sistema de tipo, seja em tempo de compilação ou em tempo de execução, anotado manualmente ou inferido automaticamente. Como Mark Manasse disse concisamente:

O problema fundamental abordado por uma teoria dos tipos é garantir que os programas tenham significado. O problema fundamental causado por uma teoria dos tipos é que programas significativos podem não ter significados atribuídos a eles. A busca por sistemas de tipos mais ricos resulta dessa tensão.

A atribuição de um tipo de dados, denominado digitação , dá significado a uma sequência de bits , como um valor na memória ou algum objeto , como uma variável . O hardware de um computador de uso geral é incapaz de discriminar entre, por exemplo, um endereço de memória e um código de instrução , ou entre um caractere , um inteiro ou um número de ponto flutuante , porque não faz distinção intrínseca entre qualquer um dos valores possíveis que uma sequência de bits pode significar . Associar uma sequência de bits a um tipo transmite esse significado ao hardware programável para formar um sistema simbólico composto por esse hardware e algum programa.

Um programa associa cada valor a pelo menos um tipo específico, mas também pode ocorrer que um valor esteja associado a vários subtipos . Outras entidades, como objetos , módulos , canais de comunicação e dependências podem ser associadas a um tipo. Até mesmo um tipo pode ser associado a um tipo. Uma implementação de um sistema de tipos poderia, em teoria, associar identificações chamadas tipo de dados (um tipo de valor), classe (um tipo de objeto) e tipo (um tipo de tipo ou metatipo). Essas são as abstrações pelas quais a digitação pode passar, em uma hierarquia de níveis contidos em um sistema.

Quando uma linguagem de programação desenvolve um sistema de tipo mais elaborado, ela ganha um conjunto de regras mais refinado do que a verificação de tipo básica, mas isso tem um preço quando as inferências de tipo (e outras propriedades) se tornam indecidíveis e quando mais atenção deve ser dada por o programador anotar o código ou considerar as operações e o funcionamento relacionados ao computador. É desafiador encontrar um sistema de tipos suficientemente expressivo que satisfaça todas as práticas de programação de uma maneira segura de tipos.

Quanto mais restrições de tipo forem impostas pelo compilador, mais fortemente tipada será a linguagem de programação. Linguagens fortemente tipadas geralmente requerem que o programador faça conversões explícitas em contextos onde uma conversão implícita não causaria nenhum dano. O sistema de tipos de Pascal foi descrito como "muito forte" porque, por exemplo, o tamanho de um array ou string faz parte de seu tipo, tornando algumas tarefas de programação difíceis. Haskell também é fortemente tipado, mas seus tipos são inferidos automaticamente, de modo que as conversões explícitas costumam ser desnecessárias.

Um compilador de linguagem de programação também pode implementar um tipo dependente ou um sistema de efeitos , o que permite que ainda mais especificações do programa sejam verificadas por um verificador de tipo. Além de pares de tipo de valor simples, uma "região" virtual de código está associada a um componente de "efeito" que descreve o que está sendo feito com o quê e permite, por exemplo, "lançar" um relatório de erro. Assim, o sistema simbólico pode ser um sistema de tipo e efeito , o que lhe confere mais verificação de segurança do que apenas verificação de tipo.

Quer seja automatizado pelo compilador ou especificado por um programador, um sistema de tipos torna o comportamento do programa ilegal se estiver fora das regras do sistema de tipos. As vantagens fornecidas pelos sistemas de tipo especificado pelo programador incluem:

  • Abstração (ou modularidade ) - os tipos permitem que os programadores pensem em um nível mais alto do que o bit ou byte, sem se preocupar com a implementação de baixo nível. Por exemplo, os programadores podem começar a pensar em uma string como um conjunto de valores de caracteres em vez de uma mera matriz de bytes. Mais ainda, os tipos permitem que os programadores pensem e expressem interfaces entre dois subsistemas de qualquer tamanho. Isso permite mais níveis de localização para que as definições necessárias para a interoperabilidade dos subsistemas permaneçam consistentes quando esses dois subsistemas se comunicam.
  • Documentação - em sistemas de tipos mais expressivos, os tipos podem servir como uma forma de documentação esclarecendo a intenção do programador. Por exemplo, se um programador declara uma função como retornando um tipo de carimbo de data / hora, isso documenta a função quando o tipo de carimbo de data / hora pode ser declarado explicitamente mais profundamente no código como um tipo inteiro.

As vantagens fornecidas pelos sistemas de tipo especificado pelo compilador incluem:

  • Otimização - a verificação de tipo estática pode fornecer informações úteis em tempo de compilação. Por exemplo, se um tipo requer que um valor seja alinhado na memória em um múltiplo de quatro bytes, o compilador pode ser capaz de usar instruções de máquina mais eficientes.
  • Segurança - um sistema de tipo permite que o compilador detecte código inválido ou sem sentido. Por exemplo, podemos identificar uma expressão 3 / "Hello, World"como inválida, quando as regras não especificam como dividir um inteiro por uma string . Uma digitação forte oferece mais segurança, mas não pode garantir a segurança de digitação completa .

Erros de digitação

Um erro de tipo é uma condição não intencional que pode se manifestar em vários estágios de desenvolvimento de um programa. Portanto, uma facilidade para detecção do erro é necessária no sistema de tipos. Em algumas linguagens, como Haskell, para a qual a inferência de tipo é automatizada, o lint pode estar disponível para seu compilador para ajudar na detecção de erros.

A segurança de tipo contribui para a correção do programa , mas pode apenas garantir a correção ao custo de tornar a própria verificação de tipo um problema indecidível . Em um sistema de tipo com verificação automática de tipo, um programa pode ser executado incorretamente, mas não produz erros de compilador. A divisão por zero é uma operação insegura e incorreta, mas um verificador de tipo em execução apenas em tempo de compilação não verifica a divisão por zero na maioria das linguagens e, em seguida, é deixado como um erro de tempo de execução . Para provar a ausência desses defeitos, outros tipos de métodos formais , conhecidos coletivamente como análises de programa , são de uso comum. Como alternativa, um sistema de tipos suficientemente expressivo, como em linguagens com tipos dependentes, pode evitar esses tipos de erros (por exemplo, expressar o tipo de números diferentes de zero ). Além disso , o teste de software é um método empírico para localizar erros que o verificador de tipo não consegue detectar.

Verificação de tipo

O processo de verificar e impor as restrições de tipos - verificação de tipo - pode ocorrer em tempo de compilação (uma verificação estática) ou em tempo de execução . Se a especificação de uma linguagem exige fortemente suas regras de digitação (ou seja, permitindo mais ou menos apenas as conversões automáticas de tipo que não perdem informações), pode-se referir ao processo como fortemente tipado , se não, como fracamente tipado . Os termos geralmente não são usados ​​em sentido estrito.

Verificação de tipo estático

A verificação estática de tipo é o processo de verificação da segurança de tipo de um programa com base na análise do texto de um programa ( código-fonte ). Se um programa for aprovado em um verificador de tipo estático, o programa terá a garantia de satisfazer algum conjunto de propriedades de segurança de tipo para todas as entradas possíveis.

A verificação estática de tipo pode ser considerada uma forma limitada de verificação de programa (consulte segurança de tipo ) e, em uma linguagem de tipo seguro, também pode ser considerada uma otimização. Se um compilador pode provar que um programa está bem tipado, então ele não precisa emitir verificações de segurança dinâmicas, permitindo que o binário compilado resultante execute mais rápido e seja menor.

A verificação estática de tipo para linguagens Turing-completas é inerentemente conservadora. Ou seja, se um sistema de tipos é sólido (o que significa que rejeita todos os programas incorretos) e decidível (o que significa que é possível escrever um algoritmo que determina se um programa está bem tipado), então ele deve ser incompleto (ou seja, são programas corretos, que também são rejeitados, embora não encontrem erros de tempo de execução). Por exemplo, considere um programa que contém o código:

if <complex test> then <do something> else <signal that there is a type error>

Mesmo que a expressão <complex test>sempre seja avaliada como trueem tempo de execução, a maioria dos verificadores de tipo rejeitará o programa como incorreto, porque é difícil (se não impossível) para um analisador estático determinar que o elsedesvio não será obtido. Conseqüentemente, um verificador de tipo estático detectará rapidamente erros de tipo em caminhos de código raramente usados. Sem a verificação de tipo estática, mesmo os testes de cobertura de código com 100% de cobertura podem ser incapazes de encontrar tais erros de tipo. Os testes podem falhar na detecção de tais erros de tipo, porque a combinação de todos os locais onde os valores são criados e todos os locais onde um determinado valor é usado deve ser levada em consideração.

Vários recursos úteis e comuns de linguagem de programação não podem ser verificados estaticamente, como downcasting . Portanto, muitas linguagens terão verificação de tipo estática e dinâmica; o verificador de tipo estático verifica o que pode e as verificações dinâmicas verificam o resto.

Muitas linguagens com verificação de tipo estático fornecem uma maneira de contornar o verificador de tipo. Algumas linguagens permitem que os programadores escolham entre segurança de tipo estática e dinâmica. Por exemplo, C # distingue entre variáveis tipadas estaticamente e dinamicamente . Os usos do primeiro são verificados estaticamente, enquanto os usos do último são verificados dinamicamente. Outras linguagens permitem escrever código que não é seguro para tipos; por exemplo, em C , os programadores podem lançar livremente um valor entre quaisquer dois tipos que tenham o mesmo tamanho, efetivamente subvertendo o conceito de tipo.

Para obter uma lista de idiomas com verificação de tipo estático, consulte a categoria de idiomas com tipo estático .

Verificação de tipo dinâmico e informações de tipo de tempo de execução

A verificação dinâmica de tipo é o processo de verificação da segurança de tipo de um programa em tempo de execução. Implementações de linguagens com verificação de tipo dinâmica geralmente associam cada objeto de tempo de execução com uma tag de tipo (ou seja, uma referência a um tipo) contendo suas informações de tipo. Essas informações de tipo de tempo de execução (RTTI) também podem ser usadas para implementar despacho dinâmico , vinculação tardia , downcasting , reflexão e recursos semelhantes.

A maioria das linguagens de tipo seguro inclui alguma forma de verificação de tipo dinâmica, mesmo que também tenha um verificador de tipo estático. A razão para isso é que muitos recursos ou propriedades úteis são difíceis ou impossíveis de verificar estaticamente. Por exemplo, suponha que um programa defina dois tipos, A e B, onde B é um subtipo de A. Se o programa tenta converter um valor do tipo A para o tipo B, que é conhecido como downcasting , a operação é válida apenas se o valor que está sendo convertido é na verdade um valor do tipo B. Portanto, uma verificação dinâmica é necessária para verificar se a operação é segura. Este requisito é uma das críticas ao downcasting.

Por definição, a verificação de tipo dinâmico pode fazer com que um programa falhe em tempo de execução. Em algumas linguagens de programação, é possível antecipar e se recuperar dessas falhas. Em outros, os erros de verificação de tipo são considerados fatais.

Linguagens de programação que incluem verificação de tipo dinâmico, mas não verificação de tipo estático, são freqüentemente chamadas de "linguagens de programação de tipo dinâmico". Para obter uma lista dessas linguagens, consulte a categoria de linguagens de programação digitadas dinamicamente .

Combinando verificação de tipo estática e dinâmica

Alguns idiomas permitem a digitação estática e dinâmica. Por exemplo, Java e algumas outras linguagens ostensivamente tipificadas estaticamente suportam tipos de downcasting para seus subtipos , consultando um objeto para descobrir seu tipo dinâmico e outras operações de tipo que dependem de informações de tipo de tempo de execução. Outro exemplo é C ++ RTTI . De modo mais geral, a maioria das linguagens de programação inclui mecanismos para despachar diferentes 'tipos' de dados, como uniões disjuntas , polimorfismo de tempo de execução e tipos variantes . Mesmo quando não está interagindo com anotações de tipo ou verificação de tipo, tais mecanismos são materialmente semelhantes às implementações de tipagem dinâmica. Veja linguagem de programação para mais discussão sobre as interações entre tipagem estática e dinâmica.

Os objetos em linguagens orientadas a objetos são geralmente acessados ​​por uma referência cujo tipo de destino estático (ou tipo de manifesto) é igual ao tipo de tempo de execução do objeto (seu tipo latente) ou a um supertipo dele. Isso está em conformidade com o princípio de substituição de Liskov , que afirma que todas as operações realizadas em uma instância de um determinado tipo também podem ser realizadas em uma instância de um subtipo. Este conceito também é conhecido como polimorfismo de subsunção ou subtipo . Em algumas linguagens, os subtipos também podem possuir tipos de retorno covariante ou contravariante e tipos de argumento, respectivamente.

Certas linguagens, por exemplo Clojure , Common Lisp ou Cython são verificados dinamicamente por tipo por padrão, mas permitem que os programas optem pela verificação de tipo estático, fornecendo anotações opcionais. Uma razão para usar essas dicas seria otimizar o desempenho de seções críticas de um programa. Isso é formalizado por digitação gradual . O ambiente de programação DrRacket , um ambiente pedagógico baseado em Lisp, e precursor da linguagem Racket, também é soft-typed.

Por outro lado, a partir da versão 4.0, a linguagem C # fornece uma maneira de indicar que uma variável não deve ser verificada estaticamente. Uma variável cujo tipo é dynamicnão estará sujeita à verificação de tipo estático. Em vez disso, o programa depende das informações do tipo de tempo de execução para determinar como a variável pode ser usada.

Em Rust , o tipo fornece tipagem dinâmica de tipos. std::any'static

Verificação de tipo estática e dinâmica na prática

A escolha entre tipagem estática e dinâmica requer certas compensações .

A tipagem estática pode encontrar erros de tipo de forma confiável em tempo de compilação, o que aumenta a confiabilidade do programa entregue. No entanto, os programadores discordam sobre a frequência com que ocorrem os erros de tipo, resultando em discordâncias adicionais sobre a proporção dos bugs codificados que seriam detectados pela representação adequada dos tipos projetados no código. Os defensores da tipagem estática acreditam que os programas são mais confiáveis ​​quando foram bem verificados, enquanto os defensores da tipagem dinâmica apontam para o código distribuído que se provou confiável e para pequenos bancos de dados de bugs. O valor da tipagem estática aumenta à medida que a força do sistema de tipos aumenta. Os defensores da tipagem dependente , implementada em linguagens como Dependent ML e Epigram , sugeriram que quase todos os bugs podem ser considerados erros de tipo, se os tipos usados ​​em um programa forem declarados corretamente pelo programador ou inferidos corretamente pelo compilador.

A tipagem estática geralmente resulta em código compilado que executa mais rápido. Quando o compilador conhece os tipos de dados exatos que estão em uso (o que é necessário para a verificação estática, seja por meio de declaração ou inferência), ele pode produzir código de máquina otimizado. Algumas linguagens com tipos dinâmicos, como Common Lisp, permitem declarações de tipo opcionais para otimização por esse motivo.

Por outro lado, a tipagem dinâmica pode permitir que os compiladores rodem mais rápido e os interpretadores carreguem novos códigos dinamicamente, porque as alterações no código-fonte em linguagens tipadas dinamicamente podem resultar em menos verificação para executar e menos código para revisitar. Isso também pode reduzir o ciclo de edição-compilação-teste-depuração.

Linguagens estaticamente tipadas que não têm inferência de tipo (como C e Java antes da versão 10 ) requerem que os programadores declarem os tipos que um método ou função deve usar. Isso pode servir como documentação de programa adicionada, que é ativa e dinâmica, em vez de estática. Isso permite que um compilador evite que ele saia da sincronia e seja ignorado pelos programadores. No entanto, uma linguagem pode ser digitada estaticamente sem exigir declarações de tipo (os exemplos incluem Haskell , Scala , OCaml , F # e, em menor extensão, C # e C ++ ), portanto, a declaração explícita de tipo não é um requisito necessário para a digitação estática em todas as linguagens.

A tipagem dinâmica permite construções que alguma verificação de tipo estático (simples) rejeitaria como ilegal. Por exemplo, funções eval , que executam dados arbitrários como código, tornam-se possíveis. Uma função eval é possível com tipagem estática, mas requer usos avançados de tipos de dados algébricos . Além disso, a tipagem dinâmica acomoda melhor o código transicional e a prototipagem, como permitir que uma estrutura de dados de espaço reservado ( objeto simulado ) seja usada de forma transparente no lugar de uma estrutura de dados completa (geralmente para fins de experimentação e teste).

A tipagem dinâmica normalmente permite a digitação duck (o que permite uma reutilização de código mais fácil ). Muitas linguagens com tipagem estática também apresentam digitação duck ou outros mecanismos, como programação genérica, que também permitem uma reutilização de código mais fácil.

Tipagem dinâmica normalmente torna a metaprogramação mais fácil de usar. Por exemplo, os modelos C ++ são normalmente mais complicados de escrever do que o código Ruby ou Python equivalente, uma vez que C ++ tem regras mais rígidas em relação às definições de tipo (para funções e variáveis). Isso força um desenvolvedor a escrever mais código clichê para um modelo do que um desenvolvedor Python precisaria. Construções de tempo de execução mais avançadas, como metaclasses e introspecção, costumam ser mais difíceis de usar em linguagens de tipo estático. Em algumas linguagens, esses recursos também podem ser usados, por exemplo, para gerar novos tipos e comportamentos em tempo real, com base em dados de tempo de execução. Essas construções avançadas geralmente são fornecidas por linguagens de programação dinâmicas ; muitos deles são digitados dinamicamente, embora a tipagem dinâmica não precise ser relacionada a linguagens de programação dinâmicas .

Sistemas de tipo forte e fraco

Os idiomas são freqüentemente referidos coloquialmente como fortemente tipados ou fracamente tipados . Na verdade, não existe uma definição universalmente aceita do que esses termos significam. Em geral, existem termos mais precisos para representar as diferenças entre os sistemas de tipo que levam as pessoas a chamá-los de "fortes" ou "fracos".

Segurança de tipo e segurança de memória

Uma terceira maneira de categorizar o sistema de tipos de uma linguagem de programação é pela segurança das operações e conversões digitadas. Os cientistas da computação usam o termo linguagem segura de tipos para descrever linguagens que não permitem operações ou conversões que violam as regras do sistema de tipos.

Os cientistas da computação usam o termo linguagem segura para a memória (ou apenas linguagem segura ) para descrever linguagens que não permitem que programas acessem a memória que não foi designada para seu uso. Por exemplo, uma linguagem de memória segura verificará os limites do array , ou então garantirá estaticamente (ou seja, em tempo de compilação antes da execução) que os acessos ao array fora dos limites do array causarão erros em tempo de compilação e talvez em tempo de execução.

Considere o seguinte programa de uma linguagem que é segura para o tipo e para a memória:

var x := 5;   
var y := "37"; 
var z := x + y;

Neste exemplo, a variável zterá o valor 42. Embora possa não ser o que o programador previu, é um resultado bem definido. Se yfosse uma string diferente, que não pudesse ser convertida em um número (por exemplo, "Hello World"), o resultado também seria bem definido. Observe que um programa pode ser seguro para o tipo ou para a memória e ainda assim travar em uma operação inválida. Isso é para linguagens em que o sistema de tipos não é suficientemente avançado para especificar com precisão a validade das operações em todos os operandos possíveis. Porém, se um programa encontrar uma operação que não seja segura para o tipo, encerrar o programa geralmente é a única opção.

Agora considere um exemplo semelhante em C:

int x = 5;
char y[] = "37";
char* z = x + y;
printf("%c\n", *z);

Neste exemplo, irá apontar para um endereço de memória cinco caracteres além , equivalente a três caracteres após o caractere zero de terminação da string apontada por . Esta é a memória que o programa não deve acessar. Ele pode conter dados inúteis e certamente não contém nada de útil. Como mostra este exemplo, C não é uma linguagem segura para a memória nem segura para tipos. zyy

Em geral, segurança de tipo e segurança de memória andam de mãos dadas. Por exemplo, uma linguagem que suporta aritmética de ponteiro e conversões de número para ponteiro (como C) não é segura para a memória nem para tipos, porque permite que a memória arbitrária seja acessada como se fosse uma memória válida de qualquer tipo.

Para obter mais informações, consulte segurança da memória .

Níveis variáveis ​​de verificação de tipo

Algumas linguagens permitem que diferentes níveis de verificação se apliquem a diferentes regiões do código. Exemplos incluem:

  • A use strictdiretiva em JavaScript e Perl aplica uma verificação mais forte.
  • O declare(strict_types=1)no PHP em uma base por arquivo permite que apenas uma variável do tipo exato da declaração de tipo seja aceita, ou um TypeErrorserá lançado.
  • O Option Strict Onem VB.NET permite que o compilador exija uma conversão entre objetos.

Ferramentas adicionais, como lint e IBM Rational Purify, também podem ser usadas para atingir um nível mais alto de rigidez.

Sistemas de tipo opcional

Foi proposto, principalmente por Gilad Bracha , que a escolha do sistema de tipos seja feita independentemente da escolha da linguagem; que um sistema de tipos deve ser um módulo que pode ser conectado a uma linguagem conforme necessário. Ele acredita que isso é vantajoso, porque o que ele chama de sistemas de tipos obrigatórios tornam as linguagens menos expressivas e o código mais frágil. O requisito de que o sistema de tipos não afeta a semântica da linguagem é difícil de cumprir.

A digitação opcional está relacionada, mas é diferente da digitação gradual . Embora ambas as disciplinas de digitação possam ser usadas para realizar análises estáticas de código ( digitação estática ), os sistemas de tipos opcionais não reforçam a segurança de tipos em tempo de execução ( digitação dinâmica ).

Polimorfismo e tipos

O termo polimorfismo se refere à capacidade do código (especialmente, funções ou classes) de agir sobre valores de vários tipos, ou à capacidade de diferentes instâncias da mesma estrutura de dados de conter elementos de diferentes tipos. Sistemas de tipo que permitem polimorfismo geralmente o fazem a fim de melhorar o potencial de reutilização de código: em uma linguagem com polimorfismo, os programadores precisam apenas implementar uma estrutura de dados como uma lista ou uma matriz associativa uma vez, em vez de uma para cada tipo de elemento com o qual eles planejam usá-lo. Por esta razão, os cientistas da computação às vezes chamam o uso de certas formas de polimorfismo de programação genérica . Os fundamentos teóricos do tipo do polimorfismo estão intimamente relacionados aos da abstração , modularidade e (em alguns casos) subtipagem .

Sistemas especializados de tipo

Muitos sistemas de tipo foram criados que são especializados para uso em certos ambientes com certos tipos de dados ou para análise de programa estático fora de banda . Freqüentemente, eles são baseados em ideias da teoria de tipo formal e estão disponíveis apenas como parte de sistemas de pesquisa de protótipos.

A tabela a seguir fornece uma visão geral sobre os conceitos teóricos de tipo que são usados ​​em sistemas de tipo especializados. Os nomes M, N, O variam sobre os termos e os nomes variam sobre os tipos. A notação (resp. ) Descreve o tipo que resulta da substituição de todas as ocorrências da variável de tipo α (resp. Variável de termo x ) em τ pelo tipo σ (resp. Termo N ).

Noção de tipo Notação Significado
Função Se M tem tipo e N tem tipo σ , então a aplicação tem tipo τ .
produtos Se M tem tipo , então é um par tal que N tem tipo σ e O tem tipo τ .
Soma Se M tem tipo , então ou é a primeira injeção tal que N tem tipo σ , ou

é a segunda injeção tal que N tem tipo τ .

Interseção Se M tem tipo , então M tem tipo σ e M tem tipo τ .
União Se M tem tipo , então M tem tipo σ ou M tem tipo τ .
Registro Se M tem tipo , então M tem um membro x que tem tipo τ .
Polimórfico Se M tem tipo , então M tem tipo para qualquer tipo σ .
Existencial Se M tem tipo , então M tem tipo para algum tipo σ .
Recursiva Se M tem tipo , então M tem tipo .
Função dependente Se M tiver tipo e N tiver tipo σ , o aplicativo terá tipo .
Produto dependente Se M tem tipo , então é um par tal que N tem tipo σ e O tem tipo .
Cruzamento dependente Se M tem tipo , então M tem tipo σ e M tem tipo .
Interseção familiar Se M tem tipo , então M tem tipo para qualquer termo N do tipo σ .
União familiar Se M tem tipo , então M tem tipo para algum termo N do tipo σ .

Tipos dependentes

Os tipos dependentes são baseados na ideia de usar escalares ou valores para descrever mais precisamente o tipo de algum outro valor. Por exemplo, pode ser o tipo de uma matriz. Podemos então definir regras de digitação, como a seguinte regra para multiplicação de matrizes:

onde k , m , n são valores inteiros positivos arbitrários. Uma variante do ML chamada Dependent ML foi criada com base neste sistema de tipos, mas como a verificação de tipo para tipos dependentes convencionais é indecidível , nem todos os programas que os usam podem ser verificados sem algum tipo de limite. O ML dependente limita o tipo de igualdade que pode decidir à aritmética Presburger .

Outras linguagens, como Epigram, tornam o valor de todas as expressões na linguagem decidível para que a verificação de tipo possa ser decidida. No entanto, em geral, a prova de decidibilidade é indecidível , portanto, muitos programas requerem anotações escritas à mão que podem ser muito pouco triviais. Como isso impede o processo de desenvolvimento, muitas implementações de linguagem fornecem uma saída fácil na forma de uma opção para desativar essa condição. Isso, no entanto, tem o custo de fazer o verificador de tipo rodar em um loop infinito quando alimentado por programas que não fazem a verificação de tipo, fazendo com que a compilação falhe.

Tipos lineares

Os tipos lineares , baseados na teoria da lógica linear e intimamente relacionados aos tipos de exclusividade , são tipos atribuídos a valores que possuem a propriedade de terem uma e somente uma referência a eles o tempo todo. Eles são valiosos para descrever grandes valores imutáveis , como arquivos, strings e assim por diante, porque qualquer operação que destrói simultaneamente um objeto linear e cria um objeto semelhante (como ' str= str + "a"') pode ser otimizada "por baixo do capô" em um mutação de lugar. Normalmente isso não é possível, pois tais mutações podem causar efeitos colaterais em partes do programa que contêm outras referências ao objeto, violando a transparência referencial . Eles também são usados ​​no protótipo do sistema operacional Singularity para comunicação entre processos, garantindo estaticamente que os processos não possam compartilhar objetos na memória compartilhada para evitar condições de corrida. A linguagem Clean (uma linguagem semelhante a Haskell ) usa este tipo de sistema para ganhar bastante velocidade (em comparação com a realização de uma cópia profunda) enquanto permanece segura.

Tipos de interseção

Intersecção tipos são tipos descrevem valores que pertencem a ambos de dois outros tipos de dados com sobreposição de conjuntos de valores. Por exemplo, na maioria das implementações de C, o char assinado tem um intervalo de -128 a 127 e o unsigned char tem um intervalo de 0 a 255, então o tipo de interseção desses dois tipos deve ter um intervalo de 0 a 127. Esse tipo de interseção pode ser ultrapassado com segurança em funções que esperam tanto caracteres assinados ou não assinados, porque ele é compatível com ambos os tipos.

Os tipos de interseção são úteis para descrever tipos de função sobrecarregados: por exemplo, se " → " é o tipo de função que recebe um argumento inteiro e retorna um inteiro e " → " é o tipo de função que recebe um argumento flutuante e retorna um flutuante, então a interseção desses dois tipos pode ser usada para descrever funções que fazem um ou outro, com base no tipo de entrada que recebem. Tal função poderia ser passada para outra função esperando uma função " → " com segurança; ele simplesmente não usaria a funcionalidade " → ". intintfloatfloatintintfloatfloat

Em uma hierarquia de subclasses, a interseção de um tipo e um tipo ancestral (como seu pai) é o tipo mais derivado. A interseção dos tipos de irmãos está vazia.

A linguagem Forsythe inclui uma implementação geral dos tipos de interseção. Uma forma restrita são os tipos de refinamento .

Tipos de união

Tipos de união são tipos que descrevem valores que pertencem a um dos dois tipos. Por exemplo, em C, o char assinado tem um intervalo de -128 a 127, e o char não assinado tem um intervalo de 0 a 255, então a união desses dois tipos teria um intervalo "virtual" geral de -128 a 255 que pode ser usado parcialmente dependendo de qual membro do sindicato é acessado. Qualquer função que lida com esse tipo de união teria que lidar com inteiros nesse intervalo completo. De modo mais geral, as únicas operações válidas em um tipo de união são as operações válidas em ambos os tipos que estão sendo unidos. O conceito de "união" do C é semelhante aos tipos de união, mas não é seguro para tipos, pois permite operações que são válidas em qualquer um dos tipos, em vez de em ambos . Os tipos de união são importantes na análise do programa, onde são usados ​​para representar valores simbólicos cuja natureza exata (por exemplo, valor ou tipo) não é conhecida.

Em uma hierarquia de subclasses, a união de um tipo e um tipo ancestral (como seu pai) é o tipo ancestral. A união de tipos de irmãos é um subtipo de seu ancestral comum (ou seja, todas as operações permitidas em seu ancestral comum são permitidas no tipo de união, mas também podem ter outras operações válidas em comum).

Tipos existenciais

Os tipos existenciais são freqüentemente usados ​​em conexão com os tipos de registro para representar módulos e tipos de dados abstratos , devido à sua capacidade de separar a implementação da interface. Por exemplo, o tipo "T = ∃X {a: X; f: (X → int);}" descreve uma interface de módulo que tem um membro de dados denominado a do tipo X e uma função denominada f que leva um parâmetro de mesmo tipo X e retorna um inteiro. Isso poderia ser implementado de diferentes maneiras; por exemplo:

  • intT = {a: int; f: (int → int); }
  • floatT = {a: float; f: (float → int); }

Esses tipos são ambos subtipos do tipo existencial mais geral T e correspondem a tipos de implementação concretos, portanto, qualquer valor de um desses tipos é um valor do tipo T. Dado um valor "t" do tipo "T", sabemos que " tf (ta)" é bem-digitado, independentemente do que o tipo abstrato X é. Isso dá flexibilidade para escolher os tipos adequados a uma implementação específica, enquanto os clientes que usam apenas valores do tipo de interface - o tipo existencial - ficam isolados dessas escolhas.

Em geral, é impossível para o inspetor de tipos inferir a qual tipo existencial um determinado módulo pertence. No exemplo acima intT {a: int; f: (int → int); } também pode ter o tipo ∃X {a: X; f: (int → int); } A solução mais simples é anotar cada módulo com seu tipo pretendido, por exemplo:

  • intT = {a: int; f: (int → int); } como ∃X {a: X; f: (X → int); }

Embora tipos de dados abstratos e módulos tenham sido implementados em linguagens de programação por algum tempo, foi somente em 1988 que John C. Mitchell e Gordon Plotkin estabeleceram a teoria formal sob o slogan: "Tipos abstratos [dados] têm tipo existencial". A teoria é um cálculo lambda tipado de segunda ordem semelhante ao Sistema F , mas com quantificação existencial em vez de universal.

Digitação gradual

A tipagem gradual é um sistema de tipo no qual as variáveis ​​podem ser atribuídas a um tipo em tempo de compilação (que é a tipagem estática) ou em tempo de execução (que é a tipagem dinâmica), permitindo que os desenvolvedores de software escolham qualquer paradigma de tipo conforme apropriado, de dentro um único idioma. Em particular, a tipagem gradual usa um tipo especial denominado dinâmico para representar tipos estaticamente desconhecidos, e a tipagem gradual substitui a noção de igualdade de tipo por uma nova relação chamada consistência que relaciona o tipo dinâmico a todos os outros tipos. A relação de consistência é simétrica, mas não transitiva.

Declaração e inferência explícita ou implícita

Muitos sistemas de tipo estático, como os de C e Java, requerem declarações de tipo : o programador deve associar explicitamente cada variável a um tipo específico. Outros, como o de Haskell, realizam inferência de tipo : o compilador tira conclusões sobre os tipos de variáveis ​​com base em como os programadores usam essas variáveis. Por exemplo, dada uma função que soma e junta, o compilador pode inferir isso e deve ser números - uma vez que a adição só é definida para números. Assim, qualquer chamada para outro lugar no programa que especifica um tipo não numérico (como uma string ou lista) como um argumento, sinalizaria um erro. f(x, y)xyxyf

As constantes e expressões numéricas e de string no código podem e muitas vezes implicam em um tipo em um contexto específico. Por exemplo, uma expressão 3.14pode implicar em um tipo de ponto flutuante , enquanto pode implicar em uma lista de inteiros - normalmente uma matriz . [1, 2, 3]

A inferência de tipos é geralmente possível, se for computável no sistema de tipos em questão. Além disso, mesmo se a inferência não for computável em geral para um determinado sistema de tipo, a inferência é freqüentemente possível para um grande subconjunto de programas do mundo real. O sistema de tipos de Haskell, uma versão de Hindley-Milner , é uma restrição do Sistema Fω aos chamados tipos polimórficos de classificação 1, nos quais a inferência de tipo é computável. A maioria dos compiladores Haskell permite o polimorfismo de classificação arbitrária como uma extensão, mas isso torna a inferência de tipo não computável. (A verificação de tipo é decidível , no entanto, e os programas de classificação 1 ainda têm inferência de tipo; programas polimórficos de classificação superior são rejeitados, a menos que sejam fornecidas anotações de tipo explícitas.)

Problemas de decisão

Um sistema de tipo que atribui tipos a termos em ambientes de tipo usando regras de tipo está naturalmente associado aos problemas de decisão de verificação de tipo , tipabilidade e ocupação de tipo .

  • Dado um ambiente de tipo , um termo e um tipo , decida se o termo pode ser atribuído ao tipo no ambiente de tipo.
  • Dado um termo , decida se existe um ambiente de tipo e um tipo de modo que o termo possa ser atribuído ao tipo no ambiente de tipo .
  • Dado um ambiente de tipo e um tipo , decida se existe um termo que pode ser atribuído ao tipo no ambiente de tipo.

Sistema de tipo unificado

Algumas linguagens como C # ou Scala possuem um sistema de tipos unificado. Isso significa que todos os tipos C #, incluindo tipos primitivos, herdam de um único objeto raiz. Cada tipo em C # herda da classe Object. Algumas linguagens, como Java e Raku , têm um tipo de raiz, mas também têm tipos primitivos que não são objetos. Java fornece tipos de objeto wrapper que existem junto com os tipos primitivos para que os desenvolvedores possam usar os tipos de objeto wrapper ou os tipos primitivos não-objeto mais simples. Raku converte automaticamente tipos primitivos em objetos quando seus métodos são acessados.

Compatibilidade: equivalência e subtipagem

Um verificador de tipo para uma linguagem tipificada estaticamente deve verificar se o tipo de qualquer expressão é consistente com o tipo esperado pelo contexto no qual essa expressão aparece. Por exemplo, em uma instrução de atribuição do formulário , o tipo inferido da expressão deve ser consistente com o tipo declarado ou inferido da variável . Essa noção de consistência, chamada de compatibilidade , é específica para cada linguagem de programação. x := eex

Se o tipo de ee o tipo de xforem iguais e a atribuição for permitida para esse tipo, então esta é uma expressão válida. Assim, nos sistemas de tipos mais simples, a questão de saber se dois tipos são compatíveis reduz-se à de se eles são iguais (ou equivalentes ). Linguagens diferentes, no entanto, têm critérios diferentes para quando duas expressões de tipo são entendidas para denotar o mesmo tipo. Essas diferentes teorias equacionais de tipos variam amplamente, dois casos extremos sendo sistemas de tipo estrutural , em que quaisquer dois tipos que descrevem valores com a mesma estrutura são equivalentes, e sistemas de tipo nominativo , em que duas expressões de tipo sintaticamente distintas não denotam o mesmo tipo ( ou seja , os tipos devem ter o mesmo "nome" para serem iguais).

Em linguagens com subtipagem , a relação de compatibilidade é mais complexa. Em particular, se Bfor um subtipo de A, então um valor de tipo Bpode ser usado em um contexto onde um de tipo Aé esperado ( covariante ), mesmo se o inverso não for verdadeiro. Assim como a equivalência, a relação de subtipo é definida de forma diferente para cada linguagem de programação, com muitas variações possíveis. A presença de polimorfismo paramétrico ou ad hoc em uma linguagem também pode ter implicações para compatibilidade de tipo.

Veja também

Notas

Referências

Leitura adicional

links externos