Type-Driven Development para uma codificação segura usando tipos

• Tipos são contratos rígidos que funções e dados devem cumprir
• Tipos são conjuntos aos quais determinados valores podem pertencer
• Tipos podem ser transformados por meio de funções, e com isso seu domínio pode ser alterado
  • Função injetora - transformar de um tipo de domínio menor para um tipo maior
  • Função sobrejetora - transformar de um tipo de domínio maior para um tipo menor
  • Função bijetora - correspondência um a um
• É possível representar as entradas e saídas da lógica com tipos
  • Isso significa que é possível abstrair a lógica por meio de tipos
  • É possível representar entradas e saídas com tipos e, a partir disso, projetar a lógica
• É possível dar nomes aos tipos de dados básicos para diferenciá-los como outros tipos
• Ao utilizar o sistema de tipos, é possível resolver vários problemas
  • Generalização usando genéricos
  • Restrição de domínio usando phantom types
  • Restrição de comportamento usando union types (ou sum types)
  • Tratamento de TODO usando tipos mínimos
  • Implementação de máquinas de estado finito usando tipos
  • Validação usando tipos dependentes
• Type-driven development é uma metodologia em que os tipos são definidos primeiro e o código é escrito a partir deles
• Type-driven development pode ser aplicado em qualquer lugar, se desejado, começando pela definição em tipos do resultado de cada procedimento
• Ao analisar requisitos, tente abstraí-los em tipos
• Mesmo que o tipo básico de dado seja o mesmo, se o significado for diferente, é melhor defini-lo como outro tipo para distingui-lo
• Depois de analisar os requisitos e pensar nos tipos, tente abstrair a lógica em tipos
  • É possível abstrair com algo como (String) -> List<Token>
• Type-driven development combina bem com test-driven development
  • Nesse ponto, type-driven development e test-driven development são semelhantes, pois ambos definem previamente entradas e resultados de saída antes de escrever o código
  • Se type-driven development pode verificar a estabilidade antecipadamente em tempo de compilação usando o sistema de tipos, test-driven development pode capturar com testes erros e casos excepcionais que não podem ser detectados apenas com tipos
• Do ponto de vista de quem projeta, usar o sistema de tipos equivale a criar regras de código para outros desenvolvedores
• No entanto, se cada tipo for definido manualmente e a quantidade de tipos aumentar demais, ou se as definições ficarem muito complexas, isso pode acabar dificultando a escrita do código ou prejudicando a legibilidade; por isso, é importante sempre manter um equilíbrio adequado

[chabulhwi]

> Uma função injetiva é o caso em que o conjunto de valores transformados não coincide entre o contradomínio e a imagem. Em termos um pouco mais simples, isso significa converter de um tipo com escopo menor para um tipo com escopo maior.

Uma função injetiva é uma função em que as imagens de quaisquer duas variáveis distintas são diferentes. Ou seja, para todos os elementos a e b pertencentes ao domínio X de uma função injetiva f, se a ≠ b, então f(a) ≠ f(b). O que no ensino médio coreano se chama de "função um para um" é uma função injetiva.

[kciter1]

Obrigado pela explicação detalhada. :) Eu tinha entendido errado. Como, inclusive, esse já é um ponto que me apontaram algumas vezes, vou estudar um pouco mais e reorganizar o conteúdo.