¿Qué es la mónada indexada?

¿Qué es la mónada indexada y la motivación para esta mónada?

He leído que ayuda a realizar un seguimiento de los efectos secundarios. Pero el tipo de firma y documentación no me lleva a ninguna parte.

¿Cuál sería un ejemplo de cómo puede ayudar a realizar un seguimiento de los efectos secundarios (o cualquier otro ejemplo válido)?

Como siempre, la terminología que usan las personas no es del todo coherente. Hay una gran variedad de nociones inspiradas por mónadas, pero estrictamente hablando. El término “mónada indexada” es uno de un número (incluidos “monadish” y “mónada parametrizada” (nombre de Atkey para ellos)) de los términos utilizados para caracterizar una de esas nociones. (Otra noción, si está interesado, es la “mónada del efecto paramétrico” de Katsumta, indexada por un monoide, donde el retorno se indexa de forma neutral y el enlace se acumula en su índice).

Antes que nada, revisemos los tipos.

IxMonad (m :: state -> state -> * -> *) 

Es decir, el tipo de “computación” (o “acción”, si lo prefiere, pero me quedaré con “computación”), se ve como

 m before after value 

donde before, after :: state y value :: * . La idea es capturar los medios para interactuar de manera segura con un sistema externo que tenga una noción de estado predecible . El tipo de cálculo le dice qué estado debe tener before ejecutarse, cuál será el estado after se ejecute y (como con las mónadas regulares sobre * ) qué tipo de value s produce el cálculo.

Los bits y piezas habituales son * -de forma parecida a una mónada y a nivel state como jugar al dominó.

 ireturn :: a -> miia -- returning a pure value preserves state ibind :: mija -> -- we can go from i to j and get an a, thence (a -> mjkb) -- we can go from j to k and get ab, therefore -> mikb -- we can indeed go from i to k and get ab 

La noción de “flecha Kleisli” (función que produce el cálculo) así generada es

 a -> mijb -- values a in, b out; state transition i to j 

y obtenemos una composición

 icomp :: IxMonad m => (b -> mjkc) -> (a -> mijb) -> a -> mikc icomp fg = \ a -> ibind (ga) f 

y, como siempre, las leyes garantizan exactamente que ireturn e icomp nos den una categoría

  ireturn `icomp` g = g f `icomp` ireturn = f (f `icomp` g) `icomp` h = f `icomp` (g `icomp` h) 

o, en comedia falsa C / Java / lo que sea,

  g(); skip = g() skip; f() = f() {h(); g()}; f() = h(); {g(); f()} 

¿Por qué molestarse? Para modelar “reglas” de interacción. Por ejemplo, no puede expulsar un DVD si no hay uno en la unidad, y no puede poner un DVD en la unidad si ya hay uno en ella. Asi que

 data DVDDrive :: Bool -> Bool -> * -> * where -- Bool is "drive full?" DReturn :: a -> DVDDrive iia DInsert :: DVD -> -- you have a DVD DVDDrive True ka -> -- you know how to continue full DVDDrive False ka -- so you can insert from empty DEject :: (DVD -> -- once you receive a DVD DVDDrive False ka) -> -- you know how to continue empty DVDDrive True ka -- so you can eject when full instance IxMonad DVDDrive where -- put these methods where they need to go ireturn = DReturn -- so this goes somewhere else ibind (DReturn a) k = ka ibind (DInsert dvd j) k = DInsert dvd (ibind jk) ibind (DEject j) k = DEject j $ \ dvd -> ibind (j dvd) k 

Con esto en su lugar, podemos definir los comandos “primitivos”

 dInsert :: DVD -> DVDDrive False True () dInsert dvd = DInsert dvd $ DReturn () dEject :: DVDrive True False DVD dEject = DEject $ \ dvd -> DReturn dvd 

de la cual otros se reúnen con ireturn e ibind . Ahora, puedo escribir (tomar prestado -notación)

 discSwap :: DVD -> DVDDrive True True DVD discSwap dvd = do dvd' < - dEject; dInsert dvd ; ireturn dvd' 

