¿Por qué 3 yx(que se le asignó 3) tienen diferentes tipos inferidos en Haskell?

type-inference monomorphism-restriction

Question

Esta pregunta ya tiene una respuesta aquí:

• ¿Cuál es la restricción de monomorfismo? 1 respuesta

La inferencia de tipos en Haskell tiene un poco de curva de aprendizaje (¡por decir lo menos!). Una buena manera de comenzar a aprender es con ejemplos simples. Entonces, el siguiente es un poco de un "mundo de hola" para la inferencia de tipo.

Considere el siguiente ejemplo:

Prelude> :t 3
3 :: (Num t) => t
Prelude> let x = 3
Prelude> :t x
x :: Integer

La pregunta es por lo tanto: ¿Por qué 3 yx tienen diferentes tipos?

Resumen del enlace:

Lea las respuestas a continuación para la historia completa; aquí hay solo un resumen del enlace:

1. Incumplimiento de tipo GHC: Haskell Report sección 4.3.4
2. Incumplimiento de tipo extendido de GHCi: Uso de la sección 2.4.5 de GHCi
3. Restricción monomórfica: Haskell wiki

Answer 1

Como nadie más ha mencionado por qué hay una restricción de monomorfismo, pensé que agregaría este fragmento de A History of Haskell: Being Lazy With Class .

6.2 La restricción del monomorfismo Una importante fuente de controversia en las primeras etapas fue la llamada "restricción de monomorfismo". Supongamos que genericLength tiene este tipo sobrecargado:

genericLength :: Num a => [b] -> a

Ahora considere esta definición:

f xs = (len, len)
where len = genericLength xs

Parece que len debe computarse solo una vez, pero en realidad se puede calcular dos veces. ¿Por qué? Porque podemos inferir el tipo len :: (Num a) => a ; cuando se desagrega con la traducción que pasa el diccionario, len convierte en una función que se llama una vez para cada aparición de len , cada una de las cuales puede usarse en un tipo diferente.

Hughes argumentó fuertemente que era inaceptable duplicar silenciosamente la computación de esta manera. Su argumento fue motivado por un programa que había escrito que corría exponencialmente más lento de lo que esperaba. (Esto fue sin duda con un compilador muy simple, pero estábamos reacios a hacer que las diferencias de rendimiento fueran tan grandes como dependientes de las optimizaciones del compilador).

Luego de mucho debate, el comité adoptó la ahora notoria restricción de monomorfismo. Dicho brevemente, dice que una definición que no se parece a una función (es decir, que no tiene argumentos en el lado izquierdo) debe ser monomórfica en cualquier variable de tipo sobrecargada. En este ejemplo, la regla obliga a len a ser utilizado en el mismo tipo en ambas instancias, lo que resuelve el problema de rendimiento. El programador puede proporcionar una firma de tipo explícita para len si se requiere un comportamiento polimórfico.

La restricción de monomorfismo es manifiestamente una verruga en el lenguaje. Parece morder a cada nuevo programador Haskell dando lugar a un mensaje de error inesperado u oscuro. Ha habido mucha discusión de alternativas. El Compilador Haskell de Glasgow (GHC, Sección 9.1) proporciona una bandera:

-fno-monomorphism-restriction

para suprimir la restricción por completo. Pero en todo este tiempo, ninguna alternativa verdaderamente satisfactoria ha evolucionado.

Encuentro que el tono del documento hacia la restricción del monomorfismo es muy interesante.

Answer 2

Esto ocurre debido al tipo de incumplimiento en GHCi , como se discutió here , here , here y here , entre otros. Desafortunadamente, esto parece ser algo difícil de buscar, ya que hay muchas maneras de describir este comportamiento antes de que conozca la frase "tipo predeterminado".

Actualización : D''oh. Se eliminó el pobre ejemplo.

Answer 3

Hay otro factor aquí, mencionado en algunos de los enlaces que incluye acfoltzer, pero podría valer la pena hacer explícito aquí. Estás encontrando el efecto de la restricción de monomorfismo . Cuando tu dices

let x = 5

haces una definición de nivel superior de una variable . El MR insiste en que tales definiciones, cuando no estén acompañadas por una firma de tipo, deberían estar especializadas a un valor monomórfico eligiendo (con suerte) instancias predeterminadas adecuadas para las variables de tipo no resueltas. Por el contrario, cuando usa :t para solicitar un tipo inferido, no se impone tal restricción o incumplimiento. Asi que

> :t 3
3 :: (Num t) => t

porque 3 está realmente sobrecargado: es admitido por cualquier tipo numérico. Las reglas predeterminadas eligen Integer como el tipo numérico predeterminado, por lo que

> let x = 3
> :t x
x :: Integer

Pero ahora apaguemos el MR.

> :set -XNoMonomorphismRestriction
> let y = 3
> :t y
y :: (Num t) => t

Sin la MR, la definición es tan polimórfica como puede ser, tan sobrecargada como 3 . Solo revisando...

> :t y * (2.5 :: Float)
y * (2.5 :: Float) :: Float
> :t y * (3 :: Int)
y * (3 :: Int) :: Int

Tenga en cuenta que el polimórfico y = 3 se está especializando de manera diferente en estos usos, de acuerdo con el método fromInteger suministrado con la instancia Num relevante. Es decir, y no está asociado con una representación particular de 3 , sino más bien un esquema para construir representaciones de 3 . Naïvely compiled, es una receta lenta, que algunas personas citan como una motivación para el MR.

Estoy (localmente pretendiendo ser) neutral en el debate sobre si la restricción de monomorfismo es un mal menor o mayor. Siempre escribo firmas de tipo para las definiciones de nivel superior, por lo que no hay ambigüedad sobre lo que estoy tratando de lograr y el MR está al lado del punto.

Al tratar de aprender cómo funciona el sistema de tipos, es realmente útil separar los aspectos de la inferencia de tipo que

1. ''seguir el plan'', especializando las definiciones polimórficas a casos de uso particulares: una cuestión bastante sólida de resolución de restricciones, que requiere unificación básica y resolución de instancias mediante retroceso; y

2. ''adivinar el plan'', generalizando tipos para asignar un esquema de tipo polimórfico a una definición sin firma de tipo: eso es bastante frágil, y cuanto más se pasa de la disciplina básica Hindley-Milner, con clases de tipo, con polimorfismo de alto rango, con GADTs, las cosas más extrañas se vuelven.

Es bueno aprender cómo funciona el primero y comprender por qué el segundo es difícil. Gran parte de la rareza en la inferencia de tipos está asociada con la segunda, y con heurísticas como la restricción de monomorfismo que trata de ofrecer un comportamiento predeterminado útil frente a la ambigüedad.