Sistema de tipos

Na programação de computadores , um sistema de tipos é um sistema lógico que compreende um conjunto de regras que atribui uma propriedade chamada tipo (por exemplo, inteiro , ponto flutuante , string ) a cada termo (uma palavra, frase ou outro conjunto de símbolos). Geralmente os termos são construções de linguagem de um programa de computador , como variáveis , expressões , funções ou módulos . [1] Um sistema de tipos determina as operações que podem ser executadas em um termo. Para variáveis, o sistema de tipos determina os valores permitidos desse termo. Os sistemas de tipos formalizam e impõem as categorias implícitas que o programador usa para tipos de dados algébricos , estruturas de dados ou outros componentes (por exemplo, "string", "matriz de float", "função que retorna booleano").

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 a gramática do tipo original da linguagem. O principal objetivo de um sistema de tipos em uma linguagem de programação é reduzir as possibilidades de bugs em programas de computador devido a erros de tipo . [2] 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 tipo permitem definir 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 despacho múltiplo e fornecer uma forma de documentação .

Visão geral do uso

Um exemplo de sistema de tipos simples é o da linguagem C. As partes de um programa C são as definições de funções . Uma função é invocada 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 invocação indica o nome da função invocada, juntamente com os nomes das variáveis ​​que contêm 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 um valor de ponto flutuante , então 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 gerará um erro ou aviso 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 forma como são avaliadas afetam a digitação da linguagem. Uma linguagem de programação pode ainda associar uma operação com diversas resoluções para cada tipo, no caso do 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 sistemas de tipos. Uma linguagem de programação deve ter a oportunidade de verificar o tipo usando o sistema de tipos , seja em tempo de compilação ou tempo de execução, anotado manualmente ou inferido automaticamente. Como Mark Manasse disse de forma concisa: [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.

Atribuir 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 número 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 . [nota 1] 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 muitos 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). Estas 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 tipos (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 .

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 simples pares de tipo de valor, uma "região" virtual de código está associada a um componente de "efeito" que descreve o que está sendo feito com what 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 do tipo especificado pelo programador incluem:

  • Abstração (ou modularidade ) – Os tipos permitem aos programadores pensar em um nível superior ao bit ou byte, não se preocupando com 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 ainda, os tipos permitem que os programadores pensem e expressem interfaces entre dois subsistemas de qualquer tamanho. Isto 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 explicitamente declarado 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 estática de tipo 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 ao compilador detectar 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 segurança completa do tipo .

Erros de tipo

Um erro de tipo ocorre quando uma operação recebe um tipo de dados diferente do esperado. [4] Por exemplo, um erro de tipo aconteceria se uma linha de código dividisse dois números inteiros e recebesse uma sequência de letras em vez de um número inteiro. [4] É uma condição não intencional [nota 2] que pode se manifestar em vários estágios do desenvolvimento de um programa. Portanto, é necessária uma facilidade para detecção do erro no sistema de tipos. Em algumas linguagens, como Haskell, para as quais a inferência de tipo é 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 só pode garantir a correção ao custo de tornar a verificação de tipo em si um problema indecidível (como no problema da parada ). Em um sistema de tipos com verificação automatizada de tipos, um programa pode ser executado incorretamente e ainda assim não produzir erros no compilador. A divisão por zero é uma operação insegura e incorreta, mas um verificador de tipo que só é executado em tempo de compilação não verifica a divisão por zero na maioria das linguagens; essa divisão surgiria 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 tipo 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 tal verificador de tipo não detectaria.

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 (uma verificação dinâmica). 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 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 passar em um verificador de tipo estático, é garantido que o programa satisfará 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 segurança de tipo ) e, em uma linguagem segura de tipo, também pode ser considerada uma otimização. Se um compilador puder provar que um programa está bem digitado, ele não precisará emitir verificações dinâmicas de segurança, permitindo que o binário compilado resultante seja executado mais rapidamente e seja menor.

