Sí.
Rutinariamente escribo código en Haskell que “no soy lo suficientemente inteligente como para escribir” apoyándome mucho en Curry-Howard. Para mí, la correspondencia Curry-Howard me proporciona mucha información sobre cómo estructurar mejor mi código.
¡La vista de los tipos como proposiciones y programas como pruebas es más importante cuanto más abstracto puedas hacer las proposiciones!
- ¿Todos los números reales tienen una expansión binaria?
- ¿Puede la ciencia / psicología cognitiva ayudarlo a comprender otras áreas más rápidamente, como las matemáticas, la física y la informática?
- ¿Qué es un buen algoritmo para convertir un número decimal de coma flotante con muchos, muchos decimales en el equivalente binario?
- ¿Por qué el problema indecidible en las máquinas de Turing es interesante desde un sentido práctico?
- Cómo formular matemáticamente para seleccionar los mejores valores de N de una matriz
Cuanto más abstracto pueda hacer sus propuestas y, por lo tanto, más generales sus tipos, más escenarios podrá reutilizar. Esto reduce la contaminación del espacio de nombres desde una perspectiva de ingeniería de software y fomenta la reutilización del código por una razón profundamente fundamental, no un anuncio hoc uno.
Además, al hacer que sus tipos sean más generales, obtiene menos implementaciones posibles que pueden escribir check. Esto le da una gran comprensión de por qué su código se comporta de la manera que lo hace y por qué debe comportarse de esa manera.
Por ejemplo, en realidad es bastante fácil arruinar la escritura de la mónada de estado, pero es casi imposible escribir la mónada de estado indexado, a pesar de que este último tiene un tipo más complejo.
Mejorar la generalidad de su código a través de la paramétrica y Curry-Howard le otorga teoremas libres más fuertes, que son leyes que puede usar para razonar sobre el comportamiento de su código solo a partir de las firmas de tipo involucradas, sin preocuparse por la implementación de la función. Esto a menudo le permite lograr el santo grial de encapsulación OOP simplemente siguiendo el mismo proceso que hace que sus tipos sean más generales y su código más reutilizable, pero de tal manera que no esté en deuda con un programador que haga lo correcto. Obtiene la encapsulación en cuestión “gratis” de los tipos y el espacio de posibles pruebas.
Si va más allá y avanza hacia la correspondencia “Curry-Howard-Lambek” que le brinda el puente de tres vías entre los tipos, las proposiciones y la teoría de categorías, puede tomar prestadas aún más herramientas en la división. La comprensión de las mónadas y las comadradas como una forma de modalidad le permite razonar sobre los sistemas de efectos utilizando la posibilidad y la necesidad modales, la modalidad (!) En lógica lineal puede verse como una comonad, la lógica lineal puede verse como el lenguaje interno de un simétrico categoría monoidal, etc.
Esto le permite mover el conocimiento entre matemática pura, programación, incluso física cuántica; después de todo, esa es solo otra categoría monoidal. Rutinariamente uso diagramas de seguimiento de la teoría de categorías cuando trabajo con cualquier cosa, desde uniones de bases de datos hasta nudos para definir la mónada correcta para que funcionen mis analizadores.
Una vez que sepa cómo funciona ese puente, ¡puede mover mucha información a través de él!
