NoMonomorfismoRestricción ayuda a preservar el intercambio?

Question

Estaba tratando de responder another question sobre polimorfismo vs compartir cuando tropecé con este extraño comportamiento.

En GHCi, cuando define explícitamente una constante polimórficas, no hay nada para compartir, lo cual es comprensible:

> let fib :: Num a => [a]; fib = 1 : 1 : zipWith (+) fib (tail fib) 
> fib !! 30 
1346269 
(5.63 secs, 604992600 bytes) 

Por otro lado, si lo intento para lograr el mismo por la omisión de la firma de tipo y desactivando la restricción de monomorfismo, ¡mi constante se comparte de repente!

> :set -XNoMonomorphismRestriction 
> let fib = 1 : 1 : zipWith (+) fib (tail fib) 
> :t fib 
fib :: Num a => [a] 
> fib !! 50 
20365011074 
(0.00 secs, 2110136 bytes) 

¿Por qué ?!

Ugh ... Cuando se compila con optimizaciones, es rápido incluso con la restricción de monomorfismo desactivada.

Answer 1

Al dar a la firma de tipo explícita, se impide que GHC de hacer ciertas suposiciones acerca de su código. Voy a mostrar un ejemplo (tomado de esta question):

foo (x:y:_) = x == y 
foo [_]  = foo [] 
foo []  = False 

Según GHCi, el tipo de esta función es Eq a => [a] -> Bool, como era de esperar. Sin embargo, si declara foo con esta firma, obtendrá un error de "variable de tipo ambiguo".

La razón por la cual esta función solo funciona sin una firma de tipo es por la forma en que funciona la comprobación de tipo en GHC. Cuando omite una firma de tipo, se supone que foo tiene el monotipo [a] -> Bool para algún tipo fijo a. Una vez que termine de escribir el grupo de enlace, generalice los tipos. Ahí es donde obtienes el forall a. ....

Por otro lado, cuando se declara una firma de tipo polimórfico, que explícitamente que foo es polimórfico (y por lo tanto el tipo de [] no tiene por qué coincidir con el tipo de primer argumento) y la pluma, se obtiene el tipo ambigua variable.

Ahora, sabiendo esto, vamos a comparar el núcleo:

fib = 0:1:zipWith (+) fib (tail fib) 
----- 
fib :: forall a. Num a => [a] 
[GblId, Arity=1] 
fib = 
    \ (@ a) ($dNum :: Num a) -> 
    letrec { 
     fib1 [Occ=LoopBreaker] :: [a] 
     [LclId] 
     fib1 = 
     break<3>() 
     : @ a 
      (fromInteger @ a $dNum (__integer 0)) 
      (break<2>() 
      : @ a 
      (fromInteger @ a $dNum (__integer 1)) 
      (break<1>() 
       zipWith 
       @ a @ a @ a (+ @ a $dNum) fib1 (break<0>() tail @ a fib1))); } in 
    fib1 

Y para el segundo:

fib :: Num a => [a] 
fib = 0:1:zipWith (+) fib (tail fib) 
----- 
Rec { 
fib [Occ=LoopBreaker] :: forall a. Num a => [a] 
[GblId, Arity=1] 
fib = 
    \ (@ a) ($dNum :: Num a) -> 
    break<3>() 
    : @ a 
     (fromInteger @ a $dNum (__integer 0)) 
     (break<2>() 
     : @ a 
     (fromInteger @ a $dNum (__integer 1)) 
     (break<1>() 
      zipWith 
      @ a 
      @ a 
      @ a 
      (+ @ a $dNum) 
      (fib @ a $dNum) 
      (break<0>() tail @ a (fib @ a $dNum)))) 
end Rec } 

Con la firma de tipo explícita, como con foo anterior, GHC tiene que tratar fib como valor potencialmente polimórficamente recursivo. nos podíamos dejar pasar algunos Num diccionario diferente a fib en zipWith (+) fib ... y en este punto habría que tirar la mayor parte de la lista de distancia, desde diferentes Num medio distinto (+). Por supuesto, una vez que compila con optimizaciones, GHC nota que el diccionario Num nunca cambia durante "llamadas recursivas" y lo optimiza.

En el núcleo de arriba, puede ver que GHC efectivamente da fib un diccionario Num (llamado $dNum) una y otra vez.

Debido fib sin tipo de firma se asumió que era monomórfica antes de que se terminó la generalización de todo el grupo de unión, la fib subpartes recibieron exactamente el mismo tipo como a toda la fib. Gracias a esto, se ve como fib:

{-# LANGUAGE ScopedTypeVariables #-} 
fib :: forall a. Num a => [a] 
fib = fib' 
    where 
    fib' :: [a] 
    fib' = 0:1:zipWith (+) fib' (tail fib') 

Y debido a que el tipo se mantiene fijo, puede utilizar sólo el diccionario dada en el arranque.

Answer 2

Aquí está usando fib con el mismo argumento de tipo en ambos casos, y ghc es lo suficientemente inteligente como para ver esto y compartir.

Ahora, si se ha utilizado la función donde se le puede llamar con diferentes argumentos de tipo, y el impago llevó a una de las personas que es muy diferente a la otra, entonces la falta de restricción monomorphism tendría que morder.

considerar el uso del término x = 2 + 2 polimórfica en dos contextos sin la restricción monomorphism, donde en un contexto en el que show (div x 2) y en otro se utiliza show (x/2), en un escenario a obtener los Integral y Show limitaciones que le hace por defecto a Integer, en el otro obtiene una restricción Fractional y Show y eso lo predetermina a Double, por lo que el resultado del cálculo no se comparte, ya que está trabajando con un término polimórfico aplicado a dos tipos distintos. Con la restricción de monomorfismo activada, intenta realizar un ajuste predeterminado una vez para algo tanto Integral como Fraccional y falla.

mente que su Tricker para conseguir todo esto al fuego en estos días con no dejar que la generalización, etc.