haskell types polymorphism type-inference monomorphism-restriction

haskell - ¿Cuál es la restricción de monomorfismo?



types polymorphism (1)

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

La restricción de monomorfismo según lo establecido por la wiki de Haskell es:

una regla contra intuitiva en la inferencia de tipo Haskell. Si olvida proporcionar una firma de tipo, a veces esta regla llenará las variables de tipo libre con tipos específicos utilizando reglas de "incumplimiento de tipo".

Lo que esto significa es que, en algunas circunstancias , si su tipo es ambiguo (es decir, polimórfico), el compilador elegirá instanciar ese tipo a algo no ambiguo.

¿Cómo lo soluciono?

En primer lugar, siempre puede proporcionar explícitamente una firma de tipo y esto evitará la activación de la restricción:

plus :: Num a => a -> a -> a plus = (+) -- Okay! -- Runs as: Prelude> plus 1.0 1 2.0

Alternativamente, si está definiendo una función, puede evitar el estilo sin puntos y , por ejemplo, escribir:

plus x y = x + y

Apagarlo

Es posible simplemente desactivar la restricción para que no tenga que hacer nada a su código para arreglarlo. El comportamiento está controlado por dos extensiones: MonomorphismRestriction lo habilitará (que es el valor predeterminado) mientras que NoMonomorphismRestriction lo deshabilitará.

Puede poner la siguiente línea en la parte superior de su archivo:

