Categorização dos sistemas de tipos (forte / fraco, dinâmico / estático)

23

Em resumo: como os sistemas de tipos são categorizados em contextos acadêmicos; particularmente, onde posso encontrar fontes respeitáveis ​​que tornem claras as distinções entre diferentes tipos de sistemas de tipos?

Em certo sentido, a dificuldade com esta pergunta não é que não consigo encontrar uma resposta, mas sim que posso encontrar muitas, e nenhuma se destaca como correta. O pano de fundo é que estou tentando melhorar um artigo no wiki da Haskell sobre digitação , que atualmente afirma as seguintes distinções:

  • Sem digitação: o idioma não tem noção de tipos ou de uma perspectiva digitada: existe exatamente um tipo no idioma. A linguagem Assembly possui apenas o tipo 'padrão de bits', Rexx e Tk apenas o tipo 'texto', o MatLab principal possui apenas o tipo 'matriz de valor complexo'.
  • Digitação fraca: existem apenas alguns tipos distintos e talvez sinônimos de tipo para vários tipos. Por exemplo, C usa números inteiros para booleanos, inteiros, caracteres, conjuntos de bits e enumerações.
  • Digitação forte: conjunto de tipos refinados, como Ada, idiomas wirthianos (Pascal, Modula-2), Eiffel

Isso é totalmente contrário à minha percepção pessoal, que era mais parecida com:

  • Digitação fraca: os objetos têm tipos, mas são implicitamente convertidos em outros tipos quando o contexto exige. Por exemplo, Perl, PHP e JavaScript são todos os idiomas em que "1"podem ser usados ​​em mais ou menos qualquer contexto 1possível.
  • Digitação forte: os objetos têm tipos e não há conversões implícitas (embora a sobrecarga possa ser usada para simulá-las), portanto, usar um objeto no contexto errado é um erro. No Python, a indexação de uma matriz com uma string ou float lança uma exceção TypeError; em Haskell, ele falhará no momento da compilação.

Pedi opiniões sobre isso a outras pessoas mais experientes no campo do que eu, e uma delas deu essa caracterização:

  • Digitação fraca: a execução de operações inválidas nos dados não é controlada ou rejeitada, mas apenas produz resultados inválidos / arbitrários.
  • Digitação forte: operações com dados são permitidas apenas se os dados forem compatíveis com a operação.

Pelo que entendi, a primeira e a última caracterizações chamariam C de tipo fraco, a segunda chamaria de tipo forte. O primeiro e o segundo chamariam Perl e PHP de tipo fraco, o terceiro os chamaria de tipo forte. Todos os três descreveriam o Python como fortemente tipado.

Eu acho que a maioria das pessoas me diria "bem, não há consenso, não há significado aceito dos termos". Se essas pessoas estiverem erradas, eu ficaria feliz em ouvir sobre isso, mas se elas estiverem certas, como os pesquisadores de CS descrevem e comparam sistemas de tipos? Que terminologia posso usar que é menos problemática?

Como questão relacionada, considero que a distinção dinâmica / estática é frequentemente dada em termos de "tempo de compilação" e "tempo de execução", o que considero insatisfatório, dado que a compilação ou não de um idioma não é tanto uma propriedade desse idioma como suas implementações. Eu sinto que deveria haver uma descrição puramente semântica da tipagem dinâmica versus estática; algo como "uma linguagem estática é aquela em que toda subexpressão pode ser digitada". Eu apreciaria quaisquer pensamentos, particularmente referências, que tragam clareza a essa noção.

