Tipo Perguntas frequentes do sistema

O autor do artigo, cuja tradução publicamos hoje, diz que este post e comentários serviram como fonte de inspiração para a redação. Segundo ele, os especialistas em TI têm conceitos errados sobre tipos, usam terminologia incorreta e, discutindo questões relacionadas a tipos, chegam a conclusões errôneas. Ele observa que não é defensor do sistema de tipos estáticos. A única coisa que o incomoda é o uso correto dos termos. Isso permite discussões construtivas. O autor diz que escreveu este material espontaneamente, mas espera que não haja erros nele. Se ele confundiu alguma coisa, ele pede que ele soubesse.



Vamos entender de uma vez por todas o que causa confusão quando se fala em sistemas de tipos.

Digitação dinâmica e falta de digitação

Algumas pessoas pensam que um sistema de tipos dinâmicos é o mesmo que um sistema de tipos não tipados. A falta de digitação significa que, em um determinado sistema de tipos, não faz sentido distinguir entre tipos. Não faz sentido distinguir tipos, mesmo que apenas um tipo esteja presente no sistema de tipos. Por exemplo:

• No assembler, o único tipo é uma sequência de bits.
• No cálculo lambda, o único tipo é função.

Alguém pode dizer isso nesta ocasião: "Mas que diferença faz - digitação dinâmica ou falta de digitação - também é uma pergunta para mim." Mas isso, de fato, é uma questão grande e importante. O fato é que, se você equiparar digitação dinâmica à falta de digitação, significa a adoção automática do fato de que um sistema de tipo dinâmico é o oposto de um sistema de tipo estático. Como resultado, dois campos opostos de programadores são formados - o campo de tipagem dinâmica e o campo de tipagem estática (e isso, como veremos na seção correspondente, está errado).

Os idiomas que não limitam o intervalo de valores das variáveis ​​são chamados de idiomas não tipados: eles não têm tipos ou, o que é a mesma coisa, eles têm apenas um tipo universal que contém todos os valores.
_{Type Systems, Luca Cardelli}

As linguagens de programação têm um recurso interessante que permite dividir aproximadamente o mundo deles em dois grupos:

• Linguagens sem tipo - programas simplesmente executados. Isso acontece rapidamente, sem tentar verificar a "uniformidade de formas".
• Linguagens digitadas - é feita uma tentativa de verificar a “uniformidade da forma” - durante a compilação ou durante a execução do programa.

_{“Sistemas de tipos para linguagens de programação”, Benjamin Pearce}

Digitação dinâmica e estática

Um sistema de tipo dinâmico é um sistema no qual os tipos são verificados dinamicamente (durante a execução do programa). Um sistema de tipo estático é um sistema no qual os tipos são verificados estaticamente (durante a compilação ou tradução de código).

Um desses sistemas é o oposto do outro? Não é não. Os dois tipos de sistemas podem ser usados ​​no mesmo idioma. De fato, a maioria dos sistemas de tipo estático também possui verificações de tipo dinâmico. Como exemplo, considere a validação das operações de entrada e saída (IO). Imagine que você precise ler os dados fornecidos por um usuário que deve inserir um número. Você verificará, durante a execução do programa, se o número é o resultado da análise da linha correspondente (como resultado da análise, uma exceção pode ser lançada ou algo como NaN será retornado). Quando você verifica os dados inseridos pelo usuário, descobrindo se eles podem ser considerados como um número - você executa uma verificação de tipo dinâmico.

Como resultado, podemos observar a ausência de confronto entre os tipos estático e dinâmico. Você pode usar, no mesmo idioma, esses e outros.

Além disso, deve-se notar que a verificação de tipo estático é um processo complexo. Às vezes, é muito difícil verificar estaticamente algumas partes de um programa. Como resultado, em vez de aplicar verificações de tipo estático, você pode recorrer a verificações dinâmicas.

É recomendável considerar um sistema de tipo estático como tipos que são verificados estaticamente. Um sistema de tipos dinâmicos é como tipos verificados dinamicamente.

Usar tipos estáticos significa conhecer tipos em tempo de compilação?

A pergunta colocada no título desta seção pode ser respondida em negativo. Se você abrir o código-fonte de qualquer analisador (incluindo o analisador JavaScript), poderá ver que o analisador conhece os tipos de valores durante a análise (isso faz parte do processo de compilação).

 let x = "test"; 

Acontece que o analisador sabe que "test" é uma sequência. Isso faz do JavaScript uma linguagem estática de tipo? Não, não é.

Digitação gradual

Um sistema de tipo gradual é um sistema de tipo estático que permite ignorar as verificações de tipo de algumas partes de um programa. Por exemplo, no TypeScript, isso é implementado usando any ou @ts-ignore .

Por um lado, isso torna o sistema de tipos menos seguro. Por outro lado, um sistema de tipos com digitação gradual permite adicionar gradualmente descrições de tipos a idiomas com digitação dinâmica.

Sistemas de tipo confiáveis ​​e não confiáveis

