haskell - racionalismo - leibniz youtube

¿Hay una mónada que no tenga un transformador de mónada correspondiente(excepto IO)?

Question

Hasta ahora, cada mónada (que puede representarse como un tipo de datos) que he encontrado tenía un transformador de mónada correspondiente, o podría tener uno. ¿Hay tal mónada que no puede tener una? ¿O todas las mónadas tienen un transformador correspondiente?

Por un transformador t correspondiente a la mónada m quiero decir que t Identity es isomorfa a m . Y, por supuesto, que satisface las leyes del transformador de mónada y que tn es una mónada para cualquier mónada n .

Me gustaría ver una prueba (idealmente constructiva) de que cada mónada tiene una, o un ejemplo de una mónada particular que no tiene una (con una prueba). Me interesan tanto las respuestas más orientadas a Haskell, como las teóricas (de categoría).

Como pregunta de seguimiento, ¿hay una mónada que tenga dos transformadores distintos t1 y t2 ? Es decir, t1 Identity es isomorfa a t2 Identity y a m , pero hay una mónada n tal que t1 n no es isomorfo a t2 n .

( IO y ST tienen una semántica especial, así que no los tomo en cuenta aquí y los descartamos por completo. Centrémonos únicamente en las mónadas "puras" que se pueden construir utilizando tipos de datos).

Answer 1

Aquí hay una respuesta ondulada de la mano que no estoy del todo segura.

Se puede pensar que las mónadas son la interfaz de los lenguajes imperativos. return es cómo inyectas un valor puro en el lenguaje, y >>= es cómo empalmes partes del lenguaje. Las leyes de Monad garantizan que las piezas de "refactorización" del lenguaje funcionen de la manera que usted esperaría. Cualquier acción adicional proporcionada por una mónada puede considerarse como sus "operaciones".

Los transformadores de mónada son una forma de abordar el problema de los "efectos extensibles". Si tenemos un Monad Transformer t que transforma una Monad m , entonces podríamos decir que el idioma m se está ampliando con operaciones adicionales disponibles a través de t . La mónada de Identity es el idioma sin efectos / operaciones, por lo que si aplica t a Identity obtendrá un idioma con solo las operaciones proporcionadas por t .

Entonces, si pensamos en las Mónadas en términos del modelo de "inyección, empalme y otras operaciones", entonces podemos simplemente reformularlas usando el Transformador de Mónada Libre. Incluso la mónada IO podría convertirse en un transformador de esta manera. La única pega es que probablemente quieras quitar esa capa de la pila de transformadores en algún momento, y la única manera sensata de hacerlo es si tienes IO en la parte inferior de la pila para que puedas realizar las operaciones allí. .

Answer 2

Estoy con @Rhymoid en este caso, creo que todas las Mónadas tienen dos (!!) transformadores. Mi construcción es un poco diferente, y mucho menos completa. Me gustaría poder tomar este boceto como una prueba, pero creo que me faltan las habilidades / intuición y / o puede ser bastante complicado.

Debido a Kleisli, cada mónada ( m ) puede descomponerse en dos funtores F_k y G_k modo que F_k quede adjunto a G_k y que m sea ​​isomorfo a G_k * F_k (aquí * es la composición del functor). Además, debido a la adjunción, F_k * G_k forma una comonad.

Yo afirmo que t_mk define de manera tal que t_mk n = G_k * n * F_k es un transformador de mónada. Claramente, t_mk Id = G_k * Id * F_k = G_k * F_k = m . Definir el return para este funtor no es difícil ya que F_k es un funtor "puntiagudo", y la join definición debería ser posible ya que el extract de la comadrona F_k * G_k puede usarse para reducir los valores de tipo (t_mk n * t_mk n) a = (G_k * n * F_k * G_k * n * F_k) a a los valores de tipo G_k * n * n * F_k , que luego se reduce mediante la join desde n .

Tenemos que ser un poco cuidadosos ya que F_k y G_k no son endofunctors en Hask. Por lo tanto, no son instancias de la clase de tipo Functor estándar, y tampoco se pueden componer directamente con n como se muestra arriba. En cambio, tenemos que "proyectar" n en la categoría de Kleisli antes de la composición, pero creo que el return de m proporciona esa "proyección".