Ben Millwood
fonte
6
Acho que você já tem sua resposta: não há uma definição aceita de digitação fraca e forte.
svick
Eu não acho isso difícil de acreditar, mas faço a pergunta na esperança de que exista uma sobre a qual ainda não ouvi :) ou pelo menos uma definição mais autoritária do que o que um cara que editou um wiki considera ser o caso .
precisa
3
Para mais discussões sobre isso, consulte esta pergunta relacionada no SO .
svick
1
Para reforçar o argumento de svick, não é possível encontrar uma referência de autoridade em algo que não é aceito. Qualquer coisa que afirme ser autoritária estaria simplesmente errada (já que qualquer número de contra-exemplos poderia ser fornecido).
EdA-qa mort-ora-y
Bem, há uma diferença entre alguém escrevendo um artigo que diz "aqui está a única definição verdadeira com a qual todos concordam" e alguém escrevendo um artigo que diz "aqui estão as definições que vou usar neste artigo, embora eu saiba que existem outras". Até o último seria melhor do que eu sei até agora. Acho que você pode estar certo, nesse caso, o que as pessoas têm a dizer sobre os diferentes tipos de sistema de tipos? A distinção dinâmica / estática é, pelo menos, concreta?
precisa

Respostas:

18

Historicamente, o termo "linguagem de programação fortemente tipada" entrou em uso nos anos 70 em reação às linguagens de programação amplamente utilizadas existentes, a maioria das quais com orifícios de tipo. Alguns exemplos:

  • No Fortran, havia coisas chamadas áreas de armazenamento "COMUM", que podiam ser compartilhadas entre módulos, mas não havia verificações para ver se cada módulo estava declarando o conteúdo do armazenamento COMUM com os mesmos tipos. Portanto, um módulo poderia declarar que um bloco de armazenamento COMMON específico tinha um número inteiro e outro um número de ponto flutuante, e os dados seriam corrompidos como resultado. Fortran também tinha instruções "EQUIVALENCE", nas quais o mesmo armazenamento poderia ser declarado como contendo dois objetos diferentes de tipos diferentes.

  • No Algol 60, o tipo de parâmetros do procedimento foi declarado como apenas "procedimento", sem especificar os tipos dos parâmetros do procedimento. Portanto, pode-se supor que um parâmetro de procedimento seja um procedimento de aceitação de número inteiro, mas passar um procedimento de aceitação real como argumento. Isso resultaria no mesmo tipo de corrupção que as declarações COMMON e EQUIVALENCE. (No entanto, o Algol 60 eliminou os problemas mais antigos.)

  • Em Pascal, foram adicionados "registros variantes", que eram quase exatamente como as antigas declarações de EQUIVALENCE.

  • Em C, foram adicionados "tipos de conversão", pelos quais qualquer tipo de dados pode ser reinterpretado como dados de um tipo diferente. Este foi um buraco tipo deliberado, destinado a programadores que supostamente sabem o que estão fazendo.

As linguagens fortemente tipadas projetadas nos anos 70 foram destinadas a eliminar todos esses buracos de tipo. Se você se aprofundar no que isso significa, significa essencialmente que as representações de dados estão protegidas. Não é possível visualizar o objeto de dados de um tipo como um objeto de outro tipo que possua o mesmo padrão de bits que sua representação interna. Os teóricos começaram a usar o termo "independência de representação" para caracterizar essa propriedade, em vez da vaga idéia de "digitação forte".

Observe que linguagens digitadas dinamicamente como Lisp, que executam a verificação completa do tipo em tempo de execução, são "fortemente tipadas" no sentido de proteger representações. Ao mesmo tempo, linguagens de tipo estaticamente perderiam a independência de representação, a menos que fizessem verificação de limites de matriz. Portanto, eles não são "fortemente tipificados" no sentido estrito do termo. Devido a essas conseqüências anômalas, o termo "fortemente tipado" caiu em desuso após os anos 70. Quando o Departamento de Defesa dos EUA desenvolveu requisitos rigorosos para o design do Ada, eles incluíram o requisito de que o idioma fosse "fortemente tipado". (Parece que naquela época se acreditava que a ideia de "fortemente tipado" era auto-evidente. Nenhuma definição foi oferecida. ) Todas as propostas de idiomas enviadas em resposta alegaram ter "tipificação forte". Quando Dijkstra analisou todas as propostas de linguagem, ele descobriu que nenhuma delas era fortemente tipada e, de fato, nem estava claro o que o termo significava. Veja o relatórioEWD663 . No entanto, vejo que o termo está voltando a ser usado agora, através de uma geração mais jovem de pesquisadores que não conhece a história quadriculada do termo.

