haskell - leibniz - monadas filosofia
¿Qué es la mónada indexada? (5)
Como escenario simple, suponga que tiene una mónada estatal.
El tipo de estado es complejo y grande, pero 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 mantendrán el estado rojo (
blueToRed
).
En una mónada normal, 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 estáticamente. 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))
Podría usar lo anterior para generar 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 IO 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, una acción que tiene el tipo
IO ... NoAccess ()
está estáticamente garantizada 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 significaría que no tiene que construir un tipo separado para la E / S restringida, lo que requeriría duplicar todas las funciones no relacionadas con archivos en ambos tipos de E / S.
¿Qué es la mónada indexada y la motivación para esta mónada?
He leído que ayuda hacer un seguimiento de los efectos secundarios. Pero la firma de tipo y la documentación no me llevan a ningún lado.
¿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 consistente. Hay una variedad de nociones inspiradas por mónadas, pero estrictamente hablando, no es del todo. 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 los términos utilizados para caracterizar una de estas nociones. (Otra noción de este tipo, si le interesa, es la "mónada del efecto paramétrico" de Katsumata, indexada por un monoide, donde el retorno se indexa de forma neutral y el enlace se acumula en su índice).
En primer lugar, verifiquemos los tipos.
IxMonad (m :: state -> state -> * -> *)
Es decir, el tipo de "cálculo" (o "acción", si lo prefiere, pero me quedaré con "cálculo"), parece
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
predecible
de estado.
El tipo de cálculo le indica cuál debe ser el estado
before
se ejecute, cuál será el estado
after
se ejecute y (como con mónadas regulares sobre
*
) qué tipo de
value
produce el cálculo.
Los bits y piezas habituales son
*
forma de mónada y en
state
como 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 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()
{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 poner un DVD en la unidad si ya hay uno en él. 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 otros se ensamblan con
ireturn
e
ibind
.
Ahora puedo escribir (tomar prestado
do
notation)
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 instanciar 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ó"), luego construimos una noción adecuada de "secuencia de cálculo" sobre ellas.
Tenga en cuenta que para cada mónada indexada
m
,
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 una mónada instanciada para alguna otra categoría.
Ahora, mira de nuevo el tipo de flecha de Kleisli
a -> m i j b
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 la unidad, ¡entra!
La unidad de DVD no tiene voz en 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 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 "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 .
¿Qué es una mejor herramienta?
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?
En realidad no, por dos razones.
Uno, se parece más a lo que es una mónada, porque
es
una mónada, pero sobre
(state -> *)
lugar de
*
.
Dos, si nos fijamos en el tipo de flecha de 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 tomado menos de medio siglo para cruzar la correspondencia Curry-Howard y convertirse en tipos Haskell.
El tipo de
returnIx
dice "puede lograr cualquier
returnIx
se
returnIx
, simplemente haciendo nada", que es la regla de la lógica de Hoare para "omitir".
La composición correspondiente es la regla de la lógica de Hoare para ";".
Terminemos observando el tipo de
bindIx
, colocando todos los cuantificadores.
bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i
Estos
forall
s tienen polaridad opuesta.
Elegimos el estado inicial
i
, y un cálculo que puede comenzar en
i
, con la condición posterior
a
.
El mundo elige cualquier estado intermedio que le guste, pero debe darnos la evidencia de que la condición posterior
b
cumple, y de cualquier estado, podemos continuar para hacerla esperar.
Entonces, en secuencia, podemos lograr la condición
b
desde el estado
i
.
Al liberar nuestro control sobre los estados "posteriores", podemos modelar cálculos
impredecibles
.
Tanto
IxMonad
como
MonadIx
son ú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 es a veces una realidad.
Con suerte, entonces, esta respuesta da alguna indicación de lo que son las mónadas indexadas, prediciendo tanto cuándo comienzan a ser útiles como 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 informáticos Bob Atkey, Conor McBride y Dominic Orchard, ya que así es como tiendo a pensar en ellas. Partes de estas construcciones tienen una historia mucho más larga e 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 sea demasiado esotérica.
Atkey
El estilo de mónada indexada de Bob Atkey es trabajar con 2 parámetros adicionales para tratar con el índice de la mónada.
Con eso obtienes las definiciones que la gente ha arrojado 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 à 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, utiliza un único 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 la 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 en
(m :: * -> *)
, la construimos sobre
(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 debe leer como "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
ibind
puede devolverle lo mismo que Atkey''s
ibind
.
Debe 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 buena 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 los endofunctores en la categoría de functores de
(k -> *)
a
(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. Yo personalmente uso un tipo de datos ''At'' para la construcción "clave" en el documento de McBride. De hecho, me acerqué a Bob Atkey en ICFP 2013 y mencioné que lo había vuelto del revés y lo había convertido en un "abrigo". Parecía visiblemente perturbado. La línea jugó mejor en mi cabeza. =)
Huerta
Finalmente, un tercer reclamante con menos referencias al nombre de "mónada indexada" se debe a Dominic Orchard, donde en su lugar utiliza un monoide de nivel de tipo para romper los índices. En lugar de pasar por los detalles de la construcción, simplemente vincularé a esta charla:
Puede ser importante observar cómo se usa la indexación en 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. Entonces 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 con
_<_
, y el tipo indica qué números son.
Luego, puede requerir que alguna función reciba un testigo 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 cierta lista está ordenada.
Las mónadas indexadas permiten codificar parte de lo que hacen los sistemas de tipos dependientes, para gestionar los efectos secundarios con mayor precisión.
Una mónada indexada no es una mónada específica como, por ejemplo, la mónada estatal, 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 de la computación.
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 estado de cálculo con
State sa
mantiene un estado de tipo
s
durante todo el 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
.
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.