Tipo de sistema

Da Wikipédia, a enciclopédia livre
Ir para a navegação Saltar para pesquisar

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 . [1] 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 of float", "function return boolean"). O principal objetivo de um sistema de tipos é reduzir as possibilidades de bugsem programas de computador [2] definindo interfaces entre diferentes partes de um programa de computador e, em seguida, verificando 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 outros propósitos, como expressar regras de negócios, permitir certas otimizações do compilador, permitir despacho 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 tipos 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 essa operação não faz sentido (erros de validade). Os sistemas de tipos geralmente são especificados como parte das linguagens de programação e incorporados aos 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 a gramática de tipos originais da linguagem.

Visão geral do uso

Um exemplo de um sistema de tipos simples é o da linguagem C. As partes de um programa C são as definições de função . 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 invocadora indica o nome da função invocada, juntamente com os nomes das variáveis ​​que contêm os valores a serem passados ​​para ela. Durante a execução, os valores são colocados em 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 umvalor de ponto flutuante , o resultado errado será calculado pela função invocada. O compilador C verifica os tipos dos argumentos passados ​​para uma função quando ela é chamada em relação aos tipos dos parâmetros declarados na definição da função. Se os tipos não corresponderem, o compilador lançará um erro em tempo de compilação.

Um compilador também pode usar o tipo estático de um valor para otimizar o armazenamento necessário 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 . Eles usarão, portanto , operações de microprocessador específicas de ponto flutuante nesses valores (adição de ponto flutuante, multiplicação, etc.).

A profundidade das restrições de tipo e a maneira de sua avaliação afetam a digitação da linguagem. 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 dos tipos. Uma linguagem de programação deve ter a oportunidade de verificação de tipos usando o sistema de tipos, seja em tempo de compilação ou em tempo de execução, anotado manualmente ou inferido automaticamente. Como Mark Manasse colocou concisamente: [3]

O problema fundamental abordado por uma teoria de tipos é garantir que os programas tenham significado. O problema fundamental causado por uma teoria de 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 tipagem , 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 nenhum dos valores possíveis que uma sequência de bits pode significar . [nota 1] Associar uma sequência de bits a um tipo transmite quesignificado para o 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 seja 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 tipos mais elaborado, ela ganha um conjunto de regras mais refinado do que a verificação básica de tipos, 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 código ou considerar operações e funcionamento relacionados ao computador. É um desafio encontrar um sistema de tipos suficientemente expressivo que satisfaça todas as práticas de programação de maneira segura .

Quanto mais restrições de tipo forem impostas pelo compilador, mais fortemente tipada será uma linguagem de programação. As linguagens fortemente tipadas geralmente exigem que o programador faça conversões explícitas em contextos em que uma conversão implícita não causaria danos. O sistema de tipos do Pascal foi descrito como "muito forte" porque, por exemplo, o tamanho de um array ou string faz parte de seu tipo, dificultando algumas tarefas de programação. [4] [5] Haskell também é fortemente tipado, mas seus tipos são inferidos automaticamente, de modo que as conversões explícitas geralmente são 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 de programa sejam verificadas por um verificador de tipos. Além de pares simples de tipo de valor, uma "região" virtual de código está associada a um componente "efeito" que descreve o que está sendo feito com o que e permitindo, por exemplo, "lançar" um relatório de erros. 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 a verificação de tipo.

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 especificados 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 um mero array de bytes. Mais alto 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 comunicarem.
  • 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 para ser um tipo inteiro.

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

  • Otimização – A verificação de tipo estático pode fornecer informações úteis em tempo de compilação. Por exemplo, se um tipo exigir que um valor seja alinhado na memória em um múltiplo de quatro bytes, o compilador poderá usar instruções de máquina mais eficientes.
  • Segurança – Um sistema de tipos permite que o compilador detecte código sem sentido ou inválido. 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 . A digitação forte oferece mais segurança, mas não pode garantir a segurança completa do tipo .

Erros de tipo