Creo que también puedes hacer esto con la descomposición de la mónada Eilenberg-Moore, dando m = G_em * F_em , tm_em n = G_em * n * F_em , y construcciones similares para lift , return y join con una dependencia similar al extract de la comonad F_em * G_em .

Answer 3

Mi solución explota la estructura lógica de los términos de Haskell. Todo el mundo sabe que una función en Haskell con el tipo de retorno t se puede convertir en una función monádica con el tipo de retorno (Monad m) => m t. Por lo tanto, si la función "vincular" pudiera tener su texto de programa "monadificado" apropiadamente, el resultado sería un transformador de mónada.

El punto de fricción es que no hay ninguna razón por la cual la "monadificación" del operador de "enlace" deba satisfacer las leyes, particularmente la asociatividad. Aquí es donde entra en juego la eliminación de corte. El teorema de eliminación de corte tiene el efecto en un texto de programa que incluye todos los enlaces de liberación, análisis de casos y aplicaciones. Además, todos los cálculos sobre un término en particular terminan siendo realizados en un solo lugar.

Dado que los parámetros de tipo "bind" son rígidos, los usos del lado derecho de "bind" están indexados por sus valores de retorno. Los términos terminan en posiciones en la estructura devuelta que hacen que el "enlace" se asocie, por lo tanto, los usos del lado derecho deben ser asociativos en el "enlace" "monadificado", y la estructura resultante es una mónada.

Esto es realmente lanoso, así que aquí hay un ejemplo. Considere la siguiente mónada de lista estricta:

rseq x y = case x of
    x:xs -> (x:xs) : y
    [] -> [] : y


evalList (x:xs) = rseq x (evalList xs)
evalList [] = []

instance Monad [] where
    return x = [x]
    ls >>= f = concat (evalList (map f ls))

Este orden de evaluación conduce al ListT estándar (en realidad no es una mónada). Sin embargo, por eliminación de corte:

instance Monad [] where
    return x = [x]
    ls >>= f = case ls of
        [] -> []
        x:xs -> case f x of
            y:ys -> (y:ys) ++ (xs >>= f)
            [] -> [] ++ (xs >>= f)

Esto proporciona la orden de evaluación exacta para ser "monadificado".

En respuesta a Petr Pudlak:

Si el tipo de la mónada en cuestión es de algún tipo de función (es conveniente que Church-encode todos los tipos de datos), el tipo de función se convierte decorando todos los valores devueltos del tipo con la mónada transformada. Esta es la porción de tipo de monadificación. La porción de valor de monadificación levanta funciones puras usando "retorno" y las combina con usos de habitantes del tipo de mónada utilizando "vincular", preservando el orden de evaluación del texto de programa original.

La lista estricta de mónada se proporcionó como ejemplo de una orden de evaluación que no se compone asociativamente, como lo demuestra el hecho de que ListT utiliza el mismo orden de evaluación que la lista estricta de mónada.

Para completar el ejemplo, la codificación de la Iglesia de la lista de la mónada es:

data List a = List (forall b. b -> (a -> List a -> b) -> b)

Monadificado, se convierte en:

data ListT m a = ListT (forall b. m b -> (a -> List a -> m b) -> m b)

cons x xs = /_ f -> f x xs

nil = /x _ -> x

instance (Monad m) => Monad (ListT m) where
    return x = cons x nil
    ls >>= f = ls nil (/x xs -> f x >>= /g ->
        g (liftM (nil ++) (xs >>= f)) (/y ys -> liftM (cons y ys ++) (xs >>= f))

Para profundizar en lo anterior, el paso de eliminación de corte obliga a consumir todos los valores utilizando una disciplina de pila, asegurando que el orden de los resultados en la estructura coincida con el orden de evaluación, esto tiene el precio de ejecutar potencialmente la misma acción muchas veces.

[Técnicamente, lo que necesita es una eliminación de corte de los aproximantes: A es una eliminación de corte (de los aproximantes) de B, si f para cada aproximada finita de B, hay un aproximante finito de A tal que A es una eliminación de corte de B. ]

Espero que eso ayude.