¿Qué hace que el sistema de tipos de Haskell sea más "potente" que los sistemas de otros idiomas?

Question

Leyendo Disadvantages of Scala type system versus Haskell?, tengo que preguntar: ¿qué es, específicamente, lo que hace que el sistema de tipos de Haskell sea más poderoso que los sistemas de otros idiomas (C, C++, Java)? Aparentemente, incluso Scala no puede realizar algunos de los mismos poderes que el sistema de tipos de Haskell. ¿Qué es, específicamente, lo que hace que el sistema de tipos de Haskell (inferencia tipo Hindley-Milner) sea tan poderoso? ¿Puede dar un ejemplo?

Answer 1

Una cosa que realmente me gusta y extraño en otros idiomas es el soporte de las tipologías, que son una solución elegante para muchos problemas (incluyendo, por ejemplo, funciones polivalentes).

Usando clases de tipos, es extremadamente fácil de definir funciones muy abstractos, que siguen siendo de tipo seguro por completo - como por ejemplo este Fibonacci-función:

fibs :: Num a => [a] 
fibs@(_:xs) = 0:1:zipWith (+) fibs xs 

Por ejemplo:

map (`div` 2) fibs  -- integral context 
(fibs !! 10) + 1.234  -- rational context 
map (:+ 1.0) fibs   -- Complex context 

Usted incluso puede definir su propio tipo numérico para esto.

Answer 2

qué se trata, en concreto, que hace que el sistema de tipos de Haskell

Se ha diseñado para la última década para ser flexible - como una lógica para la verificación de la propiedad - y de gran alcance. El sistema de tipo Haskell se ha desarrollado a lo largo de los años para fomentar una disciplina de comprobación estática expresiva y relativamente flexible, con varios grupos de investigadores que identifican técnicas de sistema de tipos que permiten nuevas clases potentes de verificación en tiempo de compilación. Scala está relativamente poco desarrollado en esa área.

Es decir, Haskell/GHC proporciona una lógica que es a la vez potente y está diseñada para fomentar la programación de tipo de nivel. Algo bastante único en el mundo de la programación funcional.

Algunos documentos que dan una idea de la dirección que el esfuerzo de ingeniería en el sistema de tipos de Haskell ha tomado:

• Fun with type functions
• Associated types with class
• Fun with functional dependencies

Answer 3

Hindley-Milner no es una tipo de sistema, pero un algoritmo de inferencia de tipo. El sistema de tipos de Haskell, en su día, solía poder inferirse completamente usando HM, pero ese barco ha navegado durante mucho tiempo por Haskell moderno con extensiones. (ML sigue siendo capaz de ser completamente inferido).

Podría decirse que la capacidad de inferir de manera total o parcial a todos los tipos produce poder en términos de expresividad.

Pero eso no es en gran parte de lo que creo que realmente se trata la pregunta.

Los documentos que se vinculan apuntan al otro aspecto: que las extensiones del sistema de tipos de Haskell lo hacen completo (y que las familias de tipo moderno hacen que el lenguaje completo se asemeje mucho más a la programación de nivel de valor). Otro buen artículo sobre este tema es McBride's Faking It: Simulating Dependent Types in Haskell.

El papel en el otro hilo en Scala: "Clases de tipo como objetos e Implicits" entra en por qué también se puede hacer la mayor parte de esto en Scala, aunque con un poco más de explicitud. Tiendo a sentir, pero esto es más una intuición que de la experiencia real de Scala, que su enfoque más ad-hoc y explícito (lo que la discusión de C++ llamó "nominal") es en última instancia un poco más desordenado.

Answer 4

El lenguaje Haskell le permite escribir un código más seguro sin renunciar a las funcionalidades. La mayoría de los lenguajes de hoy en día ofrecen características de seguridad: el lenguaje Haskell está ahí para mostrar que es posible tener ambos.

Podemos vivir sin punteros nulos, fundiciones explícitas, tipas sueltas y aún así tener un lenguaje perfectamente expresivo, capaz de producir un código final eficiente.

Más, el sistema de tipo Haskell, junto con su enfoque de codificación perezosa por defecto y pureza, le da un impulso en cuestiones complicadas pero importantes como el paralelismo y la concurrencia.

Sólo mis dos centavos.

Answer 5

Vamos con un ejemplo muy simple: Haskell's Maybe.

data Maybe a = Nothing | Just a 

En C++:

template <T> 
struct Maybe { 
    bool isJust; 
    T value; // IMPORTANT: must ignore when !isJust 
}; 

Vamos a considerar estas dos firmas de función, en Haskell:

sumJusts :: Num a => [Maybe a] -> a 

y C++:

template <T> T sumJusts(vector<maybe<T> >); 

Diferencias:

• En C++ hay más errores posibles de realizar. El compilador no comprueba la regla de uso de Maybe.
• El tipo de C++ de sumJusts no especifica que requiere + y emite desde 0. Los mensajes de error que aparecen cuando las cosas no funcionan son crípticas e impares. En Haskell el compilador simplemente se quejan de que el tipo no es una instancia de Num, muy sencillo ..

En resumen, Haskell tiene:

• TDAs
• Tipo-clases
• Un una sintaxis muy amigable y un buen soporte para los genéricos (que en C++ las personas intentan evitar a causa de todos sus cryptickynessishisms)