Um erro de tipo é uma condição não intencional [ clarificação necessária ] que pode se manifestar em vários estágios do desenvolvimento de um programa. Assim, uma facilidade para detecção do erro é necessária no sistema de tipos. Em algumas linguagens, como Haskell, para as quais a inferência de tipos é automatizada, o lint pode estar disponível para seu compilador para auxiliar 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 . [ citação necessária ] Em um sistema de tipos com verificação de tipo automatizada, 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 tipos executado apenas em tempo de compilação não verifica a divisão por zero na maioria dos idiomas 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 programas, são de uso comum. Alternativamente, um sistema de tipos suficientemente expressivo, como em linguagens de tipagem dependente, 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 encontrar erros que o verificador de tipo não pode detectar.

Verificação de tipo

O processo de verificação e aplicação das restrições de tipos — verificação de tipos — pode ocorrer em tempo de compilação (uma verificação estática) ou em tempo de execução . Se uma especificação de linguagem requer fortemente suas regras de digitação (ou seja, permitindo mais ou menos apenas aquelas 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 um sentido estrito.

Verificação de tipo estático

A verificação estática de tipo é o processo de verificar a segurança de tipo de um programa com base na análise do texto de um programa ( código-fonte ). Se um programa passa por um verificador de tipo estático, é garantido que o programa satisfaça algum conjunto de propriedades de segurança de tipo para todas as entradas possíveis.

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

A verificação de tipo estático para linguagens Turing-completas é inerentemente conservadora. Isto é, 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 é bem tipado), então ele deve ser incompleto (o que significa que há são programas corretos, que também são rejeitados, mesmo que não encontrem erros de tempo de execução). [6] Por exemplo, considere um programa contendo 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 tipos rejeitará o programa como mal tipado, porque é difícil (se não impossível) para um analisador estático determinar que a elseramificação não será executada. [7] 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ático, mesmo os testes de cobertura de código com 100% de cobertura podem não encontrar esses erros de tipo. Os testes podem não detectar tais erros de tipo, pois deve-se levar em consideração a combinação de todos os locais onde os valores são criados e todos os locais onde um determinado valor é utilizado.

Vários recursos de linguagem de programação úteis e comuns não podem ser verificados estaticamente, como downcasting . Assim, 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ático e dinâmico. Por exemplo, C# distingue entre variáveis ​​de tipo estático e de tipo dinâmico . 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, subvertendo efetivamente o conceito de tipo.

Para obter uma lista de idiomas com verificação de tipo estático, consulte a categoria para idiomas de 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. As implementações de linguagens com verificação de tipo dinâmica geralmente associam cada objeto de tempo de execução a uma marca 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 dynamic dispatch , late binding , downcasting , reflection e recursos semelhantes.

A maioria das linguagens de tipo seguro inclui alguma forma de verificação de tipo dinâmico, mesmo que também tenha um verificador de tipo estático. [ citação necessária ] [8] 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 tentar converter um valor do tipo A para o tipo B, que é conhecido como downcasting , então a operação é válida apenas se o valor que está sendo convertido for realmente um valor do tipo B. Assim, é necessária uma verificação dinâmica para verificar se a operação é segura. Essa exigência é 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.

As linguagens de programação que incluem a verificação de tipo dinâmico, mas não a verificação de tipo estática, geralmente são chamadas de "linguagens de programação de tipagem dinâmica". Para obter uma lista dessas linguagens, consulte a categoria de linguagens de programação de tipagem dinâmica .

Combinando verificação de tipo estático e dinâmico

Algumas linguagens permitem digitação estática e dinâmica. Por exemplo, Java e algumas outras linguagens ostensivamente tipadas estaticamente suportam downcasting de tipos 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 maneira 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 de variantes . Mesmo quando não interagindo com anotações de tipo ou verificação de tipo, esses mecanismos são materialmente semelhantes às implementações de tipagem dinâmica. Veja a linguagem de programaçãopara mais discussão sobre as interações entre tipagem estática e dinâmica.

