haskell - monadologia - ¿En qué medida se determinan de forma única las instancias de Aplicación/Mónada?

monadas filosofia

Question

Como se describe en esta pregunta / respuestas , las instancias de Functor se determinan de forma única, si existen.

Para las listas, hay dos ejemplos de aplicaciones bien conocidas: [] y ZipList . Por lo tanto, Applicative no es único (consulte también ¿Puede GHC derivar instancias de Functor y Applicative para un transformador de mónada? ¿Por qué no hay -XDeriveApplicative extensión -XDeriveApplicative ? ). Sin embargo, ZipList necesita listas infinitas, ya que su pure repite un elemento dado de forma indefinida.

• ¿Hay otros ejemplos, quizás mejores, de estructuras de datos que tengan al menos dos instancias Applicative ?
• ¿Existen ejemplos de este tipo que solo involucren estructuras de datos finitos? Es decir, como si, hipotéticamente, el sistema de tipos de Haskell distinguiera los tipos de datos inductivos y coinductive , ¿sería posible determinar el Aplicativo de forma única?

Yendo más lejos, si pudiéramos extender tanto [] como ZipList a una Mónada, tendríamos un ejemplo donde una mónada no está determinada únicamente por el tipo de datos y su Functor. Por desgracia, ZipList tiene una instancia de ZipList solo si nos limitamos a listas infinitas ( streams ). Y el return para [] crea una lista de un solo elemento, por lo que requiere listas finitas. Por lo tanto:

• ¿Las instancias de Monad están determinadas únicamente por el tipo de datos? ¿O hay un ejemplo de un tipo de datos que puede tener dos instancias distintas de Monad?

En el caso de que haya un ejemplo con dos o más instancias distintas, surge una pregunta obvia, si deben / pueden tener la misma instancia aplicativa:

• ¿Las instancias de la mónada están determinadas únicamente por la instancia del solicitante, o hay un ejemplo de un aplicativo que puede tener dos instancias de la mónada distintas?
• ¿Hay un ejemplo de un tipo de datos con dos instancias de Monad distintas, cada una con una súper instancia de Applicative diferente?

Y finalmente podemos hacer la misma pregunta para Alternative / MonadPlus. Esto se complica por el hecho de que hay dos conjuntos distintos de leyes MonadPlus . Suponiendo que aceptamos uno de los conjuntos de leyes (y para el Aplicativo aceptamos la distribución / absorción derecha / izquierda , vea también esta pregunta ),

• ¿La Alternativa está determinada únicamente por Applicative, y MonadPlus por Monad, o hay algún contra-ejemplo?

Si alguno de los anteriores es único, me gustaría saber por qué, para tener una pista de una prueba. Si no, un contra-ejemplo.

Answer 1

Dado que cada Applicative tiene una contraparte al Backwards ,

newtype Backwards f x = Backwards {backwards :: f x}
instance Applicative f => Applicative (Backwards f) where
  pure x = Backwards (pure x)
  Backwards ff <*> Backwards fs = Backwards (flip ($) <$> fs <*> ff)

es inusual que el Applicative esté determinado de manera única, así como (y esto está muy lejos de no estar relacionado) muchos conjuntos se extienden a los monoides de múltiples maneras.

En esta respuesta , establezco el ejercicio de encontrar al menos cuatro instancias de Solicitantes válidas distintas para listas no vacías: no lo estropearé aquí, pero daré una gran pista sobre cómo cazar.

Mientras tanto, en un trabajo reciente maravilloso (que vi en una escuela de verano hace unos meses), Tarmo Uustalu mostró una manera bastante clara de manejar este problema, al menos cuando el functor subyacente es un contenedor , en el sentido de Abbott, Altenkirch y Ghani.

Advertencia: ¡Tipos dependientes por delante!

¿Qué es un contenedor? Si tiene tipos dependientes a mano, puede presentar los funtores F similares a los contenedores de manera uniforme, según lo determinen dos componentes

1. un conjunto de formas, S: conjunto
2. un conjunto de posiciones indexadas en S, P: S -> Establecer

Hasta el isomorfismo, las estructuras de datos del contenedor en FX están dadas por el par dependiente de alguna forma s: S, y alguna función e: P s -> X, que le indica el elemento ubicado en cada posición. Es decir, definimos la extensión de un contenedor.

(S <| P) X = (s : S) * (P s -> X)

(que, por cierto, se parece mucho a una serie de potencias generalizadas si lees -> como exponencia inversa). Se supone que el triángulo le recuerda a un nodo de árbol lateralmente, con un elemento s: S que etiqueta el vértice, y que la línea de base representa el conjunto de posición P s. Decimos que algún funtor es un contenedor si es isomorfo a algún S <| P S <| P

En Haskell, puedes tomar fácilmente S = F () , pero la construcción de P puede requerir un poco de pirateo de tipos. Pero eso es algo que puedes probar en casa. Encontrará que los contenedores están cerrados bajo todas las operaciones de formación de tipos polinomiales habituales, así como la identidad,

Id ~= () <| / _ -> ()

composición, donde una forma completa está hecha de una sola forma externa y una forma interna para cada posición externa,

(S0 <| P0) . (S1 <| P1)  ~=  ((S0 <| P0) S1) <| / (s0, e0) -> (p0 : P0, P1 (e0 p0))

y algunas otras cosas, notablemente el tensor , donde hay una forma externa y otra interna (de modo que "exterior" e "interno" son intercambiables)

(S0 <| P0) (X) (S1 <| P1)   =   ((S0, S1) <| / (s0, s1) -> (P0 s0, P1 s1))

de modo que F (X) G significa " F -estructuras de G -estructuras de la misma forma", por ejemplo, [] (X) [] significa listas de listas rectangulares . Pero yo divago

Funciones polimórficas entre contenedores Cada función polimórfica

m : forall X. (S0 <| P0) X -> (S1 <| P1) X

Se puede implementar mediante un morfismo de contenedor , construido a partir de dos componentes de una manera muy particular.

1. una función f : S0 -> S1 mapeando formas de entrada a formas de salida;
2. una función g : (s0 : S0) -> P1 (f s0) -> P0 s0 mapeando las posiciones de salida a las posiciones de entrada.

Nuestra función polimórfica es entonces.

/ (s0, e0) -> (f s0, e0 . g s0)

donde la forma de salida se calcula a partir de la forma de entrada, las posiciones de salida se rellenan seleccionando elementos de las posiciones de entrada.

(Si eres Peter Hancock, tienes otra metáfora de lo que está pasando. Las formas son comandos, las posiciones son respuestas; un morfismo de contenedor es un controlador de dispositivo , que traduce los comandos de una manera, luego responde el otro).

Cada morfismo de contenedor le da una función polimórfica, pero lo contrario también es cierto. Dada tal m, podemos tomar

(f s, g s) = m (s, id)

Es decir, tenemos un teorema de representación , que dice que cada función polimórfica entre dos contenedores viene dada por tal par, f , g .

¿Qué hay del Applicative ? Nos perdimos un poco en el camino, construyendo toda esta maquinaria. Pero ha merecido la pena. Cuando los funtores subyacentes para las mónadas y los aplicativos son contenedores, las funciones polimórficas pure y <*> , return y join deben ser representadas por la noción relevante de morfismo del contenedor.

Tomemos los aplicativos primero, usando su presentación monoidal. Necesitamos

unit : () -> (S <| P) ()
mult : forall X, Y. ((S <| P) X, (S <| P) Y) -> (S <| P) (X, Y)

Los mapas de izquierda a derecha para formas requieren que entreguemos

unitS : () -> S
multS : (S, S) -> S

así que parece que podríamos necesitar un monoide. Y cuando verifica que las leyes aplicables, descubra que necesitamos exactamente un monoide. Equipar un contenedor con estructura aplicativa es refinar exactamente las estructuras monoides en sus formas con operaciones adecuadas que respetan la posición. No hay nada que hacer por unit (porque no hay una posición de origen), pero para mult , necesitamos que cuando suceda

multS (s0, s1) = s

tenemos

multP (s0, s1) : P s -> (P s0, P s1)

Satisfacer las condiciones adecuadas de identidad y asociatividad. Si cambiamos a la interpretación de Hancock, estamos definiendo un monoide (saltar, punto y coma) para los comandos, donde no hay manera de ver la respuesta al primer comando antes de elegir el segundo, ya que los comandos son una baraja de cartas perforadas. Tenemos que ser capaces de dividir las respuestas de los comandos combinados en las respuestas individuales a los comandos individuales.

Entonces, cada monoide en las formas nos da una estructura aplicativa potencial. Para las listas, las formas son números (longitudes), y hay una gran cantidad de monoides para elegir. Incluso si las formas viven en Bool , tenemos bastante elección.

¿Qué pasa con Monad ? Mientras tanto, para las mónadas M con M ~= S <| P M ~= S <| P Necesitamos

return : Id -> M
join   : M . M -> M

Mirando primero las formas, eso significa que necesitamos una especie de monoide ladeado.

return_f : () -> S
join_f   : (S <| P) S -> S  --  (s : S, P s -> S) -> S

Es desequilibrado porque tenemos un montón de formas a la derecha, no solo una. Si cambiamos a la interpretación de Hancock, estamos definiendo un tipo de composición secuencial para los comandos, donde permitimos que el segundo comando se elija sobre la base de la primera respuesta, como si estuviéramos interactuando en un teletipo. Más geométricamente, estamos explicando cómo agrupar dos capas de un árbol en una. Sería muy sorprendente si tales composiciones fueran únicas.

Nuevamente, para las posiciones, tenemos que asignar posiciones de salida individuales a pares de una manera coherente. Esto es más complicado para las mónadas: primero elegimos una posición externa (respuesta), luego tenemos que elegir una posición interna (respuesta) apropiada para la forma (comando) que se encuentra en la primera posición (elegida después de la primera respuesta).

Me encantaría enlazar con el trabajo de Tarmo para conocer los detalles, pero no parece que haya salido a la calle todavía. En realidad, ha utilizado este análisis para enumerar todas las estructuras de mónadas posibles para varias opciones de contenedor subyacente. Estoy deseando que llegue el papel!

Editar. En honor a la otra respuesta, debo observar que cuando en todas partes P s = () , entonces (S <| P) X ~= (S, X) y las estructuras de mónada / aplicativo coinciden exactamente entre sí y con Las estructuras monoides en S Es decir, para las mónadas escritores, solo tenemos que elegir las operaciones de nivel de forma, porque hay exactamente una posición para un valor en cada caso.

Answer 2

Primero, dado que los Monoid no son únicos, tampoco lo son los Writer Monad o los Applicative . Considerar

data M a = M Int a

entonces puede darle instancias de Applicative y Monad isomorfas a cualquiera de:

Writer (Sum Int)
Writer (Product Int)

Dada una instancia de Monoid para un tipo s , otro par isomorfo con diferentes instancias de Applicative / Monad es:

ReaderT s (Writer s)
State s

En cuanto a tener una instancia Applicative extienda a dos Monad diferentes, no puedo recordar ningún ejemplo. Sin embargo, cuando intenté convencerme completamente de si ZipList realmente no se puede convertir en una Monad , encontré la siguiente restricción bastante fuerte que se aplica a cualquier Monad :

join (fmap (/x -> fmap (/y -> f x y) ys) xs) = f <$> xs <*> ys

Sin embargo, eso no da una join para todos los valores: en el caso de las listas, los valores restringidos son aquellos en los que todos los elementos tienen la misma longitud, es decir, listas de listas con forma "rectangular".

(Para las mónadas de Reader , donde la "forma" de los valores monádicos no varía, estos son, de hecho, todos los valores m (mx) , por lo que tienen una extensión única. EDITAR: Piénselo bien, Either , Maybe y Writer también tienen solo valores m (mx) "rectangulares", por lo que su extensión de Applicative a Monad también es única.)

Sin embargo, no me sorprendería si existiera un Applicative con dos Monad .

Para Alternative / MonadPlus , no puedo recordar ninguna ley para los casos que utilizan la ley de Distribución a la Izquierda en lugar de Left Catch, no veo nada que le impida simplemente intercambiar (<|>) con flip (<|>) . No sé si hay una variación menos trivial.

ADENDA: De repente recordé que había encontrado un ejemplo de un Applicative con dos Monad . Es decir, listas finitas. Existe la instancia habitual de Monad [] , pero luego puede reemplazar su join por la siguiente función (haciendo que las listas vacías sean "infecciosas"):

ljoin xs
  | any null xs = []
  | otherwise   = concat xs

(Por desgracia, las listas deben ser finitas porque, de lo contrario, la comprobación null nunca terminará, y eso arruinaría la join . fmap return == id law).

Esto tiene el mismo valor que join / concat en listas rectangulares de listas, por lo que le daremos el mismo Applicative . Como recuerdo, resulta que las primeras dos leyes de la mónada son automáticas a partir de eso, y usted solo necesita marcar el ljoin . ljoin == ljoin . fmap ljoin ljoin . ljoin == ljoin . fmap ljoin ljoin . ljoin == ljoin . fmap ljoin .