Se você usar um sistema de tipos confiável (sistema de tipos de som), o programa, durante a verificação de tipo, não será "aprovado" se houver erros relacionados aos tipos neste programa. O uso de um sistema de tipo não sólido leva à possibilidade de erros de tipo no programa. É verdade que você não deve entrar em pânico depois de descobrir. Na prática, isso pode não afetá-lo. Confiabilidade ou solidez são propriedades matemáticas de um algoritmo de verificação de tipo que precisa de prova. Muitos compiladores existentes (internamente, sistemas de verificação de tipo) não são confiáveis.

Se você deseja trabalhar com sistemas de tipos confiáveis, dê uma olhada nas linguagens de programação da família ML, que usam o sistema do tipo Hindley-Milner.

Além disso, deve-se entender que um sistema do tipo confiável não ignora o programa errado (não fornece resultados de testes falsos positivos, considerando que os programas errados estão corretos), mas pode não faltar ao programa correto (pode dar resultados falsos negativos).

Um sistema de tipos que nunca rejeita o programa certo é chamado de completo.

Acontece que um sistema de tipos é confiável e completo? Até onde eu sei, esses sistemas de tipos não existem. Não tenho certeza disso até o fim, mas parece-me que a existência de tais sistemas de tipos, se baseada no teorema da incompletude de Gödel, é fundamentalmente impossível (embora eu possa estar errado).

Digitação fraca e forte

Acho inapropriado usar os termos "digitação fraca" e "digitação forte". Esses termos são ambíguos, seu uso pode dar mais confusão do que clareza. Deixe-me fazer algumas citações.

Esses idiomas podem ser chamados, figurativamente falando, idiomas com verificação de tipo fraco (ou idiomas com tipos fracos, como geralmente são chamados em várias publicações). O uso da verificação de tipo fraco no idioma significa que algumas operações inseguras são detectadas estaticamente e outras não. A "fraqueza" das verificações de tipo nos idiomas desta classe varia muito.
_{Type Systems, Luca Cardelli}

Provavelmente, a maneira mais comum de classificar sistemas de tipos é dividi-los em sistemas com digitação "fraca" e "forte". Isso só pode ser lamentado, pois essas palavras não têm praticamente nenhum significado em si mesmas. É possível, até certo ponto, comparar dois idiomas que possuem sistemas de tipos muito semelhantes e selecionar um deles como tendo um sistema de tipos mais forte que o segundo. Em outros casos, os termos "digitação forte" e "digitação fraca" são completamente sem sentido.
_{"Coisas a saber antes de discutir os sistemas de tipos", Steve Klabnik}

Os termos "digitação forte" e "digitação fraca" são extremamente ambíguos. Aqui estão alguns exemplos de seu uso:

• Às vezes, “digitação forte” é entendida como “digitação estática”. Não é difícil fazer essa "substituição", mas é melhor, falando em digitação estática, simplesmente chamá-la de "estática". O fato é que a maioria dos programadores entende claramente esse termo.
• Às vezes, quando dizem "digitação forte", significam "a ausência de uma conversão implícita de tipo". Por exemplo, em JavaScript, você pode usar expressões como "a" - 1 . Isso pode ser chamado de modelo de "digitação fraca". Mas quase todas as linguagens oferecem ao programador algumas oportunidades para conversão implícita de tipos, por exemplo, suportando a conversão automática de números inteiros em números de ponto flutuante em expressões como 1 - 1.1 . Na prática, a maioria dos profissionais que usam o termo "digitação forte" dessa maneira faz distinção entre conversões do tipo "aceitável" e "inaceitável". Mas não existe um limite geralmente aceito entre essas conversões de tipo. A "aceitabilidade" e "inaceitável" das transformações é uma avaliação subjetiva, dependendo da opinião de uma pessoa em particular.
• Às vezes, idiomas com "digitação forte" são chamados de idiomas nos quais é impossível contornar as regras do sistema de tipos que eles possuem.
• Às vezes, "digitação forte" significa ter um sistema de tipos que permite trabalhar com segurança na memória. A linguagem C é um exemplo notável de uma linguagem que não é segura na memória. Por exemplo, se xs é uma matriz de quatro números, C aprovará um código que usa construções como xs[5] ou xs[1000] sem problemas. Eles permitirão que você acesse a memória localizada após os endereços alocados para armazenar o conteúdo da matriz xs .

_{Os tipos, Gary Bernard}

As linguagens estáticas digitadas precisam de declarações de tipo?

Linguagens de tipo estático nem sempre precisam de declarações de tipo. Às vezes, um sistema de tipos pode inferir tipos (fazendo suposições com base na estrutura do código). Aqui está um exemplo (TypeScript):

 const x = "test"; 

O sistema de tipos sabe que "test" é uma string (esse conhecimento é baseado nas regras de análise de código). O sistema de tipos também sabe que x é uma constante, ou seja, o valor de x não pode ser reatribuído. Como resultado, pode-se concluir que x é do tipo string.
Aqui está outro exemplo (Flow):

 const add = (x, y) => x / y //            ^        [1]   . add(1, "2") 

O sistema de verificação de tipo vê que chamamos a função add , passando um número e uma string. Isso analisa a declaração da função. O sistema de verificação de tipo sabe que, para executar a operação de divisão, os números devem estar à direita e esquerda do operador correspondente. Um dos operandos envolvidos na operação de divisão não é um número. Como resultado, somos informados sobre o erro.