{-# LANGUAGE NoMonomorphismRestriction #-}

Si está utilizando GHCi, puede habilitar la extensión con el comando: :set :

Prelude> :set -XNoMonomorphismRestriction

También puede decirle a ghc que habilite la extensión desde la línea de comando:

ghc ... -XNoMonomorphismRestriction

Nota: Realmente debería preferir la primera opción a elegir la extensión a través de las opciones de línea de comandos.

Consulte la página de GHC para obtener una explicación de esta y otras extensiones.

Una explicación completa

Trataré de resumir a continuación todo lo que necesita saber para comprender cuál es la restricción del monomorfismo, por qué se introdujo y cómo se comporta.

Un ejemplo

Tome la siguiente definición trivial:

plus = (+)

pensaría poder reemplazar cada aparición de + con plus . En particular dado que (+) :: Num a => a -> a -> a esperarías tener también plus :: Num a => a -> a -> a .

Por desgracia, este no es el caso. Por ejemplo, intentamos lo siguiente en GHCi:

Prelude> let plus = (+) Prelude> plus 1.0 1

Obtenemos el siguiente resultado:

<interactive>:4:6: No instance for (Fractional Integer) arising from the literal ‘1.0’ In the first argument of ‘plus’, namely ‘1.0’ In the expression: plus 1.0 1 In an equation for ‘it’: it = plus 1.0 1

Es posible que deba :set -XMonomorphismRestriction en las versiones más nuevas de GHCi.

Y, de hecho, podemos ver que el tipo de plus no es lo que esperaríamos:

Prelude> :t plus plus :: Integer -> Integer -> Integer

Lo que sucedió es que el compilador vio que plus tenía el tipo Num a => a -> a -> a , un tipo polimórfico. Además, sucede que la definición anterior se enmarca en las reglas que explicaré más adelante, por lo que decidió hacer que el tipo sea monomórfico al omitir la variable de tipo a . El valor predeterminado es Integer como podemos ver.

Tenga en cuenta que si intenta compilar el código anterior utilizando ghc , no obtendrá ningún error. Esto se debe a cómo ghci maneja (y debe manejar) las definiciones interactivas. Básicamente, cada declaración ingresada en ghci debe estar completamente marcada antes de considerar lo siguiente; en otras palabras, es como si cada declaración estuviera en un módulo separado. Más adelante explicaré por qué esto importa.

Otro ejemplo

Considere las siguientes definiciones:

f1 x = show x f2 = /x -> show x f3 :: (Show a) => a -> String f3 = /x -> show x f4 = show f5 :: (Show a) => a -> String f5 = show

Esperaríamos que todas estas funciones se comporten de la misma manera y tengan el mismo tipo, es decir, el tipo de show : Show a => a -> String .

Sin embargo, al compilar las definiciones anteriores obtenemos los siguientes errores:

test.hs:3:12: No instance for (Show a1) arising from a use of ‘show’ The type variable ‘a1’ is ambiguous Relevant bindings include x :: a1 (bound at blah.hs:3:7) f2 :: a1 -> String (bound at blah.hs:3:1) Note: there are several potential instances: instance Show Double -- Defined in ‘GHC.Float’ instance Show Float -- Defined in ‘GHC.Float’ instance (Integral a, Show a) => Show (GHC.Real.Ratio a) -- Defined in ‘GHC.Real’ ...plus 24 others In the expression: show x In the expression: / x -> show x In an equation for ‘f2’: f2 = / x -> show x test.hs:8:6: No instance for (Show a0) arising from a use of ‘show’ The type variable ‘a0’ is ambiguous Relevant bindings include f4 :: a0 -> String (bound at blah.hs:8:1) Note: there are several potential instances: instance Show Double -- Defined in ‘GHC.Float’ instance Show Float -- Defined in ‘GHC.Float’ instance (Integral a, Show a) => Show (GHC.Real.Ratio a) -- Defined in ‘GHC.Real’ ...plus 24 others In the expression: show In an equation for ‘f4’: f4 = show

Entonces f2 y f4 no compilan. Además, cuando intentamos definir estas funciones en GHCi no obtenemos errores , pero el tipo para f2 y f4 es () -> String !

La restricción de monomorfismo es lo que hace que f2 y f4 requieran un tipo monomórfico, y el comportamiento diferente entre ghc y ghci se debe a diferentes reglas de incumplimiento .

¿Cuando sucede?

En Haskell, como se define en el report , hay dos tipos distintos de bindings . Enlaces de funciones y enlaces de patrones. Un enlace de función no es más que una definición de una función:

f x = x + 1

Tenga en cuenta que su sintaxis es:

<identifier> arg1 arg2 ... argn = expr

Modulo de guardias y where declaraciones. Pero en realidad no importan.

donde debe haber al menos un argumento .

Un enlace de patrón es una declaración de la forma:

<pattern> = expr

De nuevo, guardias de módulo.

Tenga en cuenta que las variables son patrones , por lo que el enlace:

plus = (+)

Es un patrón vinculante. Está vinculando el patrón plus (una variable) a la expresión (+) .

Cuando un enlace de patrón consta de solo un nombre de variable, se llama enlace de patrón simple .

¡La restricción de monomorfismo se aplica a los enlaces de patrones simples!

Bueno, formalmente deberíamos decir que:

Un grupo de declaración es un conjunto mínimo de enlaces mutuamente dependientes.

Sección 4.5.1 del report .

Y luego (Sección 4.5.5 del report ):

un grupo de declaración dado no está restringido si y solo si:

  1. cada variable del grupo está vinculada por un enlace de función (por ejemplo, fx = x ) o un enlace de patrón simple (por ejemplo, plus = (+) ; Sección 4.4.3.2), y

  2. Se proporciona una firma de tipo explícito para cada variable del grupo que está vinculada por un enlace de patrón simple. (por ejemplo, plus :: Num a => a -> a -> a; plus = (+) ).

Ejemplos añadidos por mí.

Por lo tanto, un grupo de declaración restringida es un grupo en el que, o bien hay enlaces de patrones no simples (por ejemplo, (x:xs) = f something o (f, g) = ((+), (-)) ) o hay algunos enlace de patrón sin una firma de tipo (como en plus = (+) ).

La restricción de monomorfismo afecta a grupos de declaración restringidos .

La mayoría de las veces no define funciones recursivas mutuas y, por lo tanto, un grupo de declaración se convierte en un enlace.

¿Qué hace?

La restricción de monomorfismo se describe mediante dos reglas en la Sección 4.5.5 del report .

Primera regla

La restricción habitual de Hindley-Milner sobre el polimorfismo es que solo las variables de tipo que no se encuentran libres en el medio ambiente pueden generalizarse. Además, las variables de tipo restringido de un grupo de declaración restringido pueden no generalizarse en el paso de generalización para ese grupo. (Recuerde que una variable de tipo está restringida si debe pertenecer a alguna clase de tipo; consulte la Sección 4.5.2.)

La parte resaltada es lo que introduce la restricción de monomorfismo. Dice que si el tipo es polimórfico (es decir, contiene alguna variable de tipo) y esa variable de tipo está restringida (es decir, tiene una restricción de clase: por ejemplo, el tipo Num a => a -> a -> a es polimórfico porque contiene ay también contrained porque a tiene la restricción Num sobre él), entonces no puede generalizarse.

En palabras simples, no generalizar significa que los usos de la función plus pueden cambiar su tipo.

Si tuvieras las definiciones:

plus = (+) x :: Integer x = plus 1 2 y :: Double y = plus 1.0 2

entonces obtendrías un error de tipo. Porque cuando el compilador ve que se llama más sobre un Integer en la declaración de x , unificará la variable de tipo a con Integer y, por lo tanto, el tipo de plus convierte en:

Integer -> Integer -> Integer

pero luego, cuando escriba verifique la definición de y , verá que plus se aplica a un argumento Double y los tipos no coinciden.

Tenga en cuenta que aún puede usar plus sin obtener un error:

plus = (+) x = plus 1.0 2

En este caso, primero se infiere que el tipo de plus es Num a => a -> a -> a pero luego su uso en la definición de x , donde 1.0 requiere una restricción Fractional , lo cambiará a Fractional a => a -> a -> a .

Razón fundamental

El informe dice:

La regla 1 se requiere por dos razones, las cuales son bastante sutiles.

  • La regla 1 evita que los cálculos se repitan inesperadamente. Por ejemplo, genericLength es una función estándar (en la biblioteca Data.List ) cuyo tipo viene dado por

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

    Ahora considere la siguiente expresión:

    let len = genericLength xs in (len, len)

    Parece que len debería calcularse solo una vez, pero sin la Regla 1 podría calcularse dos veces, una en cada una de las dos sobrecargas diferentes. Si el programador realmente desea que se repita el cálculo, se puede agregar una firma de tipo explícito:

    let len :: Num a => a len = genericLength xs in (len, len)

Para este punto, el ejemplo de la wiki es, creo, más claro. Considere la función:

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

Si len fuera polimórfico, el tipo de f sería:

f :: Num a, Num b => [c] -> (a, b)

¡Entonces los dos elementos de la tupla (len, len) realidad podrían ser valores diferentes ! Pero esto significa que el cálculo realizado por genericLength debe repetirse para obtener los dos valores diferentes.

La razón aquí es: el código contiene una llamada de función, pero no introducir esta regla podría producir dos llamadas de función ocultas, lo cual es contrario a la intuición.

Con la restricción de monomorfismo, el tipo de f convierte en:

f :: Num a => [b] -> (a, a)

De esta manera no hay necesidad de realizar el cálculo varias veces.

  • La regla 1 evita la ambigüedad. Por ejemplo, considere el grupo de declaración

    [(n, s)] = lee t

    Recordemos que reads es una función estándar cuyo tipo viene dado por la firma

    lee :: (Leer a) => Cadena -> [(a, Cadena)]

    Sin la Regla 1, a n se le asignaría el tipo ∀ a. Read a ⇒ a ∀ a. Read a ⇒ a s el tipo ∀ a. Read a ⇒ String ∀ a. Read a ⇒ String . El último es un tipo no válido, porque es intrínsecamente ambiguo. No es posible determinar en qué sobrecarga usar s , ni esto se puede resolver agregando una firma de tipo para s . Por lo tanto, cuando se usan enlaces de patrones no simples (Sección 4.4.3.2), los tipos inferidos son siempre monomórficos en sus variables de tipo restringido, independientemente de si se proporciona una firma de tipo. En este caso, tanto n como s son monomórficos en a .

Bueno, creo que este ejemplo se explica por sí mismo. Hay situaciones en las que no aplicar la regla da como resultado una ambigüedad de tipo.

Si deshabilita la extensión como se sugiere anteriormente , recibirá un error de tipo al intentar compilar la declaración anterior. Sin embargo, esto no es realmente un problema: ya sabes que cuando usas read tienes que decirle de alguna manera al compilador qué tipo debería intentar analizar ...

Segunda regla

  1. Cualquier variable de tipo monomórfico que permanezca cuando se complete la inferencia de tipo para un módulo completo, se considera ambigua y se resuelve a tipos particulares utilizando las reglas predeterminadas (Sección 4.3.4).

Esto significa que. Si tienes tu definición habitual:

plus = (+)

Esto tendrá un tipo Num a => a -> a -> a donde a es una variable de tipo monomórfico debido a la regla 1 descrita anteriormente. Una vez que se deduce todo el módulo, el compilador simplemente elegirá un tipo que lo reemplazará de acuerdo con las reglas predeterminadas.

El resultado final es: plus :: Integer -> Integer -> Integer .

Tenga en cuenta que esto se hace después de deducir todo el módulo.

Esto significa que si tiene las siguientes declaraciones:

plus = (+) x = plus 1.0 2.0

dentro de un módulo, antes del tipo predeterminado, el tipo de plus será: Fractional a => a -> a -> a (consulte la regla 1 para ver por qué sucede esto). En este punto, siguiendo las reglas predeterminadas, a será reemplazado por Double y entonces tendremos plus :: Double -> Double -> Double x :: Double .

Incumplimiento

Como se indicó anteriormente, existen algunas reglas predeterminadas , descritas en la Sección 4.3.4 del Informe , que el inferenciador puede adoptar y que reemplazará un tipo polimórfico por uno monomórfico. Esto sucede cuando un tipo es ambiguo .

Por ejemplo en la expresión:

let x = read "<something>" in show x

aquí la expresión es ambigua porque los tipos para show y read son:

show :: Show a => a -> String read :: Read a => String -> a

Entonces la x tiene el tipo Read a => a . Pero esta restricción es satisfecha por muchos tipos: Int , Double o () por ejemplo. ¿Cuál elegir? No hay nada que nos pueda decir.

En este caso podemos resolver la ambigüedad diciéndole al compilador qué tipo queremos, agregando una firma de tipo:

let x = read "<something>" :: Int in show x

Ahora el problema es: dado que Haskell usa la clase de tipo Num para manejar números, hay muchos casos en los que las expresiones numéricas contienen ambigüedades.

Considerar:

show 1

¿Cuál debería ser el resultado?

Como antes, 1 tiene el tipo Num a => a y hay muchos tipos de números que podrían usarse. ¿Cuál elegir?

Tener un error del compilador casi cada vez que usamos un número no es algo bueno, y por lo tanto, se introdujeron las reglas predeterminadas. Las reglas se pueden controlar mediante una declaración default . Al especificar el default (T1, T2, T3) podemos cambiar la forma en que el inferencia predetermina los diferentes tipos.

Una variable de tipo ambigua v es predeterminada si:

  • v aparece solo en contracciones del tipo C v C es una clase (es decir, si aparece como en: Monad (mv) entonces no es predeterminado).
  • al menos una de estas clases es Num o una subclase de Num .
  • Todas estas clases se definen en el Preludio o en una biblioteca estándar.

Una variable de tipo predeterminada se reemplaza por el primer tipo en la lista default que es una instancia de todas las clases de variables ambiguas.

La declaración predeterminada default es default (Integer, Double) .

Por ejemplo:

plus = (+) minus = (-) x = plus 1.0 1 y = minus 2 1

Los tipos inferidos serían:

plus :: Fractional a => a -> a -> a minus :: Num a => a -> a -> a

que, por incumplimiento de las reglas, se convierten en:

plus :: Double -> Double -> Double minus :: Integer -> Integer -> Integer

Tenga en cuenta que esto explica por qué en el ejemplo de la pregunta solo la definición de sort genera un error. El tipo Ord a => [a] -> [a] no puede ser predeterminado porque Ord no es una clase numérica.

Incumplimiento extendido

Tenga en cuenta que GHCi viene con reglas predeterminadas extendidas (o aquí para GHC8 ), que también se pueden habilitar en archivos usando las extensiones ExtendedDefaultRules .

Las variables de tipo por defecto no solo necesitan aparecer en contraints donde todas las clases son estándar y debe haber al menos una clase que esté entre Eq , Ord , Show o Num y sus subclases.

Además, la declaración predeterminada default es default ((), Integer, Double) .

Esto puede producir resultados extraños. Tomando el ejemplo de la pregunta:

Prelude> :set -XMonomorphismRestriction Prelude> import Data.List(sortBy) Prelude Data.List> let sort = sortBy compare Prelude Data.List> :t sort sort :: [()] -> [()]

en ghci no obtenemos un error de tipo, pero las restricciones Ord a dan como resultado un valor predeterminado de () que es prácticamente inútil.

Enlaces útiles

Hay muchos recursos y debates sobre la restricción del monomorfismo.

Aquí hay algunos enlaces que encuentro útiles y que pueden ayudarlo a comprender o profundizar en el tema:

Me sorprende cómo el compilador de haskell a veces infiere tipos que son menos polimórficos de lo que esperaría, por ejemplo, cuando se utilizan definiciones sin puntos.

Parece que el problema es la "restricción de monomorfismo", que está activada de forma predeterminada en las versiones anteriores del compilador.

Considere el siguiente programa haskell:

{-# LANGUAGE MonomorphismRestriction #-} import Data.List(sortBy) plus = (+) plus'' x = (+ x) sort = sortBy compare main = do print $ plus'' 1.0 2.0 print $ plus 1.0 2.0 print $ sort [3, 1, 2]

Si compilo esto con ghc no ghc y la salida del ejecutable es:

3.0 3.0 [1,2,3]

Si cambio el cuerpo main a:

main = do print $ plus'' 1.0 2.0 print $ plus (1 :: Int) 2 print $ sort [3, 1, 2]

No obtengo errores de tiempo de compilación y la salida se convierte en:

3.0 3 [1,2,3]

como se esperaba. Sin embargo, si trato de cambiarlo a:

main = do print $ plus'' 1.0 2.0 print $ plus (1 :: Int) 2 print $ plus 1.0 2.0 print $ sort [3, 1, 2]

Me sale un error de tipo:

test.hs:13:16: No instance for (Fractional Int) arising from the literal ‘1.0’ In the first argument of ‘plus’, namely ‘1.0’ In the second argument of ‘($)’, namely ‘plus 1.0 2.0’ In a stmt of a ''do'' block: print $ plus 1.0 2.0

Lo mismo ocurre cuando intenta llamar a sort dos veces con diferentes tipos:

main = do print $ plus'' 1.0 2.0 print $ plus 1.0 2.0 print $ sort [3, 1, 2] print $ sort "cba"

produce el siguiente error:

test.hs:14:17: No instance for (Num Char) arising from the literal ‘3’ In the expression: 3 In the first argument of ‘sort’, namely ‘[3, 1, 2]’ In the second argument of ‘($)’, namely ‘sort [3, 1, 2]’

  • ¿Por qué ghc repente piensa que plus no es polimórfico y requiere un argumento Int ? La única referencia a Int está en una aplicación de plus , ¿cómo puede importar eso cuando la definición es claramente polimórfica?
  • ¿Por qué ghc repente piensa que ese sort requiere una instancia de Num Char ?

Además, si trato de colocar las definiciones de funciones en su propio módulo, como en:

{-# LANGUAGE MonomorphismRestriction #-} module TestMono where import Data.List(sortBy) plus = (+) plus'' x = (+ x) sort = sortBy compare

Me sale el siguiente error al compilar:

TestMono.hs:10:15: No instance for (Ord a0) arising from a use of ‘compare’ The type variable ‘a0’ is ambiguous Relevant bindings include sort :: [a0] -> [a0] (bound at TestMono.hs:10:1) Note: there are several potential instances: instance Integral a => Ord (GHC.Real.Ratio a) -- Defined in ‘GHC.Real’ instance Ord () -- Defined in ‘GHC.Classes’ instance (Ord a, Ord b) => Ord (a, b) -- Defined in ‘GHC.Classes’ ...plus 23 others In the first argument of ‘sortBy’, namely ‘compare’ In the expression: sortBy compare In an equation for ‘sort’: sort = sortBy compare

  • ¿Por qué ghc no puede usar el tipo polimórfico Ord a => [a] -> [a] para sort ?
  • ¿Y por qué ghc trata a plus y plus'' diferente? plus debería tener el tipo polimórfico Num a => a -> a -> a y realmente no veo cómo esto es diferente del tipo de sort y, sin embargo, solo la sort genera un error.

Lo último: si comento la definición de sort el archivo compila. Sin embargo, si trato de cargarlo en ghci y ghci los tipos que obtengo:

*TestMono> :t plus plus :: Integer -> Integer -> Integer *TestMono> :t plus'' plus'' :: Num a => a -> a -> a

¿Por qué no es el tipo de plus polimórfico?

Esta es la pregunta canónica sobre la restricción del monomorfismo en Haskell como se discutió en la meta pregunta .