Type-Driven Development para programar de forma segura usando tipos

• Los tipos son contratos estrictos que las funciones y los datos deben cumplir
• Un tipo es un conjunto al que pueden pertenecer ciertos valores
• Los tipos pueden transformarse mediante funciones, y con ello su rango puede cambiar
  • Función inyectiva: transformar de un tipo con rango pequeño a uno con rango grande
  • Función sobreyectiva: transformar de un tipo con rango grande a uno con rango pequeño
  • Función biyectiva: correspondencia uno a uno
• Es posible representar con tipos la entrada y la salida de una lógica
  • Esto significa que es posible abstraer la lógica mediante tipos
  • Se pueden representar la entrada y la salida con tipos, y a partir de ello diseñar la lógica
• Es posible asignar nombres a tipos de datos básicos para distinguirlos como tipos diferentes
• Al aprovechar el sistema de tipos, se pueden resolver varios problemas
  • Generalización usando genéricos
  • Restricción de rango usando tipos fantasma
  • Restricción de comportamiento usando tipos unión (o tipos suma)
  • Manejo de TODO usando tipos mínimos
  • Implementación de máquinas de estado finito usando tipos
  • Validación usando tipos dependientes
• El desarrollo guiado por tipos es una metodología en la que primero se definen los tipos y a partir de ellos se escribe el código
• El desarrollo guiado por tipos puede aplicarse en cualquier parte si se desea, y comienza definiendo como tipos los resultados de cada procedimiento
• Al analizar requisitos, conviene intentar abstraerlos con tipos
• Aunque se trate del mismo tipo de dato básico, si el significado es distinto, es mejor definirlo como un tipo diferente para distinguirlo
• Si ya analizaste los requisitos y pensaste en los tipos, intenta abstraer la lógica con tipos
  • Se puede abstraer con una idea como (String) -> List<Token>
• El desarrollo guiado por tipos combina bien con el desarrollo guiado por pruebas
  • En el sentido de que se definen de antemano las entradas y los resultados de salida y luego se escribe el código, el desarrollo guiado por tipos y el desarrollo guiado por pruebas son similares
  • Si el desarrollo guiado por tipos puede verificar anticipadamente la seguridad en tiempo de compilación usando el sistema de tipos, el desarrollo guiado por pruebas puede detectar mediante código de prueba errores o casos excepcionales que no pueden capturarse solo con tipos
• Desde la perspectiva del diseñador, aprovechar el sistema de tipos equivale a crear reglas de código para otros desarrolladores
• Sin embargo, si se define cada tipo de manera demasiado detallada y terminan siendo demasiados tipos, o si sus definiciones se vuelven complejas, puede hacerse más difícil escribir código o reducirse la legibilidad; por eso es importante mantener siempre un equilibrio adecuado

[chabulhwi]

> Una función inyectiva se refiere al caso en que el conjunto de valores transformados no coincide entre el codominio y la imagen. Expresado de forma un poco más simple, significa convertir de un tipo con un rango pequeño a un tipo con un rango grande.

Una función inyectiva se refiere a una función en la que las imágenes de cualesquiera dos variables distintas también son distintas. Es decir, para todos los elementos a y b que pertenecen al dominio X de una función inyectiva f, si a ≠ b, entonces f(a) ≠ f(b). En las matemáticas de secundaria en Corea, lo que se llama una "función uno a uno" es una función inyectiva.

[kciter1]

Muchas gracias por la explicación tan detallada. :) Yo lo había entendido mal. De hecho, es un punto que ya me habían señalado varias veces, así que voy a estudiar un poco más y reorganizar el contenido.