¿Cómo y por qué funciona la mónada Haskell Cont?

Question

Esto es cómo se define la mónada Cont:

newtype Cont r a = Cont { runCont :: (a -> r) -> r } 

instance Monad (Cont r) where 
    return a = Cont ($ a) 
    m >>= k = Cont $ \c -> runCont m $ \a -> runCont (k a) c 

Podría explicar cómo y por qué esto funciona? ¿Qué está haciendo?

Answer 1

Lo primero que debe saber acerca de la mónada de continuación es que, fundamentalmente, no es realmente haciendo nada en absoluto. ¡Es verdad!

La idea básica de una continuación, en general, es que representa el resto de un cálculo. Digamos que tenemos una expresión como esta: foo (bar x y) z. Ahora, extraiga solo la parte entre paréntesis, bar x y --esto es parte de la expresión total, pero no es solo una función que podemos aplicar. En cambio, es algo que necesitamos para aplicar una función a. Entonces, podemos hablar del "resto del cálculo" en este caso como \a -> foo a z, que podemos aplicar al bar x y para reconstruir el formulario completo.

Ahora, sucede que este concepto de "el resto de la computación" es útil, pero es incómodo trabajar con él, ya que es algo fuera de la subexpresión que estamos considerando. Para que las cosas funcionen mejor, podemos cambiar las cosas al revés: extraemos la subexpresión que nos interesa y luego la envolvemos en una función que toma un argumento que representa el resto del cálculo: \k -> k (bar x y).

Esta versión modificada nos da mucha flexibilidad, no solo extrae una subexpresión de su contexto, sino que nos permite manipular ese contexto externo dentro de la subexpresión misma. Podemos considerarlo como una especie de cómputo suspendido, que nos da un control explícito sobre lo que sucede a continuación. Ahora, ¿cómo podríamos generalizar esto? Bueno, la subexpresión prácticamente no se modifica, así que simplemente reemplácela con un parámetro para la función de adentro hacia afuera, dándonos \x k -> k x --en otras palabras, nada más que la aplicación de función , invertida. Podríamos simplemente escribir flip ($), o agregar un poco de un sabor de idioma extranjero exótico y definirlo como un operador |>.

Ahora, sería simple, aunque tedioso y horriblemente ofuscante, traducir cada parte de una expresión a esta forma. Afortunadamente, hay una mejor manera. Como programadores de Haskell, cuando pensamos en construyendo un cálculo dentro de un contexto de contexto, lo siguiente que pensamos es decir, ¿es esto una mónada? Y en este caso la respuesta es sí, sí lo es.

de convertir esto en una mónada, comenzamos con dos bloques de construcción básicos:

• Para una mónada m, un valor de tipo m a representa tener acceso a un valor de tipo a en el contexto de la mónada .
• El núcleo de nuestros "cálculos suspendidos" es la aplicación de función volteada.

¿Qué significa tener acceso a algo del tipo a dentro de este contexto?Simplemente significa que, para algún valor x :: a, hemos aplicado flip ($) a x, dándonos una función que toma una función que toma un argumento del tipo a, y aplica esa función a x. Digamos que tenemos un cálculo suspendido que contiene un valor de tipo Bool. ¿Qué tipo nos da esto?

> :t flip ($) True 
flip ($) True :: (Bool -> b) -> b 

Así que para los cálculos en suspensión, el tipo m a se resuelve a (a -> b) -> b ... que es tal vez una decepción, puesto que ya se sabía la firma de Cont, pero sígueme por ahora.

Una cosa interesante a destacar aquí es que una especie de "inversión" también se aplica al tipo del mismo mónada: Cont b a representa una función que toma una función a -> b y evalúa a b. Como una continuación representa "el futuro" de un cálculo, entonces el tipo a en la firma representa en cierto sentido "el pasado".

Entonces, reemplazando (a -> b) -> b con Cont b a, ¿cuál es el tipo monádico para nuestra aplicación básica de bloque de construcción de función inversa? a -> (a -> b) -> b se traduce en a -> Cont b a ... el mismo tipo de firma como return y, de hecho, eso es exactamente lo que es.

A partir de ahora, todo se cae directamente de los tipos: esencialmente no hay una forma sensata de implementar >>= además de la implementación real. ¿Pero qué es realmente haciendo?

En este punto volvemos a lo que dije inicialmente: la mónada de continuación no es realmente haciendo mucho más. Algo del tipo Cont r a es trivialmente equivalente a algo del tipo a, simplemente suministrando id como argumento para el cálculo suspendido. Esto podría llevar a preguntarse si, en caso Cont r a es una monada, pero la conversión es tan trivial, no debería a sola también ser una mónada? Por supuesto, eso no funciona como está, ya que no hay un constructor de tipos para definir como una instancia de Monad, pero digamos que agregamos un contenedor trivial, como data Id a = Id a. Esto es de hecho una mónada, a saber, la mónada de identidad.

¿Qué hace >>= para la mónada identidad? La firma de tipo es Id a -> (a -> Id b) -> Id b, que es equivalente a a -> (a -> b) -> b, que es simplemente una aplicación de función simple otra vez. Una vez establecido que Cont r a es trivialmente equivalentes a Id a, se puede deducir que en este caso también, (>>=) es la aplicación simplemente función.

Por supuesto, Cont r a es un mundo invertido loca donde todo el mundo tiene barbas de chivo, así que lo que realmente sucede implica cosas arrastrando los pies alrededor de formas confusas con el fin de cálculos cadena de dos suspendidos juntos en un nuevo cómputo suspendido, pero en esencia, no ISN ¡En realidad no pasa nada inusual! Aplicando funciones a argumentos, ho hum, otro día en la vida de un programador funcional.

Answer 2

EDITAR: Artículo migrado al siguiente enlace.

He escrito un tutorial abordar directamente este tema que espero que sean de utilidad. (¡Ciertamente me ayudó a consolidar mi comprensión!) Es demasiado largo para encajar cómodamente en un tema de Desbordamiento de pila, así que lo migré al Wiki de Haskell.

favor ver: MonadCont under the hood

Answer 3

Aquí está Fibonacci:

fib 0 = 0 
fib 1 = 1 
fib n = fib (n-1) + fib (n-2) 

Imagine que tiene una máquina sin una pila de llamadas - que sólo permite la recursión de cola. ¿Cómo ejecutar fib en esa máquina? Podría reescribir fácilmente la función para que funcione en tiempo lineal, en lugar de exponencial, pero eso requiere un poco de conocimiento y no es mecánico.

El obstáculo para lo que es recursivo de cola es la tercera línea, donde hay dos llamadas recursivas. Solo podemos hacer una sola llamada, que también debe dar el resultado. Aquí es donde entran las continuaciones.

Vamos a hacer fib (n-1) tomar el parámetro adicional, que será una función que especifica lo que se debe hacer después de calcular su resultado, llámelo x. Agregará , por supuesto. Entonces: para calcular fib n, calcule fib (n-1) después de eso, si llama al resultado x, calcule , después de eso, si llama al resultado y, devuelve x+y.

En otras palabras, usted tiene que decir:

cómo hacer el cálculo siguiente: "fib' n c = fib n calcular y aplicar c al resultado"?

La respuesta es que hace lo siguiente: "calcular y aplicar fib (n-1)d al resultado", donde d x significa "calcular y aplicar e al resultado", donde e y significa c (x+y). En código:

fib' 0 c = c 0 
fib' 1 c = c 1 
fib' n c = fib' (n-1) d 
      where d x = fib' (n-2) e 
       where e y = c (x+y) 

De manera equivalente, podemos utilizar lambdas:

fib' 0 = \c -> c 0 
fib' 1 = \c -> c 1 
fib' n = \c -> fib' (n-1) $ \x -> 
       fib' (n-2) $ \y -> 
       c (x+y) 

Para obtener la identidad real de uso de Fibonacci: fib' n id. Puede pensar que la línea fib (n-1) $ ... pasa su resultado x al siguiente.

las tres últimas líneas huelen como un bloque do, y de hecho

fib' 0 = return 0 
fib' 1 = return 1 
fib' n = do x <- fib' (n-1) 
      y <- fib' (n-2) 
      return (x+y) 

es el mismo, hasta Newtypes, por definición de mónada Cont. Note las diferencias. Hay \c -> al principio, en lugar de x <- ... hay ... $ \x -> y en lugar de creturn.

intentar escribir en un estilo factorial n = n * factorial (n-1) recursiva cola utilizando CPS.

¿Cómo >>= trabajo?m >>= k es equivalente a

do a <- m 
    t <- k a 
    return t 

Hacer la traducción inversa, en el mismo estilo que en fib', se obtiene

\c -> m $ \a -> 
     k a $ \t -> 
     c t 

simplificar \t -> c t a c

m >>= k = \c -> m $ \a -> k a c 

Newtypes Agregando a obtener

m >>= k = Cont $ \c -> runCont m $ \a -> runCont (k a) c 

que se encuentra en la parte superior de esta página. Es complejo, pero si usted sabe cómo traducir entre la notación do y el uso directo, ¡no necesita saber la definición exacta de >>=! La mónada de continuación es mucho más clara si observas bloqueos.

Mónadas y continuaciones

Si nos fijamos en este uso de la mónada lista ...

do x <- [10, 20] 
    y <- [3,5] 
    return (x+y) 

[10,20] >>= \x -> 
    [3,5] >>= \y -> 
    return (x+y) 

([10,20] >>=) $ \x -> 
    ([3,5] >>=) $ \y -> 
    return (x+y) 

que se parece a continuación! De hecho, (>> =) cuando aplica un argumento tiene el tipo (a -> m b) -> m b que es Cont (m b) a. Vea sigfpe's Mother of all monads para una explicación. Lo consideraría un buen tutorial de continuación de mónadas, aunque probablemente no era así.

Como las continuidades y las mónadas están tan fuertemente relacionadas en ambas direcciones, creo que lo que se aplica a las mónadas se aplica a las continuaciones: solo el trabajo duro se las enseñará y no leerá una metáfora o analogía de burrito.

Answer 4

Creo que la manera más fácil de obtener un control sobre la mónada Cont es entender cómo usar su constructor. Voy a asumir la siguiente definición por el momento, a pesar de las realidades del paquete transformers son ligeramente diferentes:

newtype Cont r a = Cont { runCont :: (a -> r) -> r } 

Esto da:

Cont :: ((a -> r) -> r) -> Cont r a 

manera de construir un valor de tipo Cont r a, nos que tenga que dar una función a Cont:

value = Cont $ \k -> ... 

Ahora, k en sí tiene el tipo a -> r, y el cuerpo de la lambda debe tener el tipo r. Una cosa obvia que hacer sería aplicar k a un valor de tipo a, y obtener un valor de tipo r. Podemos hacer eso, sí, pero esa es realmente una de las muchas cosas que podemos hacer. Recuerde que value no necesita ser polimórfico en r, podría ser del tipo Cont String Integer u otra cosa concreta. Por lo tanto:

• Podríamos aplicar k a varios valores de tipo a, y combinar los resultados de alguna manera.
• Podríamos aplicar k a un valor de tipo a, observar el resultado, y luego decidir aplicar k a otra cosa en función de eso.
• Podríamos ignorar k en conjunto y solo producir un valor de tipo r nosotros mismos.

Pero, ¿qué significa todo esto? ¿Qué es k? Pues bien, en un do-bloque, podríamos tener algo parecido a esto:

flip runCont id $ do 
    v <- thing1 
    thing2 v 
    x <- Cont $ \k -> ... 
    thing3 x 
    thing4 

Aquí está la parte divertida: podemos, en nuestra mente y algo de manera informal, dividir el do-bloque en dos en la ocurrencia de la Cont constructor, y piense en el resto del cómputo completo después de como un valor en sí mismo. Pero espera, lo que es depende de lo x es, por lo que es realmente una funcióndesde un valor x de tipo a a algún valor resultado:

restOfTheComputation x = do 
    thing3 x 
    thing4 

De hecho, este restOfTheComputation es en términos generales lo k termina siendo. En otras palabras, llama al k con un valor que se convierte en el resultado de su cálculo Cont, el resto del cálculo se ejecuta y luego el r producido vuelve a su lambda como resultado de la llamada al k. Por lo tanto:

• si llama k varias veces, el resto de la computación conseguirá ejecutar varias veces, y los resultados pueden ser combinados como desee.
• si no llamó al k en absoluto, el resto del cómputo completo se omitirá, y la llamada runCont adjunta le devolverá cualquier valor de tipo r que haya logrado sintetizar. Es decir, a menos que alguna otra parte del cálculo que está llamando de su k, y perder el tiempo con el resultado ...

Si todavía estás conmigo en este punto que debe ser fácil ver esto podría ser bastante poderoso. Para aclarar un poco, implementemos algunas clases de tipos estándar.

instance Functor (Cont r) where 
    fmap f (Cont c) = Cont $ \k -> ... 

se nos da un valor Cont con resultado se unen x de tipo a, y una función de f :: a -> b, y queremos hacer un valor Cont con resultado se unen f x de tipo b. Pues bien, para establecer el resultado se unen, simplemente llame k ...

fmap f (Cont c) = Cont $ \k -> k (f ... 

Espera, ¿de dónde sacamos x de? Bueno, implicará c, que aún no hemos utilizado. Recuerde cómo funciona c: se le asigna una función y luego llama a esa función con su resultado de enlace. Queremos llamar al nuestra función con f aplicado a ese resultado de vinculación. Entonces:

fmap f (Cont c) = Cont $ \k -> c (\x -> k (f x)) 

Tada!El siguiente, Applicative:

instance Applicative (Cont r) where 
    pure x = Cont $ \k -> ... 

de este sencillo. Queremos que el resultado del enlace sea el x que obtenemos.

pure x = Cont $ \k -> k x 

Ahora, <*>:

Cont cf <*> Cont cx = Cont $ \k -> ... 

Esta un poco más difícil, pero utiliza esencialmente las mismas ideas que en fmap: en primer lugar obtener la función de la primera Cont, haciendo una lambda en esta una llamada :

Cont cf <*> Cont cx = Cont $ \k -> cf (\fn -> ... 

a continuación, obtener el valor x de la segunda, y crea fn x el resultado aprieto:

Cont cf <*> Cont cx = Cont $ \k -> cf (\fn -> cx (\x -> k (fn x))) 

Monad es lo mismo, aunque requiere runCont o un caso o dejar que desempaquetar el newtype.

Esta respuesta ya es bastante larga, así que no entraré en ContT (en resumen: ¡es exactamente lo mismo que Cont! La única diferencia está en el tipo de constructor de tipos, las implementaciones de todo son idénticas) o callCC (un útil combinador que proporciona una manera conveniente de ignorar k, implementando la salida anticipada de un subbloque).

Para una aplicación simple y plausible, prueba la publicación de blog de Edward Z. Yang implementando labelled break and continue in for loops.