A verificação de tipo estático para linguagens completas de Turing é inerentemente conservadora. Isto é, se um sistema de tipos é ao mesmo tempo correto (o que significa que ele rejeita todos os programas incorretos) e decidível (o que significa que é possível escrever um algoritmo que determine se um programa é bem digitado), 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 execução). [7] 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 em truetempo de execução, a maioria dos verificadores de tipo rejeitará o programa como mal digitado, porque é difícil (se não impossível) para um analisador estático determinar que a elseramificação não será executada. [8] Conseqüentemente, um verificador de tipo estático detectará rapidamente erros de tipo em caminhos de código raramente usados. Sem verificação de tipo estático, mesmo testes de cobertura de código com 100% de cobertura podem não conseguir encontrar tais erros de tipo. Os testes podem falhar na detecção de tais erros de tipo, pois deve ser levada 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.

Uma série de recursos úteis e comuns da linguagem de programação 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ática fornecem uma maneira de ignorar o verificador de tipo. Algumas linguagens permitem que os programadores escolham entre segurança de tipo estático e dinâmico. Por exemplo, historicamente o C# declara variáveis ​​estaticamente, [9] : 77, Seção 3.2  , mas o C# 4.0 introduz a dynamicpalavra-chave, que é usada para declarar variáveis ​​a serem verificadas dinamicamente em tempo de execução. [9] : 117, Seção 4.1  Outras linguagens permitem escrever código que não é seguro para o tipo; por exemplo, em C , os programadores podem converter livremente um valor entre quaisquer dois tipos que tenham o mesmo tamanho, subvertendo efetivamente o conceito de tipo.

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

Verificação dinâmica de tipo 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 dinamicamente geralmente associam cada objeto de tempo de execução a 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 , ligação tardia , downcasting , reflexão e recursos semelhantes.

A maioria das linguagens com segurança de tipo incluem alguma forma de verificação dinâmica de tipo, mesmo que também tenham um verificador de tipo estático. [10] 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, o que é conhecido como downcasting , então a operação é legal 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 dinâmica de tipo pode fazer com que um programa falhe em tempo de execução. Em algumas linguagens de programação é possível antecipar e recuperar destas 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âmica, mas não verificação de tipo estático, são frequentemente chamadas de "linguagens de programação de tipo dinâmico". Para obter uma lista dessas linguagens, consulte a categoria de linguagens de programação de tipo dinâmico .

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

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 forma 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 interage com anotações de tipo ou verificação de tipo, tais mecanismos são materialmente semelhantes às implementações de digitação dinâmica. Consulte linguagem de programação para obter mais discussões sobre as interações entre tipagem estática e dinâmica.

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. Isto está em conformidade 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 tipo 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 tais 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. [11]

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 por tipo. 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. [12] [9] : 113–119 

Em Rust , o tipo fornece digitação dinâmica de tipos. [13]dyn std::any::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 digitação estática pode encontrar erros de tipo de maneira 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 detectados pela representação adequada dos tipos projetados no código. [14] [15] Defensores da digitação estática [ quem? ] acreditam que os programas são mais confiáveis ​​quando foram bem verificados, enquanto os defensores da digitação dinâmica [ quem? ] apontam para código distribuído que se mostrou confiável e para bancos de dados de pequenos bugs. [ citação necessária ] O valor da digitação estática aumenta à medida que a força do sistema de tipos aumenta. Defensores da digitação 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. [16]

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

Por outro lado, a digitação dinâmica pode permitir que os compiladores sejam executados mais rapidamente e os intérpretes carreguem dinamicamente novo código, porque alterações no código-fonte em linguagens de tipo dinâmico podem resultar em menos verificações 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.

Linguagens de tipo estaticamente que não possuem inferência de tipos (como C e Java anteriores à versão 10 ) exigem que os programadores declarem os tipos que um método ou função deve usar. Isto 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# , Swift e, em menor grau, C# e C++ ), portanto, a declaração explícita de tipo não é um requisito necessário para digitação estática em todas as linguagens .

