Da Flexibilidade à Precisão ou Entendo os Sistemas de Tipo · clacerda

Neste artigo, exploramos um aspecto crucial da programação de computadores - os sistemas de tipo. Através da tradução anotada do primeiro parágrafo do trabalho seminal de Luca Cardelli, apresentarei a essência, e a importância fundamental dos tipos na programação de computadores.

O Propósito Fundamental dos Sistemas de Tipo

"The fundamental purpose of a type¹ system² is to prevent the occurrence of execution errors³ during the running of a program."

O propósito fundamental de um sistema de tipo¹² é prevenir a ocorrência de erros de execução³ durante o processamento de um programa."

Type/Tipo: Define um limite superior na quantidade de valores que uma variável pode assumir durante a execução de um programa. Por exemplo, uma variável do tipo Booleano só pode assumir dois valores: verdadeiro ou falso. Um inteiro de 1 byte só pode assumir os valores entre -128 to 127.
Type System/Sistema de Tipo: Refere-se ao conjunto de regras que uma linguagem de programação segue para verificar os tipos de suas variáveis e expressões. Este sistema ajuda a identificar e prevenir erros no código do programa.
Execution Errors/Erros de Execução: Problemas que ocorrem durante o functionamento de programa, podendo causar falhas ou comportamentos inesperados. O sistema de tipos visa prevenir tais erros.

O autor esclarece que a precisão desta afirmação depende do que constitui um erro de execução, algo é discutido em detalhes no artigo, depois prossegue:

"...the absence of execution errors is a nontrivial property. When such a property holds for all of the program runs that can be expressed within a programming language, we say that the language is type sound⁴"

A ausência de erros de execução é uma propriedade não trivial. Quando tal propriedade é mantida em todas as execuções possíveis de todos programas definidos dentro de uma linguagem de programação, dizemos que a linguagem possui tipo consistente.⁵

Type Sound: Refere-se a uma propriedade de linguagens de programação onde o sistema de tipos garante que nenhum erro de execução ocorrerá. Esta é uma característica desejável que indica a robustez e confiabilidade do sistema de tipos da linguagem.
Tipo Consistente: É importante destacar que essa é uma interpretação minha e não existe uma tradução estabelecida na literatura. Esta é uma tentativa de fornecer um termo em português que se aproxime do conceito original de "type sound". "Sound" também é usado para descrever algo que é tipo⁶ verdade. Por exemplo, um "sound judgment" refere-se a um julgamento que é baseado em razão e argumentos sólidos. A palavra "consistente" transmite a ideia de algo que é coerente e lógico, semelhante ao uso de "sound" em inglês.
Tipo: Em português, assim como "type" em inglês, a palavra "tipo" pode ser usada de forma bastante ampla e imprecisa. Frequentemente, é empregada em um contexto coloquial para indicar semelhança ou categoria de maneira vaga, como em expressões "tipo assim" ou "algo do tipo". No entanto, no contexto de linguagens de programação, nos referimos a um conceito específico e bem definido¹.

"It turns out that a fair amount of careful analysis is required to avoid false and embarrassing claims of type soundness for programming languages. As a consequence, the classification, description, and study of type systems has emerged as a formal discipline⁷."

Verifica-se que é necessária uma quantidade significativa de análise cuidadosa para evitar afirmações falsas e constrangedoras sobre a consistência de tipos em linguagens de programação. Como consequência, a classificação, descrição e estudo dos sistemas de tipos emergiram como uma disciplina formal.

Formal Discipline/Disciplina Formal: Uma disciplina formal envolve o uso matemática e análise rigorosos. O teorema da consistência por exemplo, oferece garantias matemáticas de que sistemas de tipos bem definidos em linguagens de programação podem prevenir efetivamente erros de execução. No entanto, entender completamente este teorema e suas implicações requer um estudo extenso e profundo.

Notas finais sobre Sistemas de Tipos

Ao finalizar nossa análise deste trabalho, é importante refletir sobre a classificação dos sistemas de tipos. Comumente, os sistemas de tipos são categorizados como "estáticos" ou "dinâmicos", "fortes" ou "fracos". No entanto, é crucial entender que essas classificações antes de prosseguir seus estudos em sistemas de tipos.

Tipos Fortes e Fracos: A distinção entre tipos fortes e fracos é frequentemente subjetiva. O que é considerado um sistema de tipo "forte" por um programador pode ser visto como "fraco" por outro, dependendo de sua familiaridade e conforto com o sistema. Essencialmente, um tipo "forte" muitas vezes se refere a um sistema que o desenvolvedor acredita ser robusto e confiável, enquanto um "fraco" pode indicar uma sensação de incerteza ou falta de segurança.
Tipos Estáticos e Dinâmicos: A diferença entre tipos estáticos e dinâmicos tem implicações mais concretas. Sistemas de tipos estáticos são aqueles em que a verificação de tipo ocorre em tempo de compilação, enquanto sistemas dinâmicos realizam essa verificação durante a execução do programa. Cada abordagem tem suas vantagens e desvantagens, e a escolha entre uma e outra muitas vezes depende das necessidades específicas do projeto e das preferências do desenvolvedor.

A escolha do termo "tipo consistente" em vez de "tipo seguro" é intencional para evitar confusões com o conceito de uma linguagem ser segura. Por exemplo, no livro "Why Rust":

If a language’s type system ensures that every program is well defined, we say that language is type safe.

Por essa definição JavaScript é uma linguagem de tipos seguros, mesmo sendo uma linguaguem não tipida. Para entender é preciso ler o artigo do Cardelli, no contexto de tipos, js é idêntico ao LISP discutido pelo autor.

Um abraço e bons estudos!