haskell - ¿Cuándo es unsafeInterleaveIO inseguro?

ghc lazy-evaluation

Question

A diferencia de otras operaciones no seguras *, la documentación para unsafeInterleaveIO no es muy clara acerca de sus posibles dificultades. ¿Entonces exactamente cuándo es inseguro? Me gustaría saber la condición tanto para el uso paralelo / concurrente como para el uso de un solo hilo.

Más específicamente, ¿son las dos funciones en el siguiente código semánticamente equivalentes? Si no, ¿cuándo y cómo?

joinIO :: IO a -> (a -> IO b) -> IO b
joinIO a f = do !x <- a
!x'' <- f x
return x''
joinIO'':: IO a -> (a -> IO b) -> IO b
joinIO'' a f = do !x <- unsafeInterleaveIO a
!x'' <- unsafeInterleaveIO $ f x
return x''

Así es como usaría esto en la práctica:

data LIO a = LIO {runLIO :: IO a}
instance Functor LIO where
fmap f (LIO a) = LIO (fmap f a)
instance Monad LIO where
return x = LIO $ return x
a >>= f = LIO $ lazily a >>= lazily . f
where
lazily = unsafeInterleaveIO . runLIO
iterateLIO :: (a -> LIO a) -> a -> LIO [a]
iterateLIO f x = do
x'' <- f x
xs <- iterateLIO f x'' -- IO monad would diverge here
return $ x:xs
limitLIO :: (a -> LIO a) -> a -> (a -> a -> Bool) -> LIO a
limitLIO f a converged = do
xs <- iterateLIO f a
return . snd . head . filter (uncurry converged) $ zip xs (tail xs)
root2 = runLIO $ limitLIO newtonLIO 1 converged
where
newtonLIO x = do () <- LIO $ print x
LIO $ print "lazy io"
return $ x - f x / f'' x
f x = x^2 -2
f'' x = 2 * x
converged x x'' = abs (x-x'') < 1E-15

Aunque preferiría evitar usar este código en aplicaciones serias debido a las terribles cosas unsafe* , al menos podría ser más perezoso de lo que sería posible con la mónada IO más estricta para decidir qué significa "convergencia", lo que lleva a (lo que creo que es) Haskell más idiomático. Y esto plantea otra pregunta: ¿por qué no es la semántica por defecto para la mónada IO de Haskell (o GHC)? He escuchado algunos problemas de administración de recursos para el IO perezoso (que GHC solo proporciona con un pequeño conjunto de comandos fijos), pero los ejemplos que normalmente se parecen se parecen a un archivo de make roto: un recurso X depende de un recurso Y, pero si falla para especificar la dependencia, obtiene un estado indefinido para X. ¿Es perezoso IO realmente el culpable de este problema? (Por otro lado, si hay un error de concurrencia sutil en el código anterior, como los puntos muertos, lo tomaría como un problema más fundamental).

Actualizar

Leyendo la respuesta de Ben y Dietrich y sus comentarios a continuación, he explorado brevemente el código fuente de ghc para ver cómo se implementa la mónada IO en GHC. Aquí resumiré mis pocos descubrimientos.

1. GHC implementa Haskell como un lenguaje impuro, no referencialmente transparente. El tiempo de ejecución de GHC funciona evaluando sucesivamente funciones impuras con efectos secundarios como cualquier otro lenguaje funcional. Por eso es importante el orden de evaluación.

2. unsafeInterleaveIO no es seguro porque puede introducir cualquier tipo de errores de concurrencia, incluso en un programa de subprocesos sigle, exponiendo la (normalmente) impureza oculta de Haskell de GHC. ( iteratee parece ser una solución agradable y elegante para esto, y ciertamente aprenderé a usarla).

3. La mónada IO debe ser estricta porque una mónada IO segura y perezosa requeriría una representación precisa (realzada) del Mundo Real, lo que parece imposible.

4. No solo las funciones monádica y unsafe IO son inseguras. La totalidad de Haskell (según lo implementado por GHC) es potencialmente insegura, y las funciones ''puras'' en Haskell (GHC) son puras solo por convención y por la buena voluntad de la gente. Los tipos nunca pueden ser una prueba de pureza.

Para ver esto, demuestro que Haskell de GHC no es referencialmente transparente independientemente de la mónada IO, independientemente de las funciones unsafe* , etc.

