haskell - quiere - neo monadología

¿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 magia RealWorld añadida. Puedo imaginar estados y puedo imaginar que RealWorld está de alguna manera puesto en IO, pero cada vez que escribo una firma ST de ST la s de la mónada ST me confunde.

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

Solo lanzo ideas y realmente agradecería que alguien más conocedor que yo me lo explique.

Answer 1

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 el llamado tipo fantasma , una cosa que solo existe en la cabeza del verificador de tipos, y que no afecta nada en el tiempo de ejecución).

Answer 2

La s mantiene los objetos dentro de la mónada ST para que se filtren 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

De acuerdo, este es un error de tipo (¡lo cual es bueno! ¡No queremos que STRef filtre fuera del cálculo original!). Es un error de tipo debido a los s adicionales. Recuerde que runST tiene la firma:

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

Esto significa que la s en el cálculo que está ejecutando no debe tener restricciones. Entonces cuando intentas evaluar a :

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

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

Otro ejemplo con forall : para mostrar claramente por qué no se puede permitir que las cosas escapen de un forall , aquí hay 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 devolvería una lista de Char o una lista de Int dependiendo de si el booleano es verdadero o falso. Simplemente está mal, al igual que el ejemplo con ST .

Por otro lado, si no tuvieras el parámetro tipo s , entonces todo tipo de verificación sería correcto, aunque el código obviamente es bastante falso.

Cómo funciona realmente el ST: En términos de implementación, la mónada ST es en realidad la misma que la mónima IO pero con una interfaz ligeramente diferente. Cuando usas la mónada ST , obtienes unsafePerformIO o su equivalente, detrás de las escenas. La razón por la que puede hacer esto de manera segura es debido a la firma de tipo de todas las funciones relacionadas con ST , especialmente la parte con el forall .