A digitação 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 digitação estática, mas requer usos avançados de tipos de dados algébricos . Além disso, a digitação 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 digitação dinâmica normalmente permite a digitação duck (o que facilita a reutilização de código ). Muitas linguagens [ especificadas ] com digitação estática também apresentam digitação duck ou outros mecanismos, como programação genérica, que também permitem a reutilização de código mais fácil.

A digitação 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 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 padrão 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 estaticamente. Em algumas linguagens, tais recursos também podem ser usados, por exemplo, para gerar novos tipos e comportamentos dinamicamente, com base em dados de tempo de execução. Tais construções avançadas são frequentemente fornecidas por linguagens de programação dinâmicas ; muitos deles são digitados dinamicamente, embora a digitação dinâmica não precise estar relacionada a linguagens de programação dinâmicas .

Sistemas de tipo forte e fraco

As linguagens são frequentemente chamadas coloquialmente de tipagem forte ou digitação fraca . 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 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 forma 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 de tipo seguro 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 memória (ou apenas linguagem segura ) para descrever linguagens que não permitem que programas acessem memória que não foi designada para seu uso. Por exemplo, uma linguagem segura para memória verificará os limites do array ou garantirá estaticamente (ou seja, em tempo de compilação antes da execução) que 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: [17]

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 tipo ou memória e ainda assim travar em uma operação inválida. Isto é para linguagens onde 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, encerrá-lo geralmente é a única opção.

Agora considere um exemplo semelhante em C:

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

Neste exemplo zapontará para um endereço de memória cinco caracteres além de y, equivalente a três caracteres após o caractere zero final da string apontada por y. Esta é a memória que não se espera que o programa acesse. Em termos C, este é simplesmente um comportamento indefinido e o programa pode fazer qualquer coisa; com um compilador simples, ele pode imprimir qualquer byte armazenado após a string "37". Como mostra este exemplo, C não é seguro para memória. Como os dados arbitrários foram considerados caracteres, também não é uma linguagem de tipo seguro.

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 memória nem segura para tipo, porque permite que memória arbitrária seja acessada como se fosse memória válida de qualquer tipo.

Para obter mais informações, consulte segurança de 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 [18] [19] [20] e Perl aplica uma verificação mais forte.
  • O declare(strict_types=1)PHP [21] por arquivo permite que apenas uma variável do tipo exato da declaração de tipo seja aceita ou seja lançada.TypeError
  • O Option Strict OnVB.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 opcionais

Foi proposto, principalmente por Gilad Bracha , que a escolha do sistema de tipos fosse feita independente 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, porque o que ele chama de sistemas de tipos obrigatórios torna as linguagens menos expressivas e o código mais frágil. [22] O requisito 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 digitação 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 ). [22] [23]

Polimorfismo e tipos

O termo polimorfismo refere-se à 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 conterem elementos de tipos diferentes. Os sistemas de tipos que permitem o polimorfismo geralmente o fazem para 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 um array associativo , 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 teóricos dos tipos do polimorfismo estão intimamente relacionados aos da abstração , modularidade e (em alguns casos) subtipagem .

Sistemas de tipo especializado

Foram criados muitos sistemas de tipos especializados para uso em determinados ambientes com determinados tipos de dados ou para análise de programas estáticos fora de banda . Freqüentemente, estes 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 dos conceitos teóricos de tipos usados ​​em sistemas de tipos especializados. Os nomes M, N, O abrangem termos e os nomes abrangem tipos. A seguinte notação será usada:

  • significa que tem tipo ;
  • é essa aplicação de on ;
  • (resp. ) descreve o tipo que resulta da substituição de todas as ocorrências da variável de tipo α (resp. termo variável x ) pelo tipo σ (resp. termo N ).
