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

He leído que es útil realizar un seguimiento de los efectos secundarios. Pero la firma tipográfica y la documentación no me llevan a ninguna parte.

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

Como siempre, la terminología que usa la gente no es del todo coherente. Hay una variedad de nociones inspiradas en mónadas, pero estrictamente hablando, no lo son. El término "mónada indexada" es uno de un número (incluyendo "mónada" y "mónada parametrizada" (el nombre de Atkey para ellos)) de términos usados ​​para caracterizar una de tales nociones. (Otra noción de este tipo, si está interesado, es la "mónada de efecto paramétrico" de Katsumata, indexada por un monoide, donde el retorno se indexa de forma neutral y la vinculación se acumula en su índice).

En primer lugar, veamos los tipos.

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

Es decir, el tipo de "cálculo" (o "acción", si lo prefiere, pero me quedo con "cálculo"), parece

m before after value

donde before, after :: statey value :: *. La idea es capturar los medios para interactuar de forma segura con un sistema externo que tiene una noción predecible de estado. El tipo de cálculo le dice cuál debe ser el estado en el que beforese ejecuta, cuál será el estado en el que afterse ejecuta y (como con las mónadas regulares *) qué tipo de values produce el cálculo.

Las partes y piezas habituales son, a la vez, *como una mónada y, a la vez, statecomo jugar al dominó.

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

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

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

y obtenemos una composición

icomp :: IxMonad m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
icomp f g = \ a -> ibind (g a) f

y, como siempre, las leyes garantizan exactamente eso ireturny icompnos dan una categoría

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

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

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

¿Por qué molestarse? Modelar "reglas" de interacción. Por ejemplo, no puede expulsar un DVD si no hay uno en la unidad y no puede colocar un DVD en la unidad si ya hay uno. Entonces

data DVDDrive :: Bool -> Bool -> * -> * where  -- Bool is "drive full?"
  DReturn :: a -> DVDDrive i i a
  DInsert :: DVD ->                   -- you have a DVD
             DVDDrive True k a ->     -- you know how to continue full
             DVDDrive False k a       -- so you can insert from empty
  DEject  :: (DVD ->                  -- once you receive a DVD
              DVDDrive False k a) ->  -- you know how to continue empty
             DVDDrive True k a        -- 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  = k a
  ibind (DInsert dvd j) k  = DInsert dvd (ibind j k)
  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 los cuales se ensamblan otros con ireturny ibind. Ahora, puedo escribir (tomar prestado una donota)

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 sus comandos primitivos directamente

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

y luego instancia la plantilla genérica

data CommandIxMonad :: (state -> state -> * -> *) ->
                        state -> state -> * -> * where
  CReturn  :: a -> CommandIxMonad c i i a
  (:?)     :: c i j a -> (a -> CommandIxMonad c j k b) ->
                CommandIxMonad c i k b

instance IxMonad (CommandIxMonad c) where
  ireturn = CReturn
  ibind (CReturn a) k  = k a
  ibind (c :? j)    k  = c :? \ a -> ibind (j a) k

En efecto, hemos dicho cuáles son las flechas primitivas de Kleisli (qué es un "dominó"), y luego hemos construido una noción adecuada de "secuencia de cálculo" sobre ellas.

Tenga en cuenta que para cada mónada indexada m, la "diagonal sin cambios" m i ies una mónada, pero en general m i jno 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 una mónada instanciada para alguna otra categoría.

Ahora, mire nuevamente el tipo de flecha de Kleisli

a -> m i j b

Sabemos que debemos estar en estado ipara 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 la unidad, ¡entra! La unidad de DVD no tiene nada que decir sobre el estado después de cada comando.

Pero eso no es cierto en general, al interactuar con el mundo. A veces, es posible que deba ceder algo de control y dejar que el mundo haga lo que quiera. Por ejemplo, si es un servidor, puede ofrecerle a su cliente una opción y el estado de su sesión dependerá de lo que elija. La operación de "elecció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 .

¿Qué es una herramienta mejor?

type f :-> g = forall state. f state -> g state

class MonadIx (m :: (state -> *) -> (state -> *)) where
  returnIx    :: x :-> m x
  flipBindIx  :: (a :-> m b) -> (m a :-> m b)  -- tidier than bindIx

¿Galletas de miedo? Realmente no, por dos razones. Primero, se parece más a lo que es una mónada, porque es una mónada, pero más (state -> *)bien que *. Dos, si miras el tipo de flecha Kleisli,

