haskell - ¿Cómo hacer que callCC sea más dinámico?

continuations

Question

Pensé que el tipo correcto para ContT debería ser

newtype ContT m a = ContT {runContT :: forall r. (a -> m r) -> m r}

y otros operadores de control

shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
reset :: Monad m => ContT m a -> ContT m a
callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a

Desafortunadamente, no puedo hacer callCC verificación de tipo callCC , y no sé cómo hacerlo. Me las arreglé para hacer shift y reset tipo de verificación

reset :: Monad m => ContT m a -> ContT m a
reset e = ContT $ / k -> runContT e return >>= k

shift :: Monad m => (forall r. (a -> ContT m r) -> ContT m r) -> ContT m a
shift e = ContT $ / (k :: a -> m r) ->
    runContT ((e $ / v -> ContT $ /c -> k v >>= c) :: ContT m r) return

pero aún así, ¿no puedo usar el shift y reset en saltos recursivos como este?

newtype H r m = H (H r m -> ContT m r)

unH (H x) = x

test = flip runContT return $ reset $ do
    jump <- shift (/f -> f (H f))
    lift . print $ "hello"
    unH jump jump

¿Alguien ha intentado esto antes?

Answer 1

¡Aunque no hay manera de ganar el juego dado, si podemos torcer el juego un poco, podríamos ganar!

newtype ContT'' m a =
    ContT'' { runContT'' :: forall r. (Maybe a -> m (Maybe r)) -> m (Maybe r) }

Como hemos visto en la otra respuesta, el problema que tenemos es, para ganar tenemos que generar un valor para un tipo arbitrario que nuestro oponente haya jugado, pero no sabemos cómo hacerlo.

Al forzar que todos los tipos crudos ( r y a ) sean decorados por Maybe , podemos evitar este problema, y ​​podemos generar el valor de cualquier Maybe t - ¡simplemente no hay que darles Nothing !

Tenemos que demostrar que esto es una Monad .

instance Monad m => Monad (ContT'' m) where
    return a = ContT'' $ /k -> k (Just a)
    a >>= f = ContT'' $ /c -> runContT'' a (
        maybe (return Nothing) (/v -> runContT'' (f v) c)) 

Y luego podemos implementar callCC :

class Monad m => MonadCont'' m where
    callCC'' :: ((a -> forall b.m b) -> m a) -> m a

instance Monad m => MonadCont'' (ContT'' m) where
    callCC'' k = ContT'' $ /c -> 
        runContT'' (k (/a -> ContT'' $ /_ -> c (Just a) >> return Nothing)) c  

Todavía estoy trabajando en cómo reset y shift .

Answer 2

¿Te gustaría jugar un juego ?

Hoy, tienes que ser callCC .

callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
--                                       you are here ^^

Todo a la izquierda de esa flecha de función son los movimientos que tu oponente ha realizado. A la derecha de la flecha está el final del juego. Para ganar, debes construir algo que coincida con el lado derecho utilizando solo las piezas que tu oponente ha proporcionado.

Afortunadamente, todavía tienes algo que decir en los asuntos. ¿Ves esta flecha aquí?

callCC :: ((a -> (forall r. ContT m r)) -> ContT m a) -> ContT m a
--                this is your opponent ^^

Cuando recibes algo que a su vez contiene una flecha, todo lo que está a la izquierda representa movimientos que puedes realizar, y la parte derecha al final de esa rama del juego, que te da otra pieza que puedes usar como parte de tu (con suerte) estrategia ganadora

Antes de continuar, simplifiquemos algunas cosas: el aspecto del transformador de la mónada no es más que una distracción, así que deséchelo; y agregar cuantificadores explícitos para cada tipo de variable.

callCC :: forall a. ((a -> (forall b. Cont b)) -> Cont a) -> Cont a

Ahora, piensa en lo que un tipo como para todos forall a. ... forall a. ... equivale a. Si produce algo con un tipo como ese, está diciendo que puede proporcionar un valor para cualquier tipo a absoluto. Si recibe algo con un tipo como ese, puede elegir un tipo específico para usar. Compare eso con un tipo como A -> ... para una función monomórfica; producir una función de este tipo dice que sabe cómo proporcionar un resultado para cualquier valor de tipo A , mientras que recibir dicha función le permite elegir un valor específico A para usar. Esta parece ser la misma situación que para todos, y de hecho, el paralelo se mantiene. Por lo tanto, podemos tratar a todos como un movimiento en el que usted o su oponente pueden jugar un tipo , en lugar de un término. Para reflejar esto, abusaré de la notación y escribiré para todos forall a. ... forall a. ... como a => ; entonces podemos tratarlo como (->) excepto que debe aparecer a la izquierda de cualquier uso de la variable de tipo que se está enlazando.

También podemos observar que lo único que se puede hacer directamente con un valor de tipo Cont a es aplicar runCont . Así que lo haremos por adelantado e incorporaremos todos los cuantificadores relevantes directamente en el tipo para callCC .

callCC :: a => ( (a -> (b => (r1 => (b -> r1) -> r1))) 
               -> (r2 => (a -> r2) -> r2)
               ) -> (r3 => (a -> r3) -> r3)

Debido a que somos capaces de tratar todas las flechas de función, podemos reordenar las cosas y eliminar paréntesis superfluos para ordenar las cosas un poco. En particular, tenga en cuenta que callCC no es realmente el final del juego, como resulta; tenemos que proporcionar una función, que equivale a proporcionar otro juego para jugar en el que nuevamente tomamos el papel de la flecha que está más a la derecha. Así que podemos salvar un paso fusionándolos. También haré flotar los argumentos de tipo a la izquierda para obtenerlos todos en un solo lugar.

callCC :: a => r3 => (a -> r3) 
       -> (r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2) 
       -> r3

Entonces ... nuestro movimiento.

Necesitamos algo del tipo r3 . Nuestro oponente ha hecho cuatro movimientos, que hemos recibido como argumentos. Un movimiento es elegir r3 , por lo que ya estamos en desventaja. Otro movimiento es a -> r3 , lo que significa que si podemos jugar un a , nuestro oponente arrojará un r3 y podremos llegar a la victoria. Desafortunadamente, nuestro oponente también ha jugado a , así que estamos de vuelta donde empezamos. O bien necesitaremos algo del tipo a , o alguna otra forma de obtener algo del tipo r3 .

El movimiento final que hizo nuestro oponente es más complicado, así que lo examinaremos solo:

r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2

Recuerda, este es el movimiento que hicieron. Entonces, la flecha que está más a la derecha aquí representa a nuestro oponente, y todo a la izquierda representa el tipo de movimientos que podemos hacer. El resultado de esto es algo del tipo r2 , donde r2 es algo que podemos jugar. Así que claramente tendremos que jugar r3 o a para progresar.

Reproduciendo a : Si jugamos a como r2 , entonces podemos jugar id como a -> r2 . El otro movimiento es más complicado, así que saltaremos dentro de eso.

b => r1 => a -> (b -> r1) -> r1

Regreso a la flecha más a la derecha que nos representa. Esta vez necesitamos producir algo del tipo r1 , donde r1 es un movimiento que hizo el oponente. También jugaron una función b -> r1 , donde el tipo b también fue un movimiento que hicieron. Así que necesitamos algo de tipo b o r1 de ellos. Desafortunadamente, todo lo que nos han dado es algo del tipo a , lo que nos deja en una posición imposible de ganar. Supongo que jugar antes era una mala elección. Intentemoslo de nuevo...

Reproducción de r3 : si jugamos r3 como r2 , también necesitamos jugar una función a -> r3 ; afortunadamente, el oponente ya jugó tal función, así que simplemente podemos usar eso. Una vez más saltamos dentro del otro movimiento:

b => r1 => a -> (b -> r1) -> r1

... solo para descubrir que es exactamente la misma situación imposible que antes. Estar a merced de la elección del oponente de r1 sin el requisito de que proporcionen una manera de construir uno, nos deja atrapados.

Tal vez un poco de engaño ayudará?

Doblando las reglas - jugando r1 :

Sabemos que en Haskell regular podemos confiar en la pereza para torcer las cosas y dejar que los cálculos se traguen su propia cola. Sin preocuparnos demasiado por cómo , imaginemos que podemos hacer lo mismo aquí: tomar el r1 que nuestro oponente juega en el juego interno, y retirarlo y volverlo a jugar como r2 .

Una vez más, aquí está el movimiento del oponente:

r2 => (b => r1 => a -> (b -> r1) -> r1) -> (a -> r2) -> r2

Después de nuestros chanchullos nudos, termina siendo equivalente a esto:

(b => a -> (b -> r1) -> r1) -> (a -> r1) -> r1

Los argumentos de tipo han desaparecido gracias a nuestro engaño, pero r1 aún es elegido por el oponente. Así que todo lo que hemos logrado aquí es barajar las cosas; claramente no hay forma de que podamos esperar obtener un A o r3 de esto, por lo que hemos llegado a otro callejón sin salida.

Así que hacemos un último intento desesperado:

Doblando las reglas - jugando b :

Esta vez tomamos la b jugada por el oponente en el juego más interno y la repartimos para jugar como r2 . Ahora el movimiento del oponente se ve así:

(r1 => a -> (b -> r1) -> r1) -> (a -> b) -> b

Y luego de vuelta en el juego interior:

r1 => a -> (b -> r1) -> r1

Continuando con el engaño, también podemos torcer el resultado b arriba, para dar a la función b -> r1 , recibir el r1 que necesitamos. ¡Éxito!

Al salir, todavía nos queda un problema. Tenemos que jugar algo de tipo a -> b . No hay una forma obvia de encontrar uno, pero ya tenemos una b por ahí, así que podemos usar const para descartar la a y--

--pero espera. ¿De dónde viene ese valor de tipo b en primer lugar? Colocándonos brevemente en los zapatos de nuestro oponente, los únicos lugares donde pueden conseguir uno son los resultados de los movimientos que hacemos. Si la única b que tenemos es la que nos dieron, terminaremos dando vueltas en círculos; el juego nunca termina

Entonces, en el juego de callCC , las únicas estrategias que hemos llevado a una pérdida o un estancamiento permanente.

callCC :: forall a. ((a -> (forall b . Cont b)) -> Cont a) -> Cont a
callCC = error "A strange game..."

Por desgracia, parece que el único movimiento ganador es no jugar.