Noção de tipo Notação Significado
Função Se e , então .
produtos Se , então é um par st e .
Soma Se , então é o primeiro ponto de injeção ou é o segundo ponto de injeção .
Interseção Se , então e .
União Se , então ou .
Registro Se , então M tem um membro .
Polimórfico Se , então para qualquer tipo σ .
Existencial Se , então para algum tipo σ .
Recursivo Se então .
Função dependente [a] Se e , então .
Par dependente [b] Se , então é um par st e .
Intersecção dependente [24] Se , então e .
Interseção familiar [24] Se , então para qualquer termo .
União familiar [24] Se , então por algum período .
  1. ^ Também conhecido como tipo de produto dependente , já que .
  2. ^ Também conhecido como tipo de soma dependente , pois .

Tipos dependentes

Os tipos dependentes são baseados na ideia de usar escalares ou valores para descrever com mais precisão 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 de 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 utilizam podem ser verificados por tipo sem algum tipo de limite. O ML dependente limita o tipo de igualdade que pode decidir à aritmética de Presburger .

Outras linguagens, como o Epigram, tornam decidível o valor de todas as expressões na linguagem, para que a verificação de tipo possa ser decidível. No entanto, em geral, a prova de decidibilidade é indecidível , por isso muitos programas exigem anotações manuscritas que podem não ser triviais. Como isso impede o processo de desenvolvimento, muitas implementações de linguagem oferecem uma saída fácil na forma de uma opção para desabilitar essa condição. Isso, no entanto, tem o custo de fazer com que o verificador de tipo seja executado em um loop infinito quando alimenta programas que não verificam o tipo, causando falha na compilação.

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 possuem 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 destrua simultaneamente um objeto linear e crie um objeto semelhante (como ' str= str + "a"') pode ser otimizada "nos bastidores" em um in- lugar mutação. Normalmente isso não é possível, pois tais mutações poderiam 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, a fim de evitar condições de corrida. A linguagem Clean (uma linguagem semelhante a Haskell ) usa esse tipo de sistema 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 intervalo de -128 a 127 e o caractere não assinado tem intervalo de 0 a 255, portanto, o tipo de interseção desses dois tipos teria intervalo de 0 a 127. Esse tipo de interseção poderia ser passado com segurança em funções que esperam 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ções sobrecarregadas: por exemplo, se " intint" é o tipo de função que recebe um argumento inteiro e retorna um número inteiro, e " floatfloat" é o tipo de função que recebe um argumento flutuante e retorna um ponto flutuante, então a interseção desses dois tipos pode ser usada para descrever funções que executam uma ou outra, com base no tipo de entrada que recebem. Tal função poderia ser passada para outra função esperando uma função " intint" com segurança; simplesmente não usaria a funcionalidade " floatfloat".

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 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

Os tipos de união são tipos que descrevem valores que pertencem a um dos dois tipos. Por exemplo, em C, o caracter assinado tem um intervalo de -128 a 127, e o caracter não assinado tem um intervalo de 0 a 255, portanto 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 manuseie esse tipo de união teria que lidar com números inteiros nesse intervalo completo. De forma mais geral, as únicas operações válidas em um tipo de união são operações válidas em ambos os tipos que estão sendo unidos. O conceito de "união" de 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 em 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 de união, mas também podem ter outras operações válidas em comum).

Tipos existenciais

Os 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 número inteiro. Isto poderia ser implementado de diferentes maneiras; por exemplo:

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

Esses tipos são 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 de qual seja o tipo abstrato X. Isso dá flexibilidade para escolher tipos adequados para 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 verificador de tipos inferir a qual tipo existencial um determinado módulo pertence. No exemplo acima intT { a: int; f: (int → int); } também poderia ter o tipo ∃X { a: X; f: (int → int); }. A solução mais simples é anotar cada módulo com o tipo pretendido, por exemplo:

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

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

Digitação gradual