Não há declarações de tipo aqui, mas isso não impede uma verificação de tipo estático do programa acima. Se você encontrar situações semelhantes no mundo real, mais cedo ou mais tarde precisará declarar alguns tipos. O sistema de tipos não pode deduzir absolutamente todos os tipos. Mas você precisa entender que um idioma pode ser chamado de "estático" não porque usa declarações de tipo, mas porque os tipos são verificados antes do início do programa.

O TypeScript é uma linguagem insegura porque o código escrito nele é compilado no código JavaScript?

TypeScript é uma linguagem doentia. Portanto, o código escrito nele pode se transformar em aplicativos não seguros. Mas isso não tem nada a ver com o que compila.

A maioria dos compiladores de desktop converte programas em algo que se parece com a linguagem assembly. E assembler é uma linguagem ainda menos segura que JS.

Aqui, se você voltar à ideia de que o TS é inseguro devido à compilação em JS, você pode ter o seguinte pensamento: “O código compilado é executado no navegador, o JS é uma linguagem insegura e pode substituir null ao local em que a linha é esperada " O pensamento é sensato. Mas isso, novamente, não dá uma razão para chamar o TS de uma linguagem insegura. Para que o TS garanta segurança dentro do aplicativo, é necessário colocar os "mecanismos de defesa" nos locais em que o código do TS interage com o mundo externo. Ou seja, por exemplo, é necessário verificar a correção dos dados que entram no programa através dos mecanismos de entrada e saída. Digamos que isso possa estar verificando o que o usuário digita, verificando respostas do servidor, verificando dados lidos no armazenamento do navegador e assim por diante.

Por exemplo, o papel desses "mecanismos de defesa" no Elm é desempenhado por " portos ". No TS, você pode usar algo como io-ts para isso.

O correspondente “mecanismo de proteção” cria uma ponte entre os sistemas do tipo estático e dinâmico.

Aqui está um exemplo simplificado:

 const makeSureIsNumber = (x: any) => {  const result = parseFloat(x);  if (isNaN(result)) {    throw Error("Not a number");  }  return result; } const read = (input: any) => {  try {    const n = makeSureIsNumber(input);    //     n, ,      //              // makeSureIsNumber "" , n    } catch (e) { } } 

É verdade que os tipos são necessários apenas para compiladores?

Os tipos são apenas o hack necessário para dar dicas ao compilador.
_{Waut Mertens}

Os tipos são necessários apenas pelos compiladores? Esta é uma questão filosófica. Tipos são necessários para pessoas, não para carros. Compiladores precisam de tipos porque são programas criados por pessoas.

O fenômeno dos tipos existe por causa das pessoas. Os tipos não existem até que uma pessoa perceba algo na forma de um "tipo de dados". A mente humana divide diferentes entidades em diferentes categorias. Tipos não fazem sentido sem um observador.

Vamos organizar um experimento mental. Pense no jogo da vida. Você tem uma grade bidimensional que consiste em células quadradas. Cada uma das células pode estar em dois estados possíveis. Pode estar "vivo" ou "morto". Cada célula pode interagir com seus oito vizinhos. São células que o limitam verticalmente, horizontalmente ou diagonalmente. No processo de localização do próximo estado do sistema, as seguintes regras se aplicam:

• Uma célula “viva” com menos de dois vizinhos “vivos” “morre”, como em uma baixa densidade populacional.
• Uma célula “viva” com dois ou três vizinhos “vivos” sobrevive e cai na próxima geração.
• Uma célula "viva", com mais de três vizinhos "vivos", "morre", como na superpopulação.
• A célula “morta”, que possui exatamente três vizinhos “vivos”, torna-se “viva”, como na reprodução da população.

Externamente, parece um campo dividido em células quadradas, que são constantemente "ativadas" e "desativadas". Aqui você pode dar uma olhada nisso.

Se você observar a Vida por algum tempo, estruturas estáveis ​​como "planador" podem aparecer no campo.


Planador

Viu ele? Um planador se move pela tela. Certo? Agora vamos desacelerar um pouco. Este planador realmente existe? Estes são apenas quadrados individuais que aparecem e desaparecem. Mas nosso cérebro pode perceber essa estrutura como algo objetivamente existente.

Além disso, podemos dizer que o “planador” existe porque os quadrados não são independentes (eles dependem dos vizinhos) e, mesmo que o próprio “planador” não exista, existe um “planador” na forma idéias platônicas.

Sumário

Considere qualquer programa escrito em uma linguagem de programação digitada. Podemos observar os tipos. Certo? Mas o programa é compilado em códigos de máquina. Nesses códigos, o mesmo é expresso no programa original (embora seja difícil para uma pessoa ler representações de programas de máquinas). Do ponto de vista do computador, não há tipos. Ele vê apenas a sequência de bits - conjuntos de zeros e uns (células "mortas" e "vivas"). Existem tipos para pessoas, não para carros.

Caros leitores! Que tipo de sistema você considera ideal para o desenvolvimento da web?