haskell - La inferencia de tipos interfiere con la transparencia referencial

referential-transparency adhoc-polymorphism

Question

¿Cuál es la promesa / garantía precisa que proporciona el lenguaje Haskell con respecto a la transparencia referencial? Al menos el informe Haskell no menciona esta noción.

Considera la expresión

(7^7^7`mod`5`mod`2)

Y quiero saber si esta expresión es o no 1. Por mi seguridad, realizaré esto dos veces:

( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )

que ahora da (True,False) con GHCi 7.4.1.

Evidentemente, esta expresión ahora es referencialmente opaca. ¿Cómo puedo saber si un programa está sujeto a tal comportamiento o no? Puedo inundar el programa con :: todo, pero eso no lo hace muy legible. ¿Hay alguna otra clase de programas de Haskell en medio que echo de menos? ¿Eso es entre uno completamente anotado y uno no anotado?

(Aparte de la única pregunta un tanto relacionada que encontré en SO, debe haber algo más sobre esto)

Answer 1

¿Cuál es la promesa / garantía precisa que proporciona el lenguaje Haskell con respecto a la transparencia referencial? Al menos el informe Haskell no menciona esta noción.

Haskell no proporciona una promesa o garantía precisa. Existen muchas funciones como unsafePerformIO o traceShow que no son referencialmente transparentes. La extensión llamada Safe Haskell sin embargo proporciona la siguiente promesa:

Transparencia referencial: las funciones en el lenguaje seguro son deterministas, evaluarlas no causará ningún efecto secundario. Las funciones en la mónada IO todavía están permitidas y se comportan como de costumbre. Sin embargo, cualquier función pura, según su tipo, tiene la garantía de ser pura. Esta propiedad permite que un usuario del lenguaje seguro confíe en los tipos. Esto significa, por ejemplo, que unsafePerformIO :: IO a -> a function no está permitida en el lenguaje seguro.

Haskell ofrece una promesa informal fuera de esto: el Preludio y las bibliotecas base tienden a estar libres de efectos secundarios y los programadores de Haskell tienden a etiquetar las cosas con efectos secundarios como tales.

Evidentemente, esta expresión ahora es referencialmente opaca. ¿Cómo puedo saber si un programa está sujeto a tal comportamiento o no? Puedo inundar el programa con :: todo, pero eso no lo hace muy legible. ¿Hay alguna otra clase de programas de Haskell en medio que echo de menos? ¿Eso es entre uno completamente anotado y uno no anotado?

Como han dicho otros, el problema surge de este comportamiento:

Prelude> ( (7^7^7`mod`5`mod`2)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(True,False)
Prelude> 7^7^7`mod`5`mod`2 :: Integer
1
Prelude> 7^7^7`mod`5`mod`2 :: Int
0

Esto sucede porque 7^7^7 es un número enorme (alrededor de 700,000 dígitos decimales) que desborda fácilmente un tipo Int 64 bits, pero el problema no será reproducible en sistemas de 32 bits:

Prelude> :m + Data.Int
Prelude Data.Int> 7^7^7 :: Int64
-3568518334133427593
Prelude Data.Int> 7^7^7 :: Int32
1602364023
Prelude Data.Int> 7^7^7 :: Int16
8823

Si se usa rem (7^7^7) 5 el resto para Int64 se informará como -3 pero como -3 es equivalente a +2 módulo 5, mod informa +2.

La respuesta de Integer se usa a la izquierda debido a las reglas predeterminadas para las clases de Integral ; el tipo Int específico de la plataforma se usa a la derecha debido al tipo de (!!) :: [a] -> Int -> a . Si usa el operador de indexación apropiado para Integral a , en su lugar obtendrá algo consistente:

Prelude> :m + Data.List
Prelude Data.List> ((7^7^7`mod`5`mod`2) == 1, genericIndex [False,True] (7^7^7`mod`5`mod`2))
(True,True)

El problema aquí no es la transparencia referencial porque las funciones que estamos llamando ^ realidad son dos funciones diferentes (ya que tienen diferentes tipos). Lo que le ha hecho tropezar es las clases de tipos, que son una implementación de ambigüedad limitada en Haskell; ha descubierto que esta ambigüedad (a diferencia de la ambigüedad no restringida, es decir, los tipos paramétricos) puede ofrecer resultados contraintuitivos. Esto no debería ser demasiado sorprendente, pero definitivamente es un poco extraño a veces.

Answer 2

¿Qué crees que tiene esto que ver con la transparencia referencial? Sus usos de 7 , ^ , mod , 5 , 2 y == son aplicaciones de esas variables a los diccionarios, sí, pero no veo por qué cree que este hecho hace que Haskell sea referencialmente opaco. ¡A menudo, aplicar la misma función a diferentes argumentos produce resultados diferentes, después de todo!

La transparencia referencial tiene que ver con esta expresión:

let x :: Int = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

x es aquí un valor único , y siempre debe tener el mismo valor único.

Por el contrario, si dices:

let x :: forall a. Num a => a; x = 7^7^7`mod`5`mod`2 in (x == 1, [False, True] !! x)

(o use la expresión en línea, que es equivalente), x es ahora una función y puede devolver diferentes valores dependiendo del argumento Num que le suministre. También puede quejarse de que let f = (+1) in map f [1, 2, 3] es [2, 3, 4] , pero let f = (+3) in map f [1, 2, 3] es [4, 5, 6] y luego diga "Haskell proporciona diferentes valores para el map f [1, 2, 3] según el contexto, por lo que es referencialmente opaco".

Answer 3

El problema es la sobrecarga, que de hecho viola la transparencia referencial. No tienes idea de lo que hace algo como (+) en Haskell; Depende del tipo.

Cuando un tipo numérico no está restringido en un programa de Haskell, el compilador usa el tipo predeterminado para elegir algún tipo adecuado. Esto es por conveniencia, y generalmente no lleva a ninguna sorpresa. Pero en este caso nos llevó a una sorpresa. En ghc puedes usar -fwarn-type-defaults para ver cuando el compilador ha usado por defecto para elegir un tipo para ti. También puede agregar la línea default () a su módulo para detener todos los valores default () .

Answer 4

No creo que haya ninguna garantía de que la evaluación de una expresión tipificada polimorfamente como 5 en diferentes tipos produzca resultados "compatibles", para cualquier definición razonable de "compatible".

Sesión GHCi:

> class C a where num :: a
> instance C Int    where num = 0
> instance C Double where num = 1
> num + length []  -- length returns an Int
0
> num + 0          -- GHCi defaults to Double for some reason
1.0

Esto parece que está rompiendo la transparencia referencial, ya que la length [] y 0 deben ser iguales, pero debajo del capó es el num que se usa en diferentes tipos.

También,

> "" == []
True
> [] == [1]
False
> "" == [1]
*** Type error

donde uno podría haber esperado False en la última línea.

Por lo tanto, creo que la transparencia referencial solo se mantiene cuando se especifican los tipos exactos para resolver el polimorfismo. Una aplicación de parámetros de tipo explícito à la System F permitiría siempre sustituir una variable con su definición sin alterar la semántica: por lo que entiendo, GHC internamente hace esto exactamente durante la optimización para garantizar que la semántica no se vea afectada. De hecho, GHC Core tiene argumentos de tipo explícito que se pasan.

Answer 5

Pensé en algo que podría ayudar a aclarar las cosas ...

La expresión mod (7^7^7) 5 tiene el tipo Integral a por lo que hay dos formas comunes de convertirlo en un Int :

1. Realice toda la aritmética utilizando operaciones y tipos de Integer y luego convierta el resultado en un Int .
2. Realice toda la aritmética utilizando las operaciones Int .

Si la expresión se usa en un contexto Int Haskell ejecutará el método # 2. Si quieres forzar a Haskell a usar el # 1 tienes que escribir:

fromInteger (mod (7^7^7) 5)

Esto asegurará que todas las operaciones aritméticas se realizarán usando operaciones y tipos de Integer .

Cuando ingresas la expresión en el REPL de ghci, las reglas predeterminadas escribieron la expresión como un Integer , por lo que se usó el método # 1. Cuando usas la expresión con el !! el operador se escribió como un Int , por lo que se calculó mediante el método # 2.

Mi respuesta original:

En Haskell la evaluación de una expresión como

(7^7^7`mod`5`mod`2)

depende completamente de qué instancia de Integral se esté utilizando, y esto es algo que cada programador de Haskell aprende a aceptar.

La segunda cosa que todo programador (en cualquier lenguaje) debe tener en cuenta es que las operaciones numéricas están sujetas a desbordamiento, subdesbordamiento, pérdida de precisión, etc. y, por lo tanto, las leyes de la aritmética no siempre son válidas. Por ejemplo, x+1 > x no siempre es cierto; La suma y el múltiplo de números reales no siempre es asociativo; La ley distributiva no siempre se cumple; etc. Cuando creas una expresión desbordante, entras en el ámbito del comportamiento indefinido.

Además, en este caso particular, hay mejores maneras de evaluar esta expresión, lo que preserva más nuestra expectativa de cuál debería ser el resultado. En particular, si desea calcular de manera eficiente y precisa un mod ^ b b, debería usar el algoritmo "mod de potencia".

Actualización: ejecute el siguiente programa para ver cómo afecta la elección de Integral instancia Integral a lo que evalúa una expresión:

import Data.Int
import Data.Word
import Data.LargeWord -- cabal install largeword

expr :: Integral a => a
expr = (7^e `mod` 5)
  where e = 823543 :: Int

main :: IO ()
main = do
  putStrLn $ "as an Integer: " ++ show (expr :: Integer)
  putStrLn $ "as an Int64:   " ++ show (expr :: Int64)
  putStrLn $ "as an Int:     " ++ show (expr :: Int)
  putStrLn $ "as an Int32:   " ++ show (expr :: Int32)
  putStrLn $ "as an Int16:   " ++ show (expr :: Int16)
  putStrLn $ "as a Word8:    " ++ show (expr :: Word8)
  putStrLn $ "as a Word16:   " ++ show (expr :: Word16)
  putStrLn $ "as a Word32:   " ++ show (expr :: Word32)
  putStrLn $ "as a Word128:  " ++ show (expr :: Word128)
  putStrLn $ "as a Word192:  " ++ show (expr :: Word192)
  putStrLn $ "as a Word224:  " ++ show (expr :: Word224)
  putStrLn $ "as a Word256:  " ++ show (expr :: Word256)

y la salida (compilada con GHC 7.8.3 (64 bits):

as an Integer: 3
as an Int64:   2
as an Int:     2
as an Int32:   3
as an Int16:   3
as a Word8:    4
as a Word16:   3
as a Word32:   3
as a Word128:  4
as a Word192:  0
as a Word224:  2
as a Word256:  1

Answer 6

Probablemente, otra cosa relacionada con la inferencia de tipo y la referencia-transparencia es la restricción "temida" del monomorfismo (su ausencia, para ser exactos). Una cita directa:

Un ejemplo, de „Una historia de Haskell“:
Considere la función genericLength, de Data.List

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

Y considera la función:

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

len tiene el tipo Num a => a y, sin la restricción de monomorfismo, podría calcularse dos veces .

Observe que en este caso los tipos de ambas expresiones son los mismos. Los resultados también lo son, pero la sustitución no siempre es posible.

Answer 7

Se ha elegido otro tipo, porque !! requiere un Int . El cálculo completo ahora usa Int lugar de Integer .

λ> ( (7^7^7`mod`5`mod`2 :: Int)==1, [False,True]!!(7^7^7`mod`5`mod`2) )
(False,False)