¿Qué es la restricción del monomorfismo?

La restricción de monomorfismo según lo establecido por el 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 se completará las variables de tipo libre con tipos específicos usando reglas de "tipo predeterminado".

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

¿Cómo lo arreglo?

En primer lugar, siempre puede proporcionar explícitamente una firma de tipo y esto evitar el desencadenamiento 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 estilo libre de puntos, y por ejemplo escribe:

plus x y = x + y

Apagándolo

Es posible simplemente desactive la restricción para que no tenga que hacer cualquier cosa a su código para arreglarlo. El comportamiento se controla mediante dos extensiones: MonomorphismRestriction lo habilitará (que es el predeterminado) mientras NoMonomorphismRestriction lo desactivará.

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

{-# LANGUAGE NoMonomorphismRestriction #-}

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

Prelude> :set -XNoMonomorphismRestriction

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

ghc ... -XNoMonomorphismRestriction

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

Refiérase a la página de GHC para una explicación de esta y otras extensiones.

Una explicación completa

Voy a tratar de resumir a continuación todo lo que necesita saber para entender lo que el la restricción del monomorfismo es, por qué se introdujo y cómo se comporta.

Un ejemplo

Tome la siguiendo una definición trivial:

plus = (+)

Usted pensaría que sería capaz de reemplazar cada aparición de + con plus. En particular, ya que (+) :: Num a => a -> a -> a usted esperaría también tener plus :: Num a => a -> a -> a.

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

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

Obtenemos la siguiente salida:

<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 necesite :set -XMonomorphismRestriction en las versiones más recientes de GHCi.}

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

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. Por otra parte sucede que la definición anterior cae bajo las reglas que explicaré más adelante y así decidió hacer el tipo monomórfico por por defecto la variable de tipo a. El valor predeterminado es Integer como podemos ver.

Tenga en cuenta que si intenta compilar el código anterior usando ghc no obtendrá ningún error. Esto se debe a cómo ghci maneja (y debe manejar) las definiciones interactivas. Básicamente, cada instrucción ingresada en ghci debe ser completamente tipo verificado antes se considera lo siguiente; en otras palabras, es como si cada declaración estuviera en una módulo. Más tarde explicaré por qué este asunto.

Algún 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 lo 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

Así que f2 y f4 no compilan. Además, al tratar de definir estas funciones en GHCi obtenemos no hay errores , pero el tipo para f2 y f4 es () -> String!

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

¿Cuándo sucede?

En Haskell, como se define en el informe , hay dos distintos tipos de fijaciones. Fijaciones de funciones y fijaciones de patrones. Un enlace de función no es otra cosa 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 guards and where declarations. Pero no lo hacen realmente asunto.}

Donde debe haber al menos un argumento.

Una encuadernación de patrón es una declaración de la forma:

<pattern> = expr

^{Otra vez, guardias modulo.}

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

plus = (+)

Es un patrón de unión. Está enlazando el patrón plus (una variable) a la expresión (+).

Cuando un enlace de patrón consiste solo en un nombre de variable es llamado a simple enlace de patrón.

La restricción de monomorfismo se aplica a las fijaciones de patrones simples!

Bueno, formalmente deberíamos decir que: {[160]]}

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

^{Sección 4.5.1 del informe .}

Y luego (Sección 4.5.5 del informe ):

Un grupo de declaración dado es no restringido si y solo si:

1. Cada variable en el grupo está vinculada por un enlace de función (por ejemplo, f x = x) o una simple unión de patrones (por ejemplo, plus = (+); Sección 4.4.3.2), y

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

^{Ejemplos añadidos por mí.}

So a restricted grupo de declaración es un grupo donde, o bien hay no simples fijaciones de patrones (por ejemplo, (x:xs) = f something o (f, g) = ((+), (-))) o hay un simple 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 se definen funciones recursivas mutuas y, por lo tanto, una declaración el grupo se convierte simplemente en un enlace.

¿Qué hace hacer?

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

Primera regla

La restricción habitual de Hindley-Milner sobre el polimorfismo es que solo el tipo las variables que no ocurren libres en el ambiente pueden ser generalizadas. Además, las variables de tipo restringido de una declaración restringida el grupo no puede generalizarse en el paso de generalización para ese grupo. (Recordemos que un tipo variable está restringido si debe pertenecer a algunos clase de tipo; véase 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 a y también está contraindicado porque el a tiene la restricción Num sobre se.) entonces no puede generalizarse.

En palabras simples no generalizar significa que el utiliza de la función plus puede cambiar su tipo.

