¿Cómo se demuestra un tipo? — El sistema de tipos de TypeScript y la correspondencia Curry–Howard

Resumen:

• Presenta una perspectiva que interpreta el sistema de tipos de TypeScript no como un simple verificador estático de tipos, sino como un sistema de prueba de la lógica.
• Explica conceptualmente por qué es posible la inferencia de tipos a partir de la correspondencia Curry–Howard (Type = Proposition, Program = Proof).
• Describe funciones de TypeScript como tipos de función, genéricos, tipos condicionales y estrechamiento de tipos, relacionándolas con implicación lógica, cuantificación universal y análisis de casos.
• Interpreta el proceso de verificación de tipos no como una aplicación de reglas, sino como un proceso de validación de relaciones entre proposiciones.
• Se enfoca en el trasfondo de diseño y la estructura matemática del sistema de tipos de TypeScript, más que en los detalles de implementación.

Resumen detallado:

1. Contexto: ¿por qué es posible la inferencia de tipos?
   En los lenguajes de tipos estáticos, la inferencia de tipos suele explicarse como un problema de implementación del tipo “¿cómo hace el compilador para hacer coincidir los tipos?”.
   Este artículo da un paso atrás y se pregunta por la razón fundamental por la que la inferencia de tipos es posible desde el origen.
   Como respuesta, propone una perspectiva que ve el sistema de tipos como un sistema de prueba de la lógica.

2. Base teórica: correspondencia Curry–Howard
   Según la correspondencia Curry–Howard, un tipo (Type) corresponde a una proposición (Proposition), y un programa (Program) corresponde a la prueba (Proof) de esa proposición.
   Desde esta perspectiva, la verificación de tipos se interpreta como el proceso de comprobar si un programa satisface una proposición determinada.

3. Correspondencia entre funciones de TypeScript y estructuras lógicas
   El texto conecta las principales funciones de TypeScript de la siguiente manera:

• tipos de función → implicación lógica (Implication)
• genéricos → cuantificación universal (Universal Quantification)
• tipos condicionales / estrechamiento de tipos → análisis de casos (Case Analysis)
  A través de esto, explica por qué ciertas expresiones de tipos resultan naturales,
  y por qué algunos tipos son estructuralmente difíciles de expresar.

4. Límites del sistema de tipos y decisiones de diseño
   Desde esta perspectiva, las restricciones y límites de TypeScript se entienden no como “falta de funcionalidades”, sino como decisiones de diseño para mantener la coherencia lógica.
   El texto se enfoca menos en técnicas o trucos prácticos y más en explicar sobre qué filosofía y base matemática se formó el sistema de tipos.

[pjh2568]

Me pareció muy interesante, gracias.

[devjeonghwan]

Aunque dicen que no es linting... para demostrar que la verificación de tipos es el cumplimiento estricto de un contrato, ¿no tendría que hacerse cumplir ese contrato en el binario y en tiempo de ejecución? Si no es así, me parece que sigue siendo un linting de tipos en un estado sintáctico flotante.

[tsboard]

Fue un contenido muy impresionante. Es la primera vez que me doy cuenta de que se puede ver desde esta perspectiva. Incluso compartí el enlace del blog en la empresa para recomendarles a mis colegas que lo leyeran. ¡Gracias!