haskell - monadas - ¿Es operacional realmente isomorfo a una mónada libre?
monadas leibniz (3)
(Permítame obtener el gran premio combinando audazmente las respuestas anteriores ;-))
La observación clave es esta: ¿ Probar qué exactamente ? La formulación en términos de Free TeletypeF
nos permite probar lo siguiente:
Cada intérprete para programas de tipo
Free TeletypeF a
debe salir cuando encuentra la instrucciónExitSuccess
. En otras palabras, obtenemos automáticamente la ley algebraica.
interpret (exitSuccess >>= k) = interpret exitSuccess
Por lo tanto, la mónada Free
realidad le permite hornear ciertas leyes algebraicas en el tipo.
En contraste, el enfoque operacional no restringe la semántica de ExitSuccess
, no hay una ley algebraica asociada que pertenezca a cada intérprete. Es posible escribir intérpretes que salen cuando se encuentra con esta instrucción, pero también es posible escribir intérpretes que no lo hacen.
Por supuesto, puede probar que cualquier intérprete en particular cumple con la ley mediante inspección, por ejemplo, porque utiliza una coincidencia de patrón de comodín. Sjoerd Visscher observa que también puede imponer esto en el sistema de tipos cambiando el tipo de retorno de ExitSuccess
a Void
. Sin embargo, esto no funciona para otras leyes que se pueden convertir en mónadas libres, por ejemplo, la ley distributiva para la instrucción mplus
.
Por lo tanto, en un giro confuso de los acontecimientos, el enfoque operacional es más libre que la mónada libre, si interpreta "libre" como "la menor cantidad de leyes algebraicas".
También significa que estos tipos de datos no son isomorfos. Sin embargo, son equivalentes: cada intérprete escrito con Free
puede transformarse en un intérprete escrito con Program
y viceversa.
Personalmente, me gusta poner todas mis leyes en el intérprete, porque hay muchas leyes que no se pueden incluir en la mónada gratuita, y me gusta tenerlas todas en un solo lugar.
Pruebas
En this publicación del blog, Tekmo señala que podemos probar que ExitSuccess
sale porque (supongo) es como el functor Const
de ese constructor (no lleva la x
por lo que fmap
comporta como const
).
Con el paquete operativo, el TeletypeF
de Tekmo podría traducirse de la siguiente manera:
data TeletypeI a where
PutStrLn :: String -> TeletypeI ()
GetLine :: TeletypeI String
ExitSuccess :: TeletypeI ()
He leído que operacional es isomorfo a una mónada libre, pero ¿podemos probar aquí que ExitSuccess
sale? Me parece que tiene exactamente el mismo problema que exitSuccess :: IO ()
, y en particular, si escribiéramos un intérprete, tendríamos que escribirlo como si no hubiera salido:
eval (ExitSuccess :>>= _) = exitSuccess
Compare con la versión de mónada gratuita que no implica ningún patrón comodín:
run (Free ExitSuccess) = exitSuccess
pereza
En el Tutorial de Monada Operacional, apfelmus menciona un inconveniente:
La mónada estatal representada como s -> (a, s) puede hacer frente a algunos programas infinitos como
evalState (sequence . repeat . state $ /s -> (s,s+1)) 0
mientras que el enfoque de la lista de instrucciones no tiene ninguna esperanza de manejar eso, ya que solo la última instrucción de retorno puede devolver valores.
¿Es esto cierto también para las mónadas gratuitas?
La respuesta es no, no puede probar que el operativo ignora el resto del programa en exitSuccess
. Contrastar TeletypeI
con TeletypeF
para ver por qué. Reescribiré TeletypeF
en notación GADT para una comparación más fácil
data TeletypeF x where | data TeletypeI x where
PutStrLn :: String -> x -> TeletypeF x | PutStrLn :: String -> TeletypeI ()
GetLine :: (String -> x) -> TeletypeF x | GetLine :: TeletypeI String
ExitSuccess :: TeletypeF x | ExitSuccess :: TeletypeI ()
Usando TeletypeF
, podemos construir programas reales de inmediato:
GetLine (/str -> PutStrLn (map toUpper str) ExitSuccess)
TeletypeI
no viene con una forma de referirse al "resto del programa" de la misma manera que TeletypeF
.
-- TeletypeF:
GetLine (/str -> "rest of program" goes here)
-- or
PutStrLn someString ("rest of program" goes here)
-- or
ExitSuccess -- there is no "rest of program" slot provided
Como TeletypeI
carece de esta información del "resto del programa", ya no puede obtener ningún conocimiento cuando se encuentre con ExitSuccess
.
-- TeletypeI
PutStrLn someString -- no information about "rest of program"
-- or
GetLine -- no information about "rest of program"
-- or
ExitSuccess -- no information about "rest of program"
Lo que está permitido venir como "resto del programa" depende completamente del tipo de Program
, que no sabe nada sobre el conjunto de instrucciones al que se está aplicando. Simplemente le permite enlazar instrucciones y terminar a través de Return
.
La respuesta es sí, pero solo si usa una traducción diferente de TeletypeF
:
data TeletypeI a where
PutStrLn :: String -> TeletypeI ()
GetLine :: TeletypeI String
ExitSuccess :: TeletypeI Void
El argumento de TeletypeI
es lo que la operación debe proporcionar al resto del programa. Es el tipo del argumento de la continuación k
en.
eval (ExitSuccess :>>= k) = ...
Como no hay valores de tipo Void
, podemos estar seguros de que nunca se llamará a k
. (Como siempre tendremos que ignorar undefined
aquí).
Un tipo equivalente es:
data TeletypeI a where
PutStrLn :: String -> TeletypeI ()
GetLine :: TeletypeI String
ExitSuccess :: TeletypeI a
Ahora tendríamos que proporcionar un valor a k
que coincida con cualquier tipo, y tampoco podemos hacer eso. Esto puede ser más práctico ya que singleton ExitSuccess
ahora tiene el tipo flexible Program TeletypeI a
.
De manera similar, exitSuccess
podría arreglar dándole el tipo IO Void
, o IO a
.