Objetos em linguagens orientadas a objetos geralmente são 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á de acordo com o princípio de substituição de Liskov , que afirma que todas as operações executadas em uma instância de um determinado tipo também podem ser executadas em uma instância de um subtipo. Este conceito também é conhecido como subsunção ou polimorfismo de subtipo . Em algumas linguagens, os subtipos também podem possuir tipos de retorno e tipos de argumento covariantes ou contravariantes , respectivamente.

Certas linguagens, por exemplo Clojure , Common Lisp ou Cython são verificadas dinamicamente por padrão, mas permitem que os programas optem pela verificação estática de tipo 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 pela 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. [9]

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 ter o tipo verificado estaticamente. Uma variável cujo tipo é dynamicnão estará sujeita à verificação de tipo estático. Em vez disso, o programa depende de informações de tipo de tempo de execução para determinar como a variável pode ser usada. [10]

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

Verificação de tipo estático e dinâmico 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 os erros de tipo ocorrem, resultando em mais divergências sobre a proporção desses bugs codificados que seriam capturados pela representação adequada dos tipos projetados no código. [12] [13] Defensores da tipagem estática [ quem? ] acreditam que os programas são mais confiáveis ​​quando são bem verificados, enquanto os defensores da tipagem dinâmica [ quem? ] apontam para código distribuído que provou ser confiável e para pequenos bancos de dados de bugs. [ citação necessária ]O valor da tipagem estática aumenta à medida que a força do sistema de tipos aumenta. Defensores da tipagem dependente , [ quem? ] implementados 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. [14]

A tipagem estática geralmente resulta em código compilado que é executado mais rapidamente. Quando o compilador conhece os tipos de dados exatos que estão em uso (o que é necessário para verificação estática, seja por meio de declaração ou inferência), ele pode produzir código de máquina otimizado. Algumas linguagens de tipagem dinâmica, 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 sejam executados mais rapidamente e os intérpretes carreguem dinamicamente o novo código, porque as alterações no código-fonte em linguagens dinamicamente tipadas podem resultar em menos verificação para executar e menos código para revisitar. [ esclarecimento necessário ] Isso também pode reduzir o ciclo de edição-compilação-teste-depuração.