O termo "digitado estaticamente" significa que toda a verificação de tipo é feita estaticamente e nenhum erro de tipo ocorrerá no tempo de execução. Se o idioma também for fortemente digitado, isso significa que realmente não há erros de tipo durante a execução. Se, por outro lado, houver furos de tipo no sistema de tipos, a ausência de erros de tipo em tempo de execução não significa nada. Os resultados podem estar completamente corrompidos.

O novo debate sobre "digitação forte versus fraca" parece ser sobre se certas conversões de tipo devem ser permitidas. Permitir uma string em que um número inteiro é necessário é "digitação fraca", de acordo com essas pessoas. Há algum sentido nisso, porque a tentativa de converter uma string em um número inteiro pode falhar, se a string não representar um número inteiro. No entanto, converter um número inteiro em uma sequência não tem esse problema. Isso seria um exemplo de "digitação fraca" de acordo com essas pessoas? Eu não faço ideia. Percebo que as discussões da Wikipedia sobre "digitação fraca" não citam nenhuma publicação arbitrada. Não acredito que seja uma ideia coerente.

Nota adicionada : o ponto básico é que o termo "digitação forte" não foi utilizado como termo técnico com uma definição rigorosa. Era mais como alguns designers de linguagem achavam: "nosso sistema de tipos é forte; captura todos os erros de tipo; não possui furos de tipo" e, portanto, quando eles publicaram seu design de linguagem, alegaram que era "fortemente tipado" . Era uma palavra da moda que parecia boa e as pessoas começaram a usá-la. O artigo de Cardelli-Wegner foi o primeiro que eu vi onde algumas análises foram fornecidas sobre o que isso significa. Meu post aqui deve ser pensado como uma elaboração de sua posição.

Uday Reddy
fonte
Você pode dar algumas referências para o desenvolvimento histórico? "a ausência de erros do tipo tempo de execução não significa nada" - você quer dizer tempo de compilação aqui?
Raphael
Aqui está um artigo sobre Euclides que apareceu no Google Scholar. Lembro-me de ver vários artigos nos anos 70, onde se dizia que os idiomas eram fortemente tipificados. Geralmente era pensado como um discurso de vendas.
Uday Reddy
1
@Raphael. Eu quis dizer "erros de tipo de tempo de execução". Para chegar ao tempo de execução, o programa precisaria passar pelo verificador de tipo estático em primeiro lugar. O ponto é que uma linguagem fortemente tipada, por exemplo, Java, fornecerá erros de tipo em tempo de execução quando não puder verificá-los em tempo de compilação. Uma linguagem de furo de tipo, por exemplo, C, permitirá que o tempo de execução produza lixo em vez de dar erros.
precisa
1
@benmachine. Veja a seção "verificação de tipo" no artigo de Euclides que citei. Eu acho que o ponto principal é que "fortemente digitado" é uma palavra da moda. Não é uma noção técnica. Na melhor das hipóteses, o conteúdo técnico significa que não há furos de tipo.
precisa
1
Em uma implementação moderna típica em que dois tipos inteiros diferentes têm a mesma representação (por exemplo, ambos inte longsendo 32 bits ou ambos longe long longsendo 64), um programa que usa um ponteiro para um desses tipos para gravar algum armazenamento e usa um ponteiro do outro tipo lê-lo, geralmente não aciona um erro detectável em tempo de execução, mas pode funcionar mal arbitrariamente de outras maneiras arbitrárias.O C moderno perde, assim, o presente de segurança de tipo de outros idiomas, sem obter nenhuma semântica que as implementações de qualidade da linguagem de Ritchie tiveram. oferecido anteriormente em troca #
308
7

