¿Cómo funciona la mónada ST?

Question

Entiendo que la mónada ST es algo así como un hermano pequeño de IO, que a su vez es la mónada estatal con RealWorld magia añadida. Puedo imaginar los estados y puedo imaginar que RealWorld está de alguna manera puesto en IO, pero cada vez que escribo una firma tipo de ST, el s de la mónada ST me confunde.

Tome, por ejemplo, ST s (STArray s a b). ¿Cómo funciona el s allí? ¿Se usa solo para crear una dependencia de datos artificiales entre cálculos sin que se pueda hacer referencia a ellos como estados en la mónada de estado (debido al forall)?

Estoy tirando ideas y realmente agradecería a alguien más entendido que yo que me lo explique.

Answer 1

El s mantiene objetos dentro de la mónada ST de la fuga hacia el exterior de la mónada ST.

-- This is an error... but let's pretend for a moment... 
let a = runST $ newSTRef (15 :: Int) 
    b = runST $ writeSTRef a 20 
    c = runST $ readSTRef a 
in b `seq` c 

Bueno, esto es un error de tipo (que es una buena cosa! No queremos STRef a filtrarse fuera del cálculo original!). Es un error de tipo debido al extra s. Recuerde que runST tiene la firma:

runST :: (forall s . ST s a) -> a 

Esto significa que el s en la computación que se está ejecutando tiene que tener ninguna restricción sobre el mismo. Así que cuando se trata de evaluar a:

a = runST (newSTRef (15 :: Int) :: forall s. ST s (STRef s Int)) 

El resultado tendría STRef s Int tipo, que es un error ya que el s ha "escapado" fuera de la forall en runST. Las variables de tipo siempre tienen que aparecer en el interior de forall, y Haskell permite cuantificadores implícitos forall en todas partes. Simplemente no existe una regla que le permita descubrir de manera significativa el tipo de devolución de a.

Otro ejemplo con forall: para mostrar claramente por qué no se puede permitir que las cosas escapan un forall, aquí es un ejemplo más simple:

f :: (forall a. [a] -> b) -> Bool -> b 
f g flag = 
    if flag 
    then g "abcd" 
    else g [1,2] 

> :t f length 
f length :: Bool -> Int 

> :t f id 
-- error -- 

Por supuesto f id es un error, ya que volvería una lista de Char o una lista de Int dependiendo de si el valor booleano es verdadero o falso. Simplemente está mal, al igual que en el ejemplo con ST.

Por otro lado, si no tiene el parámetro de tipo s, entonces todo lo que se escribe es correcto, aunque el código es obviamente bastante falso.

¿Cómo funciona realmente ST: Implementación-sabio, el ST mónada es en realidad el mismo que el IO mónada pero con una interfaz ligeramente diferente. Cuando utiliza la mónada ST en realidad obtiene unsafePerformIO o su equivalente, detrás de las escenas. La razón por la que puede hacerlo de manera segura es por la firma de tipo de todas las funciones relacionadas con ST, especialmente la parte con forall.

Answer 2

El s es solo un truco que hace que el sistema de tipo te detenga haciendo cosas que no serían seguras. No "hace" nada en tiempo de ejecución; simplemente hace que el verificador de tipos rechace programas que hacen cosas dudosas. (Es un tipo phantom, una cosa solo existe en la cabeza del corrector de tipos, y no afecta nada en tiempo de ejecución.)