As linguagens de tipagem estática que não possuem inferência de tipo (como C e Java anteriores à versão 10 ) exigem que os programadores declarem os tipos que um método ou função deve usar. Isso pode servir como documentação adicional do programa, 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 (exemplos incluem Haskell , Scala , OCaml , F# e, em menor grau , C# e C++), portanto, a declaração de tipo explícita não é um requisito necessário para a tipagem estática em todos os idiomas.

A tipagem dinâmica permite construções que algumas verificações de tipo estático (simples) rejeitariam como ilegais. 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 de transição 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 de pato (o que facilita a reutilização de código ). Muitas linguagens [ especificar ] com tipagem estática também apresentam a tipagem de pato ou outros mecanismos, como programação genérica, que também permitem a 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 tipicamente mais complicados de escrever do que o código Ruby ou Python equivalente, pois o C++ tem regras mais fortes 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çãosão muitas vezes mais difíceis de usar em linguagens de tipagem estática. 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 tipados dinamicamente, embora a tipagem dinâmica não precise estar relacionada a linguagens de programação dinâmicas .

Sistemas de tipos fortes e fracos

As línguas são muitas vezes referidas coloquialmente como fortemente tipadas ou fracamente tipadas . 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 tipos 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 tipadas. Cientistas da computação usam o termo type-safe language para descrever linguagens que não permitem operações ou conversões que violem 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 segura para a memória verificará os limites do array , ou então garantirá estaticamente (ou seja, em tempo de compilação antes da execução) que o acesso ao array fora dos limites do array causará erros em tempo de compilação e talvez em tempo de execução.

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

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

Neste exemplo, a variável zterá o valor 42. Embora isso possa não ser o que o programador antecipou, é um resultado bem definido. Se yfosse uma string diferente, uma que não pudesse ser convertida em um número (por exemplo, "Hello World"), o resultado também estaria bem definido. Observe que um programa pode ser seguro de tipo ou de memória e ainda 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. Mas se um programa encontrar uma operação que não seja de tipo seguro, encerrar o programa geralmente é a única opção.

Agora considere um exemplo semelhante em C:

intx = 5 ; _   
caractere y [] = "37" ;   
caractere * 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 final 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 útil. Como este exemplo mostra, C não é uma linguagem de memória nem de tipo seguro. 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 o tipo, 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 sejam aplicados a diferentes regiões de código. Exemplos incluem:

  • A use strictdiretiva em JavaScript [16] [17] [18] e Perl aplica uma verificação mais forte.
  • O declare(strict_types=1)em PHP [19] em uma base por arquivo permite que apenas uma variável do tipo exato da declaração de tipo seja aceita, ou a TypeErrorserá lançada.
  • 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 rigor.

Sistemas de tipo opcional

Foi proposto, principalmente por Gilad Bracha , que a escolha do sistema de tipos seja feita independentemente da escolha do idioma; 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, pois o que ele chama de sistemas de tipos obrigatórios torna as linguagens menos expressivas e o código mais frágil. [20] A exigência de que o sistema de tipos não afete a semântica da linguagem é difícil de cumprir.

A digitação opcional está relacionada, mas distinta da digitação gradual . Embora ambas as disciplinas de tipagem possam ser usadas para realizar análise estática de código ( tipagem estática ), os sistemas de tipos opcionais não impõem segurança de tipo em tempo de execução ( tipagem dinâmica ). [20] [21]

Polimorfismo e tipos

O termo polimorfismo refere-se à capacidade do código (especialmente, funções ou classes) de agir em valores de vários tipos, ou à capacidade de diferentes instâncias da mesma estrutura de dados conter elementos de diferentes tipos. Sistemas de tipos que permitem polimorfismo geralmente o fazem para melhorar o potencial de reutilização de código: em uma linguagem com polimorfismo, os programadores precisam implementar uma estrutura de dados como uma lista ou um array associativo apenas uma vez, em vez de uma vez para cada tipo de elemento com o qual 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 da teoria dos tipos do polimorfismo estão intimamente relacionados aos da abstração ,modularidade e (em alguns casos) subtipagem .

Sistemas de tipos especializados

Muitos sistemas de tipos foram criados especializados para uso em determinados ambientes com determinados tipos de dados ou para análise de programa estático fora de banda . Frequentemente, eles são baseados em ideias da teoria formal dos tipos 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 tipos que são usados ​​em sistemas de tipos especializados. Os nomes M, N, O variam entre os termos e os nomesgama 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. termo variável x ) em τ pelo tipo σ (resp. termo N ).

Noção de tipo Notação Significado
Função Se M tem tipoe N tem tipo σ , então a aplicaçãotem tipo τ .
produtos Se M tem tipo, entãoé um par tal que N tem tipo σ e O tem tipo τ .
Soma Se M tem tipo, qualquer entãoé 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 o tipo σ e M tem o tipo τ .
União Se M tem tipo, então M tem o tipo σ ou M tem o tipo τ .
Registro Se M tem tipo, então M tem um membro x do tipo τ .
Polimórfico Se M tem tipo, então M tem tipopara qualquer tipo σ .
Existencial Se M tem tipo, então M tem tipopara algum tipo σ .
Recursivo Se M tem tipo, então M tem tipo.
Função dependente Se M tem tipoe N tem tipo σ , então a aplicaçãotem tipo.
Produto dependente Se M tem tipo, entãoé um par tal que N tem tipo σ e O tem tipo.
Interseção dependente [22] Se M tem tipo, então M tem o tipo σ e M tem o tipo.
Interseção familiar [22] Se M tem tipo, então M tem tipopara qualquer termo N do tipo σ .
União familiar [22] Se M tem tipo, então M tem tipopara 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 dematriz. 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 ML dependente foi criada com base nesse sistema de tipos, mas como a verificação de tipos para tipos dependentes convencionais é indecidível , nem todos os programas que os utilizam podem ser verificados sem algum tipo de limite. ML dependente limita o tipo de igualdade que pode decidir à aritmética de 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 exigem anotações manuscritas que podem ser muito não 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 desabilitar essa condição. Isso, no entanto, tem o custo de fazer o verificador de tipos rodar em um loop infinito quando alimentados com programas que não verificam tipos, fazendo com que a compilação falhe.

