haskell - monadas - ¿Es operacional realmente isomorfo a una mónada libre?

monadas leibniz

Question

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?

Answer 1

(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ón ExitSuccess . 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.

Answer 2

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 .

Answer 3

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 .