Convertir A = > M[B] en M [A = > B]

Question

Convertir A = > M[B] en M [A = > B]

Para una mónada M, ¿es posible convertir A => M[B] en M[A => B]?

He intentado seguir los tipos en vano, lo que me hace pensar que no es posible, pero pensé que me gustaría preguntar de todos modos. Además, buscando Hoogle para a -> m b -> m (a -> b) no devolvió nada, así que no estoy sosteniendo mucha suerte.

38

haskell scala scalaz

Author: Noel M, 2014-12-03

Source

3 answers

Las otras respuestas han ilustrado muy bien que en general no es posible implementar una función de a -> m b a m (a -> b) para cualquier mónada m. Sin embargo, hay mónadas específicas donde es bastante posible implementar esta función. Un ejemplo es la mónada lectora:

data Reader r a = R { unR :: r -> a }

commute :: (a -> Reader r b) -> Reader r (a -> b)
commute f = R $ \r a -> unR (f a) r

4

Author: svenningsson,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2014-12-11 16:20:05

No.

Por ejemplo, Option es una mónada, pero la función (A => Option[B]) => Option[A => B] no tiene una implementación significativa:

def transform[A, B](a: A => Option[B]): Option[A => B] = ???

¿Qué pones en lugar de ???? Some? Some ¿de qué entonces? O None?

3

Author: ZhekaKozlov,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/ajaxhispano.com/template/agent.layouts/content.php on line 61
2014-12-03 10:29:02

score 55 · Accepted Answer

En la práctica

No, no se puede hacer, al menos no de una manera significativa.

Considere este código de Haskell

action :: Int -> IO String
action n = print n >> getLine

Esto toma n primero, lo imprime (IO realizado aquí), luego lee una línea del usuario.

Supongamos que tenemos un hipotético transform :: (a -> IO b) -> IO (a -> b). Entonces, como un experimento mental, considere:

action' :: IO (Int -> String)
action' = transform action

Lo anterior tiene que hacer todo el IO de antemano, antes de conocer n, y luego devolver una función pura. Esto no puede ser equivalente al código arriba.

Para enfatizar el punto, considere este código sin sentido a continuación:

test :: IO ()
test = do f <- action'
          putStr "enter n"
          n <- readLn
          putStrLn (f n)

Mágicamente, action' debe saber de antemano lo que el usuario va a escribir a continuación! Una sesión se vería como

42     (printed by action')
hello  (typed by the user when getLine runs)
enter n
42     (typed by the user when readLn runs)
hello  (printed by test)

Esto requiere una máquina del tiempo, por lo que no se puede hacer.

En teoría

No, no se puede hacer. El argumento es similar a el que di a una pregunta similar.

Asumir por contradicción transform :: forall m a b. Monad m => (a -> m b) -> m (a -> b) existe. Especializarse m a la continuación monad ((_ -> r) -> r) (Omito la envoltura newtype).

transform :: forall a b r. (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

Especializarse r=a:

transform :: forall a b. (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

Se aplica:

transform const :: forall a b. ((a -> b) -> a) -> a

Por el isomorfismo de Curry-Howard, la siguiente es una tautología intuicionista{[19]]}

((A -> B) -> A) -> A

Pero esta es la Ley de Peirce, que no es demostrable en la lógica intuicionista. Contradicción.