a :-> m b   =   forall state. a state -> m b state

obtienes el tipo de cálculos con una condición previa a y una condición posterior b, como en Good Old Hoare Logic. Las afirmaciones en la lógica del programa han tardado menos de medio siglo en cruzar la correspondencia Curry-Howard y convertirse en tipos Haskell. El tipo de returnIxdice "puede lograr cualquier condición posterior que se cumpla, 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, poniendo todos los cuantificadores.

bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

Estos foralls tienen polaridad opuesta. Elegimos el estado inicial iy un cálculo que puede comenzar en i, con poscondición a. El mundo elige cualquier estado intermedio jque le guste, pero debe darnos la evidencia de que la poscondición bes válida y, a partir de ese estado, podemos continuar para bmantenernos. Entonces, en secuencia, podemos lograr la condición bdel estado i. Al soltar nuestro control sobre los estados "posteriores", podemos modelar cálculos impredecibles .

Ambos IxMonady MonadIxson útiles. Ambos modelan la validez 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 a veces es una realidad. Con suerte, entonces, esta respuesta da alguna indicación de qué 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 ubica entre los informáticos Bob Atkey, Conor McBride y Dominic Orchard, ya que así es como tiendo a pensar en ellos. Partes de estas construcciones tienen una historia mucho más ilustre e interpretaciones más agradables a través de la teoría de categorías, pero primero supe de ellas asociadas con estos nombres, y estoy tratando de evitar que esta respuesta se vuelva 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 -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

También podemos definir comonads indexados a la Atkey. De hecho, aprovecho mucho los que están en el lenscódigo base .

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 cambio, 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. a i -> b i 

entonces podemos escribir la definición de McBride como

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

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 (m :: (k -> *) -> (k -> *).

Curiosamente, puede recuperar el estilo de mónada indexada de Atkey de McBride utilizando un tipo de datos inteligente, que McBride en su estilo inimitable elige decir que debería leer como "en clave".

data (:=) :: a i j 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 ibindpuede devolverle lo mismo que Atkey 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 se ha ganado estrictamente.

Otra cosa interesante 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 endofunctores en la categoría de functores de (k -> *)a en (k -> *)lugar de la categoría de functores de *a *.

Un ejercicio divertido es descubrir cómo hacer la conversión de McBride a Atkey para comonads indexados . Personalmente, utilizo un tipo de datos 'At' para la construcción "en clave" en el artículo de McBride. De hecho, me acerqué a Bob Atkey en ICFP 2013 y mencioné que lo había vuelto del revés para convertirlo en un "abrigo". Parecía visiblemente perturbado. La línea se desarrolló mejor en mi cabeza. =)

Huerta

Finalmente, un tercer reclamante al que se hace referencia mucho menos comúnmente al nombre de "mónada indexada" se debe a Dominic Orchard, donde en su lugar usa un monoide de nivel de tipo para romper índices. En lugar de repasar los detalles de la construcción, simplemente vincularé esta charla:

https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf

Como escenario simple, suponga que tiene una mónada estatal. El tipo de estado es complejo y grande, 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 un estado 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 evitar esto de forma estática. La mónada indexada cumple este objetivo:

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 de 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 pila 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, suponga que desea una mónada de E / S restringida que no permita el acceso a archivos. Podrías usar, por ejemplo,

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

De esta manera, IO ... NoAccess ()se garantiza estáticamente que una acción que tiene un tipo no tendrá acceso a archivos. En cambio, una acción de tipo IO ... FilesAccessed ()puede acceder a archivos. Tener una mónada indexada significaría que no tiene que construir un tipo separado para el IO restringido, lo 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 => m aun valor en una mónada indexada sería IndexedMonad m => m i j adonde iy json tipos de índice, de modo que ese ies el tipo de índice al comienzo del cálculo monádico y jal final del cálculo. En cierto modo, puede pensar ien una especie de tipo de entrada y jcomo el tipo de salida.

Utilizando Statecomo ejemplo, un cálculo con estado State s amantiene un estado de tipo sdurante todo el cálculo y devuelve un resultado de tipo a. Una versión indexada IndexedState i j a, es un cálculo con estado en el que el estado puede cambiar a un tipo diferente durante el cálculo. El estado inicial tiene el tipo iy el estado y el final del cálculo tiene el tipo j.

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

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

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

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

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

Las mónadas indexadas permiten codificar parte de lo que hacen los sistemas de tipo dependiente, para gestionar los efectos secundarios con mayor precisión.