pero no lo físicamente imposible

 discSwap :: DVD -> DVDDrive True True DVD discSwap dvd = do dInsert dvd; dEject -- ouch! 

Alternativamente, uno puede definir los comandos primitivos de uno directamente

 data DVDCommand :: Bool -> Bool -> * -> * where InsertC :: DVD -> DVDCommand False True () EjectC :: DVDCommand True False DVD 

y luego crear una instancia de la plantilla genérica

 data CommandIxMonad :: (state -> state -> * -> *) -> state -> state -> * -> * where CReturn :: a -> CommandIxMonad ciia (:?) :: cija -> (a -> CommandIxMonad cjkb) -> CommandIxMonad cikb instance IxMonad (CommandIxMonad c) where ireturn = CReturn ibind (CReturn a) k = ka ibind (c :? j) k = c :? \ a -> ibind (ja) k 

En efecto, hemos dicho lo que son las flechas primitivas de Kleisli (lo que es un "dominó"), y luego construimos una noción adecuada de "secuencia de cálculo" sobre ellas.

Tenga en cuenta que por cada mónada indexada m , la mii "sin cambio diagonal" es una mónada, pero en general, mij no lo es. Además, los valores no están indexados, pero los cálculos están indexados, por lo que una mónada indexada no es solo la idea habitual de la mónada instanciada para alguna otra categoría.

Ahora, mira nuevamente el tipo de flecha de Kleisli

 a -> mijb 

Sabemos que debemos estar en el estado i para comenzar, y predecimos que cualquier continuación comenzará desde el estado j . ¡Sabemos mucho sobre este sistema! ¡Esta no es una operación arriesgada! Cuando ponemos el dvd en el disco, ¡entra! La unidad de DVD no tiene voz en qué es el estado después de cada comando.

Pero eso no es cierto en general, cuando se interactúa con el mundo. A veces es posible que necesites ceder algo de control y dejar que el mundo haga lo que quiera. Por ejemplo, si usted es un servidor, puede ofrecerle a su cliente una opción, y su estado de sesión dependerá de lo que elija. La operación de "opción de oferta" del servidor no determina el estado resultante, pero el servidor debería poder continuar de todos modos. No es un "comando primitivo" en el sentido anterior, por lo que las mónadas indexadas no son una herramienta tan buena para modelar el escenario impredecible .

¿Cuál es una mejor herramienta?

 type f :-> g = forall state. f state -> g state class MonadIx (m :: (state -> *) -> (state -> *)) where returnIx :: x :-> mx flipBindIx :: (a :-> mb) -> (ma :-> mb) -- tidier than bindIx 

Bizcochos aterrador? No realmente, por dos razones. Primero, se parece más a lo que es una mónada, porque es una mónada, pero termina (state -> *) lugar de * . Dos, si miras el tipo de una flecha Kleisli,

 a :-> mb = forall state. a state -> mb state 

obtienes el tipo de cálculos con una precondición b a postcondición b , como en Good Old Hoare Logic. Las afirmaciones en la lógica de los progtwigs han llevado menos de medio siglo para cruzar la correspondencia Curry-Howard y convertirse en tipos Haskell. El tipo de returnIx dice "puede lograr cualquier returnIx que se mantenga, simplemente sin hacer nada", que es la regla de Hoare Logic para "omitir". La composición correspondiente es la regla de Hoare Logic para ";".

Terminemos mirando el tipo de bindIx , colocando todos los cuantificadores.

 bindIx :: forall i. mai -> (forall j. aj -> mbj) -> mbi 

Estos forall tienen polaridad opuesta. Elegimos el estado inicial i , y un cálculo que puede comenzar en i , con la poscondición a . El mundo elige cualquier estado intermedio j lo que le gusta, pero debe darnos la evidencia de que la poscondición b es válida, y de cualquier estado tal, podemos continuar para hacer b . Entonces, en secuencia, podemos lograr la condición b del estado i . Al liberar nuestro control sobre los estados "posteriores", podemos modelar cálculos impredecibles .