Si tuvieras las definiciones:{[160]]}

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 plus es llamado sobre un Integer en la declaración de x unificará el tipo variable a con Integer y por lo tanto el tipo de plus se convierte en:

Integer -> Integer -> Integer

Pero luego, cuando escriba check the definition of y, verá que plus se aplica a un argumento Double, y los tipos no coinciden.

Tenga en cuenta que todavía puede usar plus sin obtener un error:

plus = (+)
x = plus 1.0 2

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

Justificación

El informe dice:

La regla 1 es requerida 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 como si len se debe calcular solo una vez, pero sin Regla 1 se puede ser calculado dos veces, una vez en cada uno de dos diferentes sobrecargas. Si el programador realmente desea que el cálculo se repita, se puede añadir una firma de tipo explícita:

  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)

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

La justificación aquí es: el código contiene una llamada a la función, pero no introduce esta regla podría producir dos llamadas a funciones ocultas, lo cual es contrario a lo intuitivo.

Con la restricción de monomorfismo el tipo de f se 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

  Recordar que reads es una función estándar, cuyo tipo es la firma

  Reads:: (Read a) = > String - > [(a, String)]

  Sin Regla 1, a n se le asignaría el tipo ∀ a. Read a ⇒ a y s el tipo ∀ a. Read a ⇒ String. Este último es un tipo no válido, porque es inherentemente ambiguo. No es posible determinar en qué sobrecarga usar s, tampoco se puede resolver esto añadiendo una firma de tipo para s. Por lo tanto, cuando se utilizan encuadernaciones 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 monomorfos en a.

Bueno, creo que este ejemplo se explica por sí mismo. Hay situaciones cuando no la aplicación de la regla resulta en ambigüedad de tipo.

Si deshabilita la extensión como se sugiere anteriormente, obtendrá un error de tipo cuando tratando de compilar la declaración anterior. Sin embargo, esto no es realmente un problema: ya sabes que al usar 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 la inferencia de tipo para un entero el módulo está completo, se consideran ambiguos y se resuelven a tipos particulares utilizando las reglas de incumplimiento (Sección 4.3.4 ).

Esto significa que. Si tiene su definición habitual:

plus = (+)

, Esto tendrá un tipo Num a => a -> a -> a donde a es un variable de tipo monomórfica debido a la regla 1 descrita anteriormente. Una vez que todo el módulo se infiere que el compilador simplemente elegirá un tipo que reemplazará a a de acuerdo con el incumplimiento regla.

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

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

Esto significa que si usted tiene las siguientes declaraciones:

plus = (+)

x = plus 1.0 2.0

Dentro de un módulo, antes de tipo predeterminado el tipo de plus será: Fractional a => a -> a -> a (ver regla 1 para saber por qué sucede esto). En este punto, siguiendo las reglas de incumplimiento, a se reemplazará por Double y así tendremos plus :: Double -> Double -> Double y x :: Double.

Incumplimiento

Como se indicó anteriormente, existen algunas reglas de incumplimiento, descritas en Sección 4.3.4 del Informe, que el inferencer 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

So el 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 pueda decirnos.

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

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

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

Considere:

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 de compilador casi cada vez que usamos un número no es algo bueno, y por lo tanto se introdujeron las reglas de incumplimiento. Las reglas pueden ser controladas utilizando una declaración default. Al especificar default (T1, T2, T3) podemos cambiar cómo el inferencer default los diferentes tipo.

Una variable de tipo ambigua v es predeterminada si:

• v aparece solo en contraindicaciones del tipo C v donde C es una clase (es decir, si aparece como en: Monad (m v) entonces es no por defecto).
• al menos una de estas clases es Num o una subclase de Num.
• todas estas clases están definidas en el Prelude o en una biblioteca estándar.

Una variable de tipo predeterminada se sustituye por la primero escriba en la lista default es una instancia de todas las clases de la variable ambigua.

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 reglas de incumplimiento, se convierten en: {[160]]}

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

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

Extended defaulting

Tenga en cuenta que GHCi viene con extended defaulting rules (or herefor GHC8 ), que también se puede habilitar en archivos usando las extensiones ExtendedDefaultRules.

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

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

Esto puede producir resultados impares. 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 un valor predeterminado de () que es prácticamente inútil.

Enlaces útiles

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

Aquí hay algunos enlaces que encuentro útil y que puede ayudarle a entender o profundizar en el tema:

• La página wiki de Haskell: Restricción de monomorfismo
• El informe
• Una entrada de blog accesible y agradable
• Las secciones 6.2 y 6.3 de Una Historia De Haskell: Ser perezoso Con la Clase trata de la restricción de monomorfismo y la omisión de tipos