Mucha gente ha enumerado cosas buenas sobre Haskell. Pero en respuesta a su pregunta específica "¿por qué el sistema de tipos hace que los programas sean más correctos?", Sospecho que la respuesta es "polimorfismo paramétrico".
Considere la siguiente función de Haskell:
foobar :: x -> y -> y
Hay literalmente solamente una forma posible de implementar esta función. Solo por la firma de tipo, puedo decir con precisión qué hace esta función, porque solo hay una cosa posible que puede hacer. [OK, no del todo, ¡pero casi!]
Detente y piensa en eso por un momento. Eso es realmente un gran problema! Significa que si escribo una función con esta firma, en realidad es imposible que la función haga algo más de lo que pretendía. (La firma de tipo en sí puede estar equivocada, por supuesto. Ningún lenguaje de programación evitará todos los errores).
Considere esta función:
fubar :: Int -> (x -> y) -> y
Esta función es imposible . Literalmente no puede implementar esta función. Puedo decir eso solo por la firma de tipo.
Como puede ver, ¡una firma tipo Haskell le dice mucho!
Compare con C #. (Lo siento, mi Java está un poco oxidado).
public static TY foobar<TX, TY>(TX in1, TY in2)
Hay un par de cosas que este método podría hacer:
- Regresar
in2
como el resultado.
- Bucle para siempre, y nunca devolver nada.
- Lanza una excepción y nunca devuelvas nada.
En realidad, Haskell también tiene estas tres opciones. Pero C # también le brinda las opciones adicionales:
- Regreso nulo. (Haskell no tiene nulo).
- Modifique
in2
antes de devolverlo. (Haskell no tiene modificación en el lugar).
- Usa la reflexión. (Haskell no tiene reflejo).
- Realice múltiples acciones de E / S antes de devolver un resultado. (Haskell no le permitirá realizar E / S a menos que declare que realiza E / S aquí).
La reflexión es un martillo particularmente grande; usando la reflexión, puedo construir un nuevo TY
objeto de la nada, ¡y devolverlo! Puedo inspeccionar ambos objetos y hacer diferentes acciones dependiendo de lo que encuentre. Puedo hacer modificaciones arbitrarias a los dos objetos pasados.
I / O es un martillo igualmente grande. El código podría estar mostrando mensajes al usuario, abriendo conexiones de bases de datos, o formateando su disco duro, o cualquier cosa, realmente.
La foobar
función de Haskell , por el contrario, solo puede tomar algunos datos y devolverlos sin cambios. No puede "mirar" los datos, porque su tipo es desconocido en tiempo de compilación. No puede crear nuevos datos, porque ... bueno, ¿cómo se construyen los datos de cualquier tipo posible? Necesitarías reflexión para eso. No puede realizar ninguna E / S, porque la firma de tipo no declara que se está realizando la E / S. Por lo tanto, no puede interactuar con el sistema de archivos o la red, ¡ni siquiera ejecutar hilos en el mismo programa! (Es decir, es 100% garantizado a prueba de hilos).
Como puede ver, al no permitirle hacer un montón de cosas, Haskell le permite hacer garantías muy sólidas sobre lo que realmente hace su código. Tan apretado, de hecho, que (para un código realmente polimórfico) generalmente solo hay una forma posible de que las piezas puedan encajar.
(Para ser claros: aún es posible escribir funciones Haskell donde la firma de tipo no le dice mucho. Int -> Int
Podría ser casi cualquier cosa. Pero incluso entonces, sabemos que la misma entrada siempre producirá la misma salida con 100% de certeza. ¡Java ni siquiera garantiza eso!)
Maybe
solo hacia el final. Si tuviera que elegir una cosa que los idiomas más populares deberían tomar prestada de Haskell, sería esta. Es una idea muy simple (por lo que no es muy interesante desde un punto de vista teórico), pero esto solo facilitaría mucho nuestro trabajo.