Tanto IxMonad como MonadIx son útiles. Tanto la validez del modelo de los cálculos interactivos con respecto al estado cambiante, predecible e impredecible, respectivamente. La previsibilidad es valiosa cuando se puede obtener, pero la imprevisibilidad es a veces un hecho de la vida. Con suerte, entonces, esta respuesta da una indicación de lo que son las mónadas indexadas, prediciendo cuándo comienzan a ser útiles y cuándo se detienen.

Hay al menos tres formas de definir una mónada indexada que conozco.

Me referiré a estas opciones como mónadas indexadas a la X , donde X se extiende sobre los científicos informáticos Bob Atkey, Conor McBride y Dominic Orchard, ya que así es como tiendo a pensar en ellos. Algunas partes de estas construcciones tienen una historia mucho más ilustre y más bellas interpretaciones a través de la teoría de categorías, pero primero me enteré de ellas asociadas con estos nombres, y trato de evitar que esta respuesta sea demasiado esotérica.

Atkey

El estilo de mónada indexada de Bob Atkey es trabajar con 2 parámetros adicionales para lidiar con el índice de la mónada.

Con eso obtienes las definiciones que la gente ha lanzado en otras respuestas:

 class IMonad m where ireturn :: a -> miia ibind :: mija -> (a -> mjkb) -> mikb 

También podemos definir comonads indexados à la Atkey también. De hecho, obtengo mucho kilometraje de aquellos en la base de código de la lens .

McBride

La siguiente forma de mónada indexada es la definición de Conor McBride de su artículo “Kleisli Arrows of Outrageous Fortune” . En su lugar, usa un solo parámetro para el índice. Esto hace que la definición de mónada indexada tenga una forma bastante inteligente.

Si definimos una transformación natural usando parametricidad de la siguiente manera

 type a ~> b = forall i. ai -> bi 

entonces podemos escribir la definición de McBride como

 class IMonad m where ireturn :: a ~> ma ibind :: (a ~> mb) -> (ma ~> mb) 

Esto se siente bastante diferente al de Atkey, pero se siente más como una mónada normal, en lugar de construir una mónada (m :: * -> *) , la construimos sobre (m :: (k -> *) -> (k -> *) .

Curiosamente, puedes recuperar el estilo de mónada indexada de Atkey de McBride usando un tipo de datos inteligente, que McBride en su estilo inimitable elige decir que debes leer como “en clave”.

 data (:=) :: aij where V :: a -> (a := i) i 

Ahora puedes resolver eso

 ireturn :: IMonad m => (a := j) ~> m (a := j) 

que se expande a

 ireturn :: IMonad m => (a := j) i -> m (a := j) i 

solo se puede invocar cuando j = i, y luego una lectura cuidadosa de ibind puede hacerte volver a lo mismo que ibind de ibind . Necesita pasar estas estructuras de datos (: =), pero recuperan el poder de la presentación de Atkey.

Por otro lado, la presentación de Atkey no es lo suficientemente fuerte como para recuperar todos los usos de la versión de McBride. El poder ha sido estrictamente ganado.

Otra cosa agradable es que la mónada indexada de McBride es claramente una mónada, es solo una mónada en una categoría de functor diferente. Funciona sobre endofunctors en la categoría de funtores de (k -> *) a (k -> *) lugar de la categoría de funtores de * a * .

Un ejercicio divertido es descubrir cómo hacer la conversión de McBride a Atkey para comonads indexados. Yo personalmente uso un tipo de datos ‘At’ para la construcción “en clave” en el documento de McBride. De hecho, me acerqué a Bob Atkey en ICFP 2013 y mencioné que lo había convertido en un “Escudo”. Parecía visiblemente perturbado. La línea se jugó mejor en mi cabeza. =)

Huerta

Finalmente, un tercer reclamante con mucho menos referencia al nombre de “mónada indexada” se debe a Dominic Orchard, donde en su lugar utiliza un monoide de nivel de tipo para aplastar índices. En lugar de ir a través de los detalles de la construcción, simplemente voy a vincular a esta charla:

http://www.cl.cam.ac.uk/~dao29/ixmonad/ixmonad-fita14.pdf