-- An evil example of a function whose result depends on a particular
-- evaluation order without reference to unsafe* functions or even
-- the IO monad.
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE BangPatterns #-}
import GHC.Prim
f :: Int -> Int
f x = let v = myVar 1
-- removing the strictness in the following changes the result
!x'' = h v x
in g v x''
g :: MutVar# RealWorld Int -> Int -> Int
g v x = let !y = addMyVar v 1
in x * y
h :: MutVar# RealWorld Int -> Int -> Int
h v x = let !y = readMyVar v
in x + y
myVar :: Int -> MutVar# (RealWorld) Int
myVar x =
case newMutVar# x realWorld# of
(# _ , v #) -> v
readMyVar :: MutVar# (RealWorld) Int -> Int
readMyVar v =
case readMutVar# v realWorld# of
(# _ , x #) -> x
addMyVar :: MutVar# (RealWorld) Int -> Int -> Int
addMyVar v x =
case readMutVar# v realWorld# of
(# s , y #) ->
case writeMutVar# v (x+y) s of
s'' -> x + y
main = print $ f 1

Solo para una referencia fácil, reuní algunas de las definiciones relevantes para la mónada IO implementada por GHC. (Todas las rutas a continuación son relativas al directorio superior del repositorio de origen de ghc).

-- Firstly, according to "libraries/base/GHC/IO.hs",
{-
The IO Monad is just an instance of the ST monad, where the state is
the real world. We use the exception mechanism (in GHC.Exception) to
implement IO exceptions.
...
-}
-- And indeed in "libraries/ghc-prim/GHC/Types.hs", We have
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
-- And in "libraries/base/GHC/Base.lhs", we have the Monad instance for IO:
data RealWorld
instance Functor IO where
fmap f x = x >>= (return . f)
instance Monad IO where
m >> k = m >>= / _ -> k
return = returnIO
(>>=) = bindIO
fail s = failIO s
returnIO :: a -> IO a
returnIO x = IO $ / s -> (# s, x #)
bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO $ / s -> case m s of (# new_s, a #) -> unIO (k a) new_s
unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a
-- Many of the unsafe* functions are defined in "libraries/base/GHC/IO.hs":
unsafePerformIO :: IO a -> a
unsafePerformIO m = unsafeDupablePerformIO (noDuplicate >> m)
unsafeDupablePerformIO :: IO a -> a
unsafeDupablePerformIO (IO m) = lazy (case m realWorld# of (# _, r #) -> r)
unsafeInterleaveIO :: IO a -> IO a
unsafeInterleaveIO m = unsafeDupableInterleaveIO (noDuplicate >> m)
unsafeDupableInterleaveIO :: IO a -> IO a
unsafeDupableInterleaveIO (IO m)
= IO ( / s -> let
r = case m s of (# _, res #) -> res
in
(# s, r #))
noDuplicate :: IO ()
noDuplicate = IO $ /s -> case noDuplicate# s of s'' -> (# s'', () #)
-- The auto-generated file "libraries/ghc-prim/dist-install/build/autogen/GHC/Prim.hs"
-- list types of all the primitive impure functions. For example,
data MutVar# s a
data State# s
newMutVar# :: a -> State# s -> (# State# s,MutVar# s a #)
-- The actual implementations are found in "rts/PrimOps.cmm".

Entonces, por ejemplo, ignorando al constructor y asumiendo la transparencia referencial, tenemos

unsafeDupableInterleaveIO m >>= f
==> (let u = unsafeDupableInterleaveIO)
u m >>= f
==> (definition of (>>=) and ignore the constructor)
/s -> case u m s of
(# s'',a'' #) -> f a'' s''
==> (definition of u and let snd# x = case x of (# _,r #) -> r)
/s -> case (let r = snd# (m s)
in (# s,r #)
) of
(# s'',a'' #) -> f a'' s''
==>
/s -> let r = snd# (m s)
in
case (# s, r #) of
(# s'', a'' #) -> f a'' s''
==>
/s -> f (snd# (m s)) s

Esto no es lo que normalmente obtendríamos de unir las mónadas de estado perezoso habituales. Suponiendo que la variable de estado s tiene un significado real (que no lo hace), se parece más a una IO concurrente (o IO intercalada como la función correctamente dice) que a una IO perezosa como normalmente lo entendemos por "mónada de estado perezoso" en donde a pesar de la pereza los estados están correctamente enhebrados por una operación asociativa.

Intenté implementar una mónada de IO realmente perezosa, pero pronto me di cuenta de que para definir una composición monádica perezosa para el tipo de datos de IO, necesitamos poder levantar / liberar el Mundo Real. Sin embargo, esto parece imposible porque no hay un constructor ni para State# s ni para RealWorld . E incluso si fuera posible, tendría que representar la representación funcional y precisa de nuestro mundo real, lo cual también es imposible.

Pero todavía no estoy seguro de si el estándar Haskell 2010 rompe la transparencia referencial o si el IO perezoso es malo en sí mismo. Al menos, parece completamente posible construir un modelo pequeño de RealWorld en el que el IO perezoso sea perfectamente seguro y predecible. Y puede haber una aproximación suficientemente buena que sirva para muchos propósitos prácticos sin romper la transparencia referencial.

Answer 1

Básicamente, todo lo que aparece debajo de "Actualizar" en la pregunta está tan confundido que ni siquiera está mal, así que por favor, trate de olvidarlo cuando esté tratando de entender mi respuesta.

Mira esta función:

badLazyReadlines :: Handle -> IO [String]
badLazyReadlines h = do
l <- unsafeInterleaveIO $ hGetLine h
r <- unsafeInterleaveIO $ badLazyReadlines h
return (l:r)

Además de lo que estoy tratando de ilustrar: la función anterior tampoco permite llegar al final del archivo. Pero ignora eso por ahora.

main = do
h <- openFile "example.txt" ReadMode
lns <- badLazyReadlines h
putStrLn $ lns ! 4

Esto imprimirá la primera línea de "example.txt", porque el quinto elemento de la lista es en realidad la primera línea que se lee del archivo.

Answer 2

En la parte superior, las dos funciones que tiene son siempre idénticas.

v1 = do !a <- x
y
v2 = do !a <- unsafeInterleaveIO x
y

Recuerde que unsafeInterleaveIO difiere la operación de IO hasta que su resultado sea forzado, sin embargo, la está forzando de inmediato mediante el uso de una coincidencia estricta de patrones, por lo que la operación no se aplaza en absoluto. Así que v1 y v2 son exactamente iguales.

En general

En general, depende de usted demostrar que su uso de unsafeInterleaveIO es seguro. Si llama a unsafeInterleaveIO x , debe probar que se puede llamar a x en cualquier momento y aún así producir el mismo resultado.

Sentimiento moderno sobre Lazy IO

... es que Lazy IO es peligroso y una mala idea el 99% del tiempo.

El principal problema que está tratando de resolver es que IO se debe hacer en la mónada IO , pero desea poder realizar IO incrementales y no desea volver a escribir todas sus funciones puras para llamar a devoluciones de llamada IO para obtener mas datos La IO incremental es importante porque usa menos memoria, lo que le permite operar con conjuntos de datos que no caben en la memoria sin cambiar demasiado los algoritmos.

La solución de Lazy IO es hacer IO fuera de la mónada IO . Esto no es generalmente seguro.

Hoy en día, las personas están resolviendo el problema de la IO incremental de diferentes maneras mediante el uso de bibliotecas como Conduit o Pipes . Los conductos y tuberías son mucho más deterministas y de buen comportamiento que Lazy IO, resuelven los mismos problemas y no requieren construcciones inseguras.

Recuerde que unsafeInterleaveIO es realmente unsafePerformIO con un tipo diferente.

Ejemplo

Aquí hay un ejemplo de un programa que está roto debido a la pereza de IO:

rot13 :: Char -> Char
rot13 x
| (x >= ''a'' && x <= ''m'') || (x >= ''A'' && x <= ''M'') = toEnum (fromEnum x + 13)
| (x >= ''n'' && x <= ''z'') || (x >= ''N'' && x <= ''Z'') = toEnum (fromEnum x - 13)
| otherwise = x
rot13file :: FilePath -> IO ()
rot13file path = do
x <- readFile path
let y = map rot13 x
writeFile path y
main = rot13file "test.txt"

Este programa no funcionará. Reemplazar la IO perezosa por una IO estricta hará que funcione.

Campo de golf

From Lazy IO rompe la pureza de Oleg Kiselyov en la lista de correo de Haskell:

Demostramos cómo la perversa IO rompe la transparencia referencial Una función pura del tipo Int->Int->Int da diferentes enteros dependiendo del orden de evaluación de sus argumentos. Nuestro código Haskell98 no utiliza más que la entrada estándar. Llegamos a la conclusión de que la exaltación de la pureza de Haskell y la publicidad perezosa de IO es inconsistente.

...

Lazy IO no debe considerarse un buen estilo. Una de las definiciones comunes de pureza es que las expresiones puras deben evaluar los mismos resultados independientemente del orden de evaluación, o que los iguales pueden ser sustituidos por iguales. Si una expresión del tipo Int se evalúa como 1, deberíamos poder reemplazar cada aparición de la expresión con 1 sin cambiar los resultados y otros observables.

De Lazy vs correct IO de Oleg Kiselyov en la lista de correo de Haskell:

Después de todo, lo que podría ser más contra el espíritu de Haskell que una función "pura" con efectos secundarios observables. Con Lazy IO, uno tiene que elegir entre la corrección y el rendimiento. La aparición de dicho código es especialmente extraña después de la evidencia de interbloqueos con Lazy IO, presentada en esta lista hace menos de un mes. Sin mencionar el uso impredecible de recursos y la dependencia de los finalizadores para cerrar archivos (olvidando que GHC no garantiza que los finalizadores se ejecutarán en absoluto).

Kiselyov escribió la biblioteca Iteratee , que fue la primera alternativa real a la IO perezosa.

Answer 3

La pereza significa que cuándo (y si) se lleva a cabo exactamente un cálculo depende de cuándo (y si) la implementación del tiempo de ejecución decide que necesita el valor. Como programador de Haskell, abandonas completamente el control sobre el orden de evaluación (excepto por las dependencias de datos inherentes a tu código, y cuando comienzas a jugar con rigor para forzar el tiempo de ejecución a tomar ciertas decisiones).

Eso es genial para los cálculos puros , porque el resultado de un cálculo puro será exactamente el mismo cada vez que lo haga (excepto que si realiza cálculos que realmente no necesita, puede encontrar errores o no terminar, cuando otra evaluación el orden podría permitir que el programa termine con éxito, pero todos los valores no inferiores calculados por cualquier orden de evaluación serán los mismos).

Pero cuando escribe un código dependiente de IO, la orden de evaluación es importante . El objetivo principal de IO es proporcionar un mecanismo para construir cálculos cuyos pasos dependan y afecten el mundo fuera del programa, y ​​una parte importante de esto es que esos pasos están explícitamente secuenciados. El uso de unsafeInterleaveIO descarta esa secuencia explícita y renuncia al control de cuándo (y si) la operación de IO se lleva a cabo realmente en el sistema de tiempo de ejecución.

Esto no es seguro en general para las operaciones de E / S, ya que puede haber dependencias entre sus efectos secundarios que no pueden deducirse de las dependencias de datos dentro del programa. Por ejemplo, una acción de IO puede crear un archivo con algunos datos y otra acción de IO puede leer el mismo archivo. Si ambos se ejecutan "perezosamente", entonces solo se ejecutarán cuando se necesite el valor de Haskell resultante. Sin embargo, la creación del archivo es probablemente IO () , y es muy posible que nunca se necesite el () . Eso podría significar que la operación de lectura se realiza primero, ya sea fallando o leyendo datos que ya estaban en el archivo, pero no los datos que la otra operación debería haber colocado allí. No hay garantía de que el sistema de ejecución los ejecute en el orden correcto. Para programar correctamente con un sistema que siempre hizo esto para IO , tendría que poder predecir con precisión el orden en que el tiempo de ejecución de Haskell elegirá para realizar las diversas acciones de IO .

Considere a unsafeInterlaveIO como una promesa para el compilador (que no puede verificar, solo va a confiar en usted) que no importa cuándo se lleva a cabo la acción IO , o si se elimina por completo. Esto es realmente lo que son todas las funciones unsafe* ; proporcionan instalaciones que no son seguras en general, y para las cuales la seguridad no puede verificarse automáticamente, pero puede ser segura en casos particulares. La responsabilidad recae en usted para garantizar que su uso de ellos sea, de hecho, seguro. Pero si haces una promesa al compilador, y tu promesa es falsa, el resultado puede ser un error desagradable. El "inseguro" en el nombre es asustarlo para que piense en su caso particular y decida si realmente puede prometerlo al compilador.

Answer 4

Su joinIO y joinIO'' no son semánticamente equivalentes. Por lo general, serán iguales, pero hay una sutileza involucrada: un patrón explosivo hace que un valor sea estricto, pero eso es todo lo que hace. Los patrones de explosión se implementan utilizando seq , y eso no impone un orden de evaluación en particular, en particular los siguientes dos son semánticamente equivalentes:

a `seq` b `seq` c
b `seq` a `seq` c

GHC puede evaluar una b o una primera antes de regresar c. De hecho, puede evaluar c primero, luego a y b, luego devolver c. O, si puede probar estáticamente que a o b no tienen fondo, o que c es inferior, no tiene que evaluar a o b en absoluto. Algunas optimizaciones hacen uso genuino de este hecho, pero no aparece muy a menudo en la práctica.

unsafeInterleaveIO , por el contrario, es sensible a todos o cualquiera de esos cambios, no depende de la propiedad semántica de cuán estricta es la función, sino de la propiedad operacional de cuando se evalúa algo. Por lo tanto, todas las transformaciones anteriores son visibles para él, por lo que es razonable considerar que unsafeInterleaveIO realiza su IO de forma no determinista, más o menos siempre que se considere apropiado.

Esto es, en esencia, la razón por la que unsafeInterleaveIO no es seguro: es el único mecanismo en el uso normal que puede detectar transformaciones que deberían preservar el significado. Es la única forma en que puede detectar la evaluación, lo que por derechos debería ser imposible.

Dejando de lado, es probable que sea justo anteponer mentalmente unsafe a cada función de GHC.Prim , y probablemente a varios otros GHC. módulos también. Ciertamente no son ordinarios Haskell.