Tipos lineares

Tipos lineares , baseados na teoria da lógica linear , e intimamente relacionados aos tipos de exclusividade , são tipos atribuídos a valores que têm a propriedade de terem uma e apenas uma referência a eles em todos os momentos. Eles são valiosos para descrever grandes valores imutáveis , como arquivos, strings e assim por diante, porque qualquer operação que simultaneamente destrua um objeto linear e crie um objeto semelhante (como ' str= str + "a"') pode ser otimizada "sob o 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 operacionalSingularidade 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 esse sistema de tipos para ganhar muita velocidade (em comparação com a execução de uma cópia profunda) enquanto permanece segura.

Tipos de interseção

Os tipos de interseção são tipos que descrevem valores que pertencem a dois outros tipos com conjuntos de valores sobrepostos. Por exemplo, na maioria das implementações de C, o caractere assinado tem um intervalo de -128 a 127 e o caractere não assinado tem um intervalo de 0 a 255, portanto, o tipo de interseção desses dois tipos teria um intervalo de 0 a 127. Esse tipo de interseção pode ser passado com segurança em funções esperando caracteres assinados ou não assinados, porque é 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 float e retorna um float, então a interseção desses dois tipos pode ser usada para descrever funções que fazem uma ou outra, com base no tipo de entrada que elas recebem. Tal função pode 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 de tipos irmãos está vazia.

A linguagem Forsythe inclui uma implementação geral de 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 caractere assinado tem um intervalo de -128 a 127, e o caractere 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 manipule esse tipo de união teria que lidar com inteiros nesse intervalo completo. De maneira 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 válidas em qualquer tipo, em vez de ambos. Os tipos de união são importantes na análise de programas, 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 irmãos é um subtipo de seu ancestral comum (ou seja, todas as operações permitidas em seu ancestral comum são permitidas no tipo união, mas também podem ter outras operações válidas em comum).

Tipos existenciais

Tipos existenciais são frequentemente usados ​​em conexão com 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 possui um membro de dados denominado a do tipo X e uma função denominada f que recebe um parâmetro do mesmo tipo X e retorna um inteiro. Isso pode 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 tipado, independentemente de qual seja o tipo abstrato X. Isso oferece flexibilidade para escolher tipos adequados a uma implementação específica, enquanto clientes que usam apenas valores do tipo de interface — o tipo existencial — são isolados dessas escolhas.

Em geral, é impossível para o verificador 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, não foi até 1988 que John C. Mitchell e Gordon Plotkin estabeleceram a teoria formal sob o slogan: "Tipos abstratos [dados] têm tipo existencial". [23] 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 tipos no qual as variáveis ​​podem receber um tipo em tempo de compilação (que é tipagem estática) ou em tempo de execução (que é tipagem dinâmica), permitindo que os desenvolvedores de software escolham qualquer paradigma de tipo conforme apropriado, de dentro uma única língua. [24] Em particular, a tipagem gradual usa um tipo especial chamado dynamic 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. [25]

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

Muitos sistemas de tipos estáticos, como os de C e Java, exigem 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 tipos : 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 juntos, o compilador pode inferir isso e deve ser números—já que a adição é definida apenas para números. Assim, qualquer chamada para outro lugar no programa que especifique um tipo não numérico (como uma string ou uma lista) como argumento sinalizaria um erro. f(x, y)xyxyf