Em um sistema de tipos com digitação gradual , variáveis ​​podem receber um tipo em tempo de compilação (que é digitação estática) ou em tempo de execução (que é digitação dinâmica). [26] Isso permite que os desenvolvedores de software escolham qualquer tipo de paradigma conforme apropriado, dentro de uma única linguagem. [26] A digitação gradual usa um tipo especial denominado dinâmico para representar tipos estaticamente desconhecidos; a digitação gradual substitui a noção de igualdade de tipos 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. [27]

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

Muitos sistemas de tipos estáticos, 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 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 , o compilador pode inferir que e devem ser números – já que a adição só é definida para números. Assim, qualquer chamada para outro local do programa que especifique um tipo não numérico (como uma string ou lista) como argumento sinalizaria um erro. f(x, y)xyxyf

Constantes e expressões numéricas e de string no código podem, e muitas vezes implicam, digitar 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 tipo de sistema, a inferência é frequentemente 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 tipos é computável. A maioria dos compiladores Haskell permite o polimorfismo de classificação arbitrária como 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 recebam 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 digitação está naturalmente associado aos problemas de decisão de verificação de tipos , tipabilidade e habitação de tipos . [28]

  • Dado um tipo ambiental , um termo e um tipo , decida se o termo pode receber o tipo no tipo ambiente.
  • Dado um termo , decida se existe um tipo de ambiente e um tipo tal que o termo possa receber o tipo no tipo de ambiente .
  • Dado um tipo de ambiente e um type , decida se existe um termo ao qual possa ser atribuído o tipo no tipo de ambiente.

Sistema de tipo unificado

Algumas linguagens como C# ou Scala possuem um sistema de tipos unificado. [29] 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 , possuem um tipo raiz, mas também possuem tipos primitivos que não são objetos. [30] 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. Raku converte automaticamente tipos primitivos em objetos quando seus métodos são acessados. [31]

Compatibilidade: equivalência e subtipagem

Um verificador de tipo para uma linguagem de tipo estaticamente deve verificar se o tipo de qualquer expressão é consistente com o tipo esperado pelo contexto em que essa expressão aparece. Por exemplo, em uma instrução de atribuição no formato , 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 de 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 à questão de saber se são iguais (ou equivalentes ). Linguagens diferentes, entretanto, 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 tipos estruturais , nos quais quaisquer dois tipos que descrevem valores com a mesma estrutura são equivalentes, e sistemas de tipos nominativos , nos quais não há duas expressões de tipos sintaticamente distintas denotando 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: 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 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 computadores Burroughs ALGOL determinou o conteúdo de um local de memória por meio de seus bits de sinalização. Os bits de flag 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. Somente o MCP (Programa de Controle Mestre) poderia escrever nos bits do código do sinalizador.
  2. ^ Por exemplo, uma abstração com vazamento pode surgir durante o desenvolvimento, o que pode mostrar que é necessário mais desenvolvimento de tipo. —"A avaliação de um programa bem digitado sempre termina".—B. Nordström, K. Petersson e JM Smith [5] Uma mudança sistemática nas variáveis ​​para evitar a captura de uma variável livre pode introduzir erros , em uma linguagem de programação funcional onde as funções são cidadãs de primeira classe. [6] —Do artigo sobre cálculo lambda .

Referências

  1. ^ Pierce 2002, pág. 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ág. 1: “O propósito 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ág. 208.
  4. ^ ab Sethi, R. (1996). Linguagens de programação: Conceitos e construções (2ª ed.). Addison-Wesley. pág. 142. ISBN 978-0-201-59065-4. OCLC604732680  .
  5. ^ Nordstrom, B.; Petersson, K.; Smith, JM (2001). "Teoria dos Tipos de Martin-Löf". Estruturas Algébricas e Lógicas . Manual de Lógica em Ciência da Computação. Vol. 5. Imprensa da Universidade de Oxford. pág. 2.ISBN _ 978-0-19-154627-3.
  6. ^ Turner, DA (12 de junho de 2012). "Alguma história das linguagens de programação funcional" (PDF) . palestra convidada na TFP12, na St Andrews University . Veja a seção sobre Algol 60.
  7. ^ "... qualquer sistema de tipo sólido e decidível deve ser incompleto" —D. Rémy (2017). pág. 29, Rémy, Didier. "Tipo de sistemas para linguagens de programação" (PDF) . Arquivado do original (PDF) em 14 de novembro de 2017 . Recuperado em 26 de maio de 2013 .
  8. ^ Perfurar 2002.
  9. ^ abcSkeet, Jon (2019). C# em profundidade (4 ed.). Tripulação. ISBN 978-1617294532.
  10. ^ Miglani, Gaurav (2018). "Despacho de método dinâmico ou polimorfismo de tempo de execução em Java". Arquivado do original em 07/12/2020 . Recuperado em 28/03/2021 .
  11. ^ Wright, Andrew K. (1995). Digitação suave prática (PhD). Universidade do Arroz. hdl :1911/16900.
  12. ^ "dinâmico (referência C #)" . Biblioteca MSDN . Microsoft . Recuperado em 14 de janeiro de 2014 .
  13. ^ "std::any - Ferrugem" . doc.rust-lang.org . Recuperado em 07/07/2021 .
  14. ^ Meijer, Erik; DRAYTON, Peter. "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 .
  15. ^ Laucher, Amanda; Snively, Paul (2012). "Tipos vs testes". InfoQ.
  16. ^ Xi, Hongwei (1998). Tipos Dependentes em Programação Prática (PhD). Departamento de Ciências Matemáticas, Universidade Carnegie Mellon. 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. S2CID245490  .
  17. ^ Visual Basic é um exemplo de linguagem com segurança de tipo e memória.
  18. ^ "4.2.2 A variante estrita do ECMAScript" . Especificação de linguagem ECMAScript® 2020 (11ª ed.). ECMA. Junho de 2020. ECMA-262.
  19. ^ "Modo estrito - JavaScript" . MDN . Desenvolvedor.mozilla.org. 03/07/2013 . Recuperado em 17/07/2013 .
  20. ^ "Modo Estrito (JavaScript)" . MSDN . Microsoft . Recuperado em 17/07/2013 .
  21. ^ "Digitação estrita" . Manual do PHP: Referência da Linguagem: Funções .
  22. ^ ab Bracha, G. "Tipos conectáveis" (PDF) .
  23. ^ "Claro. Chama-se" digitação gradual ", e eu a qualificaria como moderna. ..." Existe uma linguagem que permite digitação estática e dinâmica? . fluxo de pilha. 2012.
  24. ^ abc Kopylov, Alexei (2003). "Interseção dependente: uma nova forma de definir registros na teoria dos tipos". 18º Simpósio IEEE sobre Lógica em Ciência da Computação . LICS 2003. Sociedade de Computação IEEE. pp. 86–95. CiteSeerX 10.1.1.89.4223 . doi :10.1109/LICS.2003.1210048. 
  25. ^ 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. S2CID1222153  .
  26. ^ ab Siek, Jeremy (24 de março de 2014). "O que é digitação gradual?".
  27. ^ Siek, Jeremy; Taha, Walid (setembro de 2006). Digitação Gradual para Linguagens Funcionais (PDF) . Esquema e Programação Funcional 2006 . Universidade de Chicago . pp. 81–92.
  28. ^ 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.
  29. ^ "8.2.4 Tipo de unificação do sistema" . Especificação da linguagem C# (5ª ed.). ECMA. Dezembro de 2017. ECMA-334.
  30. ^ "Tipos Nativos" . Documentação Perl 6 .
  31. ^ "Numéricos, § Boxe automático" . Documentação Perl 6 .

Leitura adicional

links externos

  • Mídia relacionada aos sistemas de tipos no Wikimedia Commons
  • Smith, Chris (2011). "O que saber antes de debater sistemas de tipos".
Retrieved from "https://en.wikipedia.org/w/index.php?title=Type_system&oldid=1209858998#Dynamic_type_checking_and_runtime_type_information"