haskell - Utilice MonadRef para implementar MonadCont

continuations delimited-continuations

Question

Existe un problema bien conocido que no podemos usar para todos los tipos en el tipo de devolución Cont .

Sin embargo, debería estar bien tener la siguiente definición:

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

y luego encuentra una instancia que tenga sentido. En este documento, el autor afirmó que podemos implementar MonadFix sobre ContT rm siempre que m implemente MonadFix y MonadRef . Pero creo que si tenemos un MonadRef podemos implementar callCC'' como el siguiente:

--satisfy law: mzero >>= f === mzero
class Monad m => MonadZero m where
mzero :: m a
instance (MonadZero m, MonadRef r m) => MonadCont'' m where
callCC'' k = do
ref <- newRef Nothing
v <- k (/a -> writeRef ref (Just a) >> mzero)
r <- readRef ref
return $ maybe v id r
shift = ...
reset = ...

(Desafortunadamente no estoy familiarizado con la semántica de shift y reset así que no les proporcioné implementaciones)

Esta implementación me parece bien. Intuitivamente, cuando se llama callCC'' , alimentamos k que una función que tiene su propio efecto siempre falla (aunque no podemos proporcionar un valor de tipo arbitrario b , pero siempre podemos proporcionar mzero de tipo mb y de acuerdo con la ley debería detener efectivamente todos los efectos adicionales que se calculan), y captura el valor recibido como el resultado final de callCC'' .

Entonces mi pregunta es:

¿Funciona esta implementación como se espera para un callCC ideal? ¿Podemos implementar shift y reset con la semántica adecuada también?

Además de lo anterior, quiero saber:

Para garantizar el comportamiento correcto, debemos asumir alguna propiedad de MonadRef . Entonces, ¿qué leyes tendría MonadRef para hacer que la implementación anterior se comporte como se esperaba?

ACTUALIZAR

Resulta que la implementación ingenua anterior no es lo suficientemente buena. Para que satisfaga la "corriente de continuación"

callCC $/k -> k m === callCC $ const m === m

Tenemos que ajustar la implementación a

instance (MonadPlus m, MonadRef r m) => MonadCont'' m where
callCC'' k = do
ref <- newRef mzero
mplus (k $ /a -> writeRef ref (return a) >> mzero) (join (readRef ref))

En otras palabras, el MonadZero original no es suficiente, tenemos que ser capaces de combinar un valor de mzero con un cálculo normal sin cancelar todo el cálculo.

Lo anterior no responde a la pregunta, solo se ajusta porque el intento original fue falsificado para ser candidato. Pero para la versión actualizada, las preguntas originales siguen siendo preguntas. Especialmente, el reset y el shift aún están por implementarse.

Answer 1

(Todavía no se trata de una respuesta, pero solo se me ocurrieron algunas pistas. Espero que esto conduzca a la respuesta real, solo o de otra persona).

Llamada por valor es dual para llamar por nombre - Philip Wadler

En el documento anterior, el autor introdujo el "Cálculo dual", un cálculo tipado que corresponde a la lógica clásica. En la última sección, hay un segmento que dice

Una estrategia dual para llamar por necesidad podría evitar esta ineficacia sobrescribiendo un coterm con su covalor la primera vez que se evalúa.

Como se indica en el documento de Wadler, la llamada por nombre evalúa las continuaciones con entusiasmo (regresa antes de que se evalúen todos los valores) mientras call-by-value evalúa las continuaciones de forma perezosa (solo regresa después de todos los valores evaluados).

Ahora, eche un vistazo al callCC'' anterior, creo que este es un ejemplo del doble de call-by-need en el lado de continuación. La estrategia de la evaluación es proporcionar una "continuación" falsa a la función dada, pero almacenar en caché el estado en este punto para llamar a la continuación "verdadera" más adelante. Esto de alguna manera es como hacer un caché de la continuación, así que una vez que termina el cálculo, restauramos esa continuación. Pero la caché del valor evaluado es lo que significa llamar por necesidad.

En general, sospecho que el estado (cómputo hasta el punto de tiempo actual) es dual a la continuación (el cálculo futuro). Esto explicará algunos fenómenos. Si esto es cierto, no es una sorpresa que MonadRef (corresponde a un estado global y polimórfico) es dual a MoncadCont (corresponde a continuaciones globales y polimórficas), por lo que se pueden usar para implementarse entre sí.