Constantes e expressões numéricas e de string no código podem e geralmente implicam tipo em um contexto específico. Por exemplo, uma expressão 3.14pode implicar um tipo de ponto flutuante , enquanto pode implicar uma lista de inteiros—normalmente um array . [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 que a inferência não seja computável em geral para um determinado sistema de tipos, a inferência geralmente é 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 rank 1, nos quais a inferência de tipos é computável. A maioria dos compiladores Haskell permite polimorfismo de classificação arbitrária como uma extensão, mas isso torna a inferência de tipo não computável. ( No entanto, a verificação de tipo é decidível e os programas de classificação 1 ainda têm inferência de tipo; programas polimórficos de classificação mais alta são rejeitados, a menos que sejam fornecidas anotações de tipo explícitas.)

Problemas de decisão

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

  • Dado um ambiente de tipo, um termo, e um tipo, decidir se o termopode ser atribuído o tipono ambiente tipo.
  • Dado um termo, decidir se existe um ambiente de tipoe um tipotal que o termopode ser atribuído o tipono ambiente tipo.
  • Dado um ambiente de tipoe um tipo, decidir se existe um termoque pode ser atribuído ao tipono ambiente tipo.

Sistema de tipo unificado

Algumas linguagens como C# ou Scala possuem um sistema de tipos unificado. [27] 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 raiz, mas também têm tipos primitivos que não são objetos. [28] Java fornece tipos de objetos wrapper que existem junto com os tipos primitivos para que os desenvolvedores possam usar os tipos de objetos wrapper ou os tipos primitivos não-objetos mais simples. O Raku converte automaticamente tipos primitivos em objetos quando seus métodos são acessados. [29]

Compatibilidade: equivalência e subtipagem

Um verificador de tipo para uma linguagem tipada 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, essa é 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 à questão de serem iguais (ou equivalentes ). Linguagens diferentes, no entanto, têm critérios diferentes para quando duas expressões de tipo são entendidas como denotando o mesmo tipo. Essas diferentes teorias equacionais de tipos variam amplamente, sendo dois casos extremos sistemas de tipo estrutural , nos quais 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 em que um de tipo Aé esperado ( covariante ), mesmo que o inverso não seja 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 na compatibilidade de tipos.

Veja também

Notas

  1. A linha de computador Burroughs ALGOL determinava o conteúdo de um local de memória por seus bits de sinalização. Os bits de sinalização especificam o conteúdo de um local de memória. Instrução, tipo de dados e funções são especificados por um código de 3 bits além de seu conteúdo de 48 bits. Apenas o MCP (Master Control Program) poderia escrever nos bits do código de flag.

Referências

  1. ^ Pierce 2002 , p. 1: "Um sistema de tipos é um método sintático tratável para provar a ausência de certos comportamentos do programa classificando frases de acordo com os tipos de valores que elas computam."
  2. ^ Cardelli 2004 , p. 1: "O objetivo fundamental de um sistema de tipos é evitar a ocorrência de erros de execução durante a execução de um programa."
  3. ^ Pierce 2002 , p. 208.
  4. ^ Tyson, JR (25 de abril de 1983). "JRT diz que é culpado - de criar um Pascal utilizável" . Infomundo . Vol. 5, não. 1. p. 66.
  5. ^ Kernighan, Brian (1981). "Por que Pascal não é minha linguagem de programação favorita" . Arquivado a partir do original em 2012-04-06 . Recuperado em 22/10/2011 .
  6. ^ "... qualquer sistema de tipo sólido e decidível deve estar incompleto" —D. Remy (2017). pág. 29, Rémy, Didier. "Sistemas de tipos para linguagens de programação" (PDF) . Recuperado em 26 de maio de 2013 .
  7. ^ Perfure 2002 .
  8. ^ Gaurav Miglani, Gaurav (2018). "Dispatch Método Dinâmico ou Polimorfismo de Tempo de Execução em Java" . Arquivado a partir do original em 2020-12-07 . Recuperado 2021-03-28 .
  9. ^ Wright, Andrew K. (1995). Digitação suave prática (PhD). Universidade do Arroz. HD : 1911/16900 .
  10. ^ "dinâmico (referência C#)" . Biblioteca MSDN . Microsoft . Recuperado em 14 de janeiro de 2014 .
  11. ^ "std::any — Rust" . doc.rust-lang.org . Recuperado 2021-07-07 .
  12. ^ Meijer, Erik; Drayton, Pedro. "Digitação estática sempre que possível, digitação dinâmica quando necessário: o fim da guerra fria entre linguagens de programação" (PDF) . Corporação Microsoft .
  13. ^ Lançador, Amanda; Snively, Paul (2012). "Tipos vs Testes" . InfoQ.
  14. ^ Xi, Hongwei (1998). Tipos Dependentes em Programação Prática (PhD). Departamento de Ciências Matemáticas, Carnegie Mellon University. CiteSeerX 10.1.1.41.548 . 
    Xi, Hongwei; Pfenning, Frank (1999). "Tipos dependentes em programação prática". Anais do 26º Simpósio ACM SIGPLAN-SIGACT sobre Princípios de Linguagens de Programação . ACM. pp. 214-227. CiteSeerX  10.1.1.69.2042 . doi : 10.1145/292540.292560 . ISBN 1581130953. S2CID  245490 .
  15. ^ Visual Basic é um exemplo de uma linguagem que é segura para tipos e memória.
  16. ^ "4.2.2 A Variante Estrita de ECMAScript" . Especificação de linguagem ECMAScript® 2020 (11ª ed.). ECMA. Junho de 2020. ECMA-262.
  17. ^ "Modo estrito - JavaScript" . MDN . Desenvolvedor.mozilla.org. 03-07-2013 . Recuperado 2013-07-17 .
  18. ^ "Modo Estrito (JavaScript)" . MSDN . Microsoft . Recuperado 2013-07-17 .
  19. ^ "Digitação rigorosa" . Manual do PHP: Referência da Linguagem: Funções .
  20. ^ a b Bracha, G. "Tipos plugáveis" (PDF) .
  21. ^ "Claro. É chamado de "digitação gradual", e eu o classificaria como moderno. ..." Existe uma linguagem que permite digitação estática e dinâmica? . estouro de pilha. 2012.
  22. ^ a b c Kopylov, Alexei (2003). "Interseção dependente: Uma nova maneira de definir registros na teoria dos tipos". 18º Simpósio IEEE de Lógica em Ciência da Computação . LICS 2003. IEEE Computer Society. págs. 86-95. CiteSeerX 10.1.1.89.4223 . doi : 10.1109/LICS.2003.1210048 . 
  23. ^ Mitchell, John C.; Plotkin, Gordon D. (julho de 1988). "Tipos abstratos têm tipo existencial" (PDF) . ACM Trans. Programa. Lang. Sist . 10 (3): 470–502. doi : 10.1145/44501.45065 . S2CID 1222153 .  
  24. Siek, Jeremy (24 de março de 2014). "O que é digitação gradual?" .
  25. ^ Siek, Jeremy; Taha, Walid (setembro de 2006). Digitação Gradual para Linguagens Funcionais (PDF) . Esquema e Programação Funcional 2006 . Universidade de Chicago . págs. 81-92.
  26. ^ Barendregt, Henk; Dekkers, Wil; Statman, Richard (20 de junho de 2013). Cálculo lambda com tipos . Cambridge University Press. pág. 66. ISBN 978-0-521-76614-2.
  27. ^ "8.2.4 Tipo unificação do sistema". Especificação da linguagem C# (5ª ed.). ECMA. Dezembro de 2017. ECMA-334.
  28. ^ "Tipos Nativos" . Perl 6 Documentação .
  29. ^ "Numéricos, § Auto-boxing" . Perl 6 Documentação .

Leitura adicional

Links externos