O artigo que Uday Reddy encontrou em sua resposta, Sobre tipos de compreensão, abstração de dados e polimorfismo (1985), fornece as seguintes respostas:

Dizem que as linguagens de programação nas quais o tipo de cada expressão pode ser determinada pela análise estática do programa são estaticamente tipadas. A digitação estática é uma propriedade útil, mas o requisito de que todas as variáveis ​​e expressões sejam vinculadas a um tipo no tempo de compilação às vezes é muito restritivo. Pode ser substituído pelo requisito mais fraco de que todas as expressões são garantidas como consistentes com o tipo, embora o próprio tipo possa ser estaticamente desconhecido; Isso geralmente pode ser feito introduzindo algumas verificações de tipo em tempo de execução. Os idiomas em que todas as expressões são consistentes com o tipo são chamados de idiomas fortemente tipados. Se um idioma for fortemente digitado, seu compilador pode garantir que os programas que ele aceita serão executados sem erros de tipo. Em geral, devemos nos esforçar para digitar com firmeza e adotar a digitação estática sempre que possível.

máquinas automáticas
fonte
publicado como wiki da comunidade, pois não mereço o crédito por encontrar isso.
precisa
A questão que tenho aqui está relacionada ao primeiro comentário de svick. Embora seja bom que você tenha encontrado uma definição de digitação forte, essa certamente não é uma definição comumente aceita.
edA-qa mort-ora-y
@ edA-qamort-ora-y: com que base você diz isso? Você tem algo melhor do que evidências anedóticas sobre o que é e o que não é comumente aceito? Alguma citação? (Entendo que você pode ter um ponto válido, mesmo que não tenha, mas ainda acho que o exposto responde à minha pergunta; mesmo que não haja consenso, é bom saber pelo menos uma das respostas acadêmicas sérias).
precisa
1
Realmente não posso provar a ausência de uma definição acordada, posso? Não é logicamente possível. No entanto, os artigos da Wikipedia sobre tipagem forte fornecem muitas evidências e referências para desacordo e contradição. en.wikipedia.org/wiki/Strong_typing
edA-qa mort-ora-y
@ edA-qamort-ora-y: As citações da Wikipedia não são tão úteis: algumas não são acadêmicas, outras são citadas por outras razões que não a definição dos termos. O documento Typeful Programming parece promissor, mas apenas se refere brevemente às definições; talvez valha a pena editar a minha resposta de qualquer maneira. Com relação à prova de ausência, acho que evidências de controvérsia / desacordo entre as pessoas que sabem do que estão falando são suficientes para mim (o que, de fato, o trabalho do Typeful Programming pode me dar).
precisa
6

Respostas autorizadas podem ser encontradas no artigo da pesquisa de Cardelli e Wegner: Sobre a compreensão de tipos, abstração de dados e polimorfismo .

Lembre-se de que, embora "digitação forte" tenha um significado aceito, "digitação fraca" não. Qualquer falha na digitação forte pode ser considerada fraca e as pessoas podem diferir sobre que tipo de falha é aceitável e o que não é.

Uday Reddy
fonte
Excelente, era exatamente isso que eu queria. O trabalho exige um pouco de leitura, então acho que deveria haver uma resposta que resuma os pontos mais importantes. Devo editá-los em sua resposta ou postar minha própria resposta do wiki da comunidade? De qualquer maneira, eu vou dar-lhe mais alguns dias no caso de alguém tem qualquer entrada, em seguida, aceitar o que resta :)
Ben Millwood
@benmachine. Vale a pena ler o artigo completo, mas as questões conceituais de alto nível são abordadas apenas nas duas primeiras seções.
precisa
4
Ainda acho que deve ser resumido nesta página. O link pode expirar mais tarde.
precisa
@benmachine. Você pode publicar um resumo como sua própria resposta à sua pergunta.
precisa