Como un escenario simple, suponga que tiene una mónada de estado. El tipo de estado es uno grande complejo, sin embargo, todos estos estados se pueden dividir en dos conjuntos: estados rojo y azul. Algunas operaciones en esta mónada tienen sentido solo si el estado actual es azul. Entre estos, algunos mantendrán el estado azul ( blueToBlue ), mientras que otros harán que el estado sea rojo ( blueToRed ). En una mónada regular, podríamos escribir

 blueToRed :: State S () blueToBlue :: State S () foo :: State S () foo = do blueToRed blueToBlue 

desencadenando un error de tiempo de ejecución ya que la segunda acción espera un estado azul. Nos gustaría prevenir esto estáticamente. La mónada indexada cumple este objective:

 data Red data Blue -- assume a new indexed State monad blueToRed :: State S Blue Red () blueToBlue :: State S Blue Blue () foo :: State S ?? ?? () foo = blueToRed `ibind` \_ -> blueToBlue -- type error 

Se desencadena un error de tipo porque el segundo índice de blueToRed ( Red ) difiere del primer índice de blueToBlue ( Blue ).

Como otro ejemplo, con las mónadas indexadas puede permitir que una mónada de estado cambie el tipo para su estado, por ejemplo, podría tener

 data State old new a = State (old -> (new, a)) 

Puede usar lo anterior para construir un estado que sea una stack heterogénea de tipo estático. Las operaciones tendrían tipo

 push :: a -> State old (a,old) () pop :: State (a,new) new a 

Como otro ejemplo, supongamos que quiere una món IO restringida que no permite el acceso a archivos. Podría usar, por ejemplo

 openFile :: IO any FilesAccessed () newIORef :: a -> IO any any (IORef a) -- no operation of type :: IO any NoAccess _ 

De esta forma, una acción que tenga tipo IO ... NoAccess () está garantizada estáticamente como libre de acceso a archivos. En cambio, una acción de tipo IO ... FilesAccessed () puede acceder a los archivos. Tener una mónada indexada significa que no es necesario crear un tipo separado para el IO restringido, que requeriría duplicar todas las funciones no relacionadas con archivos en ambos tipos de IO.

Una mónada indexada no es una mónada específica como, por ejemplo, la mónada de estado sino una especie de generalización del concepto de mónada con parámetros de tipo adicionales.

Mientras que un valor monádico “estándar” tiene el tipo Monad m => ma un valor en una mónada indexada sería IndexedMonad m => mija donde i y j son tipos de índice, de modo que i es el tipo de índice al comienzo de la monádica computación y j al final del cálculo. En cierto modo, puede pensar en i como una especie de tipo de entrada j como el tipo de salida.

Usando State como ejemplo, un Stateful computation State sa mantiene un estado de tipo s largo del cálculo y devuelve un resultado de tipo a . Una versión indexada, IndexedState ija , es un cálculo con estado donde el estado puede cambiar a un tipo diferente durante el cálculo. El estado inicial tiene el tipo i y el estado y el final del cálculo tiene el tipo j .

Usar una mónada indexada sobre una mónada normal rara vez es necesaria, pero puede usarse en algunos casos para codificar garantías estáticas más estrictas.

Puede ser importante observar cómo se usa la indexación en los tipos dependientes (por ejemplo, en agda). Esto puede explicar cómo la indexación ayuda en general, luego traducir esta experiencia a mónadas.

La indexación permite establecer relaciones entre instancias particulares de tipos. Luego puede razonar acerca de algunos valores para establecer si esa relación se cumple.

Por ejemplo (en agda) puede especificar que algunos números naturales estén relacionados con _<_ , y el tipo indica qué números son. Entonces puede requerir que alguna función reciba un testigo que m < n , porque solo entonces la función funciona correctamente, y sin proporcionar tal testigo el progtwig no comstackrá.

Como otro ejemplo, dada la suficiente perseverancia y el soporte del comstackdor para el idioma elegido, podría codificar que la función asum que una determinada lista está ordenada.

Las mónadas indexadas permiten codificar algunos de los sistemas de tipos dependientes, para administrar los efectos secundarios de manera más precisa.