haskell - quiere - ¿Cómo se puede expresar la mónada de continuación utilizando la mónada libre?

mónada significado

Question

Supuestamente, todas las mónadas se pueden expresar usando Free (si esto no es cierto, ¿qué es un contra-ejemplo y por qué)? ¿Cómo se puede expresar la mónada de continuación o su transformador correspondiente utilizando Free o FreeT ? ¿ FreeT sería el funtor correspondiente? O si no pueden, ¿por qué?

Actualización: por expresamente quiero decir básicamente isomorfos a Free F donde F es un functor que estamos buscando, como por ejemplo Writer w es isomorphic a Free ((,) w) .

Answer 1

Aquí hay un par de pequeñas pruebas de que no existe un Functor f tal que para todos a :: * y m :: * -> * FreeT fma es equivalente a ContT rma utilizando la interpretación normal de FreeT .

Deje m :: * -> * modo que no haya una instancia de Functor m . Debido al instance Functor (ContT rm) hay un Functor (ConT rm) instancia Functor (ConT rm) . Si ContT r y FreeT f son equivalentes, esperaríamos a Functor (FreeT fm) . Sin embargo, utilizando la interpretación normal de FreeT , instance (Functor f, Functor m) => Functor (FreeT fm) , no hay una instancia de Functor (FreeT fm) porque no hay una instancia de Functor m . ( FreeT normal de FreeT de requerir FreeT Monad m a solo requerir Functor m ya que solo hace uso de liftM .)

Sea m :: * -> * tal que no hay una instancia de Monad m . Debido a la instance Monad (ContT rm) hay una instancia Monad (ConT rm) . Si ContT r y FreeT f son equivalentes, esperaríamos Monad (FreeT fm) . Sin embargo, utilizando la interpretación normal de FreeT , instance (Functor f, Monad m) => Monad (FreeT fm) , no hay una instancia de Monad (FreeT fm) porque no hay una instancia de Monad m .

Si no queremos usar la interpretación normal de Free o FreeT podemos FreeT monstruos que funcionan como Cont r o ContT r . Por ejemplo, hay un Functor (fr) tal que Free (fr) a puede ser equivalente a Cont ra utilizando una interpretación anormal de Free , es decir, Cont r sí.

Answer 2

Aquí hay una respuesta tonta que muestra que tanto tu pregunta como mi respuesta anterior deben funcionar.

Cont puede expresarse fácilmente usando Free :

import Control.Monad.Free
import Control.Monad.Trans.Cont

type Cont'' r = Free (Cont r)

quotient :: Cont'' r a -> Cont r a
quotient = retract

Cont es un (cociente de) la mónada libre sobre sí misma (por supuesto). Así que ahora tienes que aclarar exactamente qué quieres decir con "expreso".

Answer 3

La mónada de continuación es el contraejemplo que estás buscando. No tengo el conocimiento suficiente para proporcionar una prueba completa, pero le daré un par de referencias para consultar.

La idea es que las mónadas tienen un concepto de "rango" asociado con ellas. "Rango" significa aproximadamente el número de operaciones necesarias para proporcionar la funcionalidad completa de la mónada.

Sospecho que, con la excepción de las mónadas derivadas de la continuación, todas las mónadas con las que tratamos en Haskell tienen rango, por ejemplo, Identity , Maybe , State s , Either e , Either e ... y sus combinaciones a través de sus transformadores. Por ejemplo, la Identity se genera por ninguna operación, Maybe se genera por Nothing , el State s por get y put s y Either e por Left e . (Tal vez esto muestre que, de hecho, todos tienen un rango finito , o tal vez put s cuenta como una operación diferente para cada s , por lo que el State s tiene el rango del tamaño de s , no estoy seguro).

Las mónadas libres ciertamente tienen rango porque Free f se genera explícitamente por las operaciones codificadas por f .

Aquí hay una definición técnica de rango, pero no es muy esclarecedor: http://journals.cambridge.org/action/displayAbstract?aid=4759448

Aquí puede ver la afirmación de que la mónada de continuación no tiene rango: http://www.cs.bham.ac.uk/~hxt/cw04/hyland.pdf . No estoy seguro de cómo prueban eso, pero la implicación es que la mónada de continuación no es generada por ninguna colección de operaciones y, por lo tanto, no se puede expresar como (un cociente de) una mónada libre.

Esperemos que alguien pueda venir y ordenar mis tecnicismos, pero esta es la estructura de la prueba que desea.

Answer 4

Vea mi respuesta a una pregunta suya del año pasado . Consideremos r = Bool (o más generalmente cualquier tipo r que admita un automorfismo no trivial).

Defina m (hasta wtyppers newtype) como m :: (() -> Bool) -> Bool; mf = not (f ()) m :: (() -> Bool) -> Bool; mf = not (f ()) . Entonces m no es trivial pero m >> m es trivial. Así que Cont Bool no es isomorfo a una mónada libre.

El cálculo completo en Haskell:

rwbarton@morphism:/tmp$ ghci
GHCi, version 7.8.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> import Control.Monad.Cont
Prelude Control.Monad.Cont> let m :: Cont Bool (); m = ContT (/f -> fmap not (f ()))
Loading package transformers-0.3.0.0 ... linking ... done.
Prelude Control.Monad.Cont> runCont m (const False) -- m not trivial
True
Prelude Control.Monad.Cont> runCont (m >> m) (const False)
False
Prelude Control.Monad.Cont> runCont (m >> m) (const True) -- (m >> m) trivial
True