¿Hasta qué punto se determinan de forma única las instancias aplicativas/Mónadas?

Dado que cada Applicative tiene una Backwards contraparte,

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 Applicative esté determinado de manera única, al igual que (y esto está muy lejos de no estar relacionado) muchos conjuntos se extienden a los monoides de múltiples maneras.

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

Mientras tanto, en algún maravilloso trabajo reciente (que visto en una escuela de verano hace unos meses), Tarmo Uustalu mostró una manera bastante clara de manejar este problema, al menos cuando el funtor 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 funtores F similares a contenedores de manera uniforme, como determinados por dos componentes

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

Hasta el isomorfismo, las estructuras de datos de contenedores en F X 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 lee -> como exponenciación inversa). El triángulo se supone que te recuerda a un árbol nodo lateralmente, con un elemento s : S etiquetando el ápice, y la línea de base representando el conjunto de posición P s. Decimos que algún funtor es un contenedor si es isomorfo a algún S <| P.

En Haskell, puedes fácilmente tomar S = F (), pero construir P puede tomar un poco de mecanografía. 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 polinómicos habituales, así como identidad,

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

Composición, donde una forma completa está hecha de una sola forma exterior y una forma interior para cada posición exterior, {[45]]}

(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 una forma interna (por lo que "exterior" e "interior" 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-todas-de-la-misma-forma", por ejemplo, [] (X) [] significa rectangular listas-de-listas. Pero yo digress

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 que asigna posiciones de salida a posiciones de entrada.

Nuestra función polimórfica es entonces{[45]]}

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

Donde la forma de salida se calcula a partir de la forma de entrada, luego las posiciones de salida se llenan recogiendo elementos de las posiciones de entrada.

(Si eres Peter Hancock, tienes otra metáfora para lo que está pasando. Las formas son Comandos; Las Posiciones son Respuestas; un morfismo de contenedor es un controlador de dispositivo , traduciendo comandos de una manera, luego responde de la otra.)

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

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

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

¿Qué pasa con Applicative?Nos perdimos un poco en el camino, construyendo toda esta maquinaria. Pero ha valido la pena. Cuando los funtores subyacentes para mónadas y aplicativos son contenedores, las funciones polimórficas pure y <*>, return y join debe ser representable por the relevant notion of container morphism.

Tomemos primero los aplicativos, 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 compruebas que las leyes aplicables, encuentras que necesitamos exactamente un monoide. Equipar un recipiente con estructura aplicativa es exactamente refinar las estructuras monoides en sus formas con las adecuadas operaciones que respetan la posición. No hay nada que hacer para unit (porque no hay chocie de la posición de la fuente), pero para mult, necesitamos que whenenver

multS (s0, s1) = s

Tenemos

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

Satisfacer las condiciones apropiadas de identidad y asociatividad. Si cambiamos a la interpretación de Hancock, estamos definiendo un monoide (skip, punto y coma) para los comandos, donde no hay manera de mirar la respuesta al primer comando antes de elegir el segundo, como los comandos son una baraja de tarjetas perforadas. Tenemos que ser capaces de dividir las respuestas a 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 muchos monoides entre los que elegir. Incluso si las formas viven en Bool, tenemos un poco de elección.

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

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

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

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

Está desequilibrado porque tenemos un montón de formas a la derecha, no solo una. Si cambiamos a la interpretación de Hancock, estamos definiendo una especie de composición secuencial para comandos, donde dejamos que el segundo comando sea elegido sobre la base de la primera respuesta, como si estuviéramos interactuando en un teletipo. Más geométricamente, estamos explicando cómo glom dos capas de un árbol en uno. Sería muy sorprendente si tal las composiciones eran únicas.

Nuevamente, para las posiciones, tenemos que mapear posiciones de salida individuales a pares de una manera coherente. Esto es más complicado para las mónadas: primero elegimos una posición exterior (respuesta), luego tenemos que elegir una posición interior(respuesta) adecuada a la forma (comando) encontrada en la primera posición (elegida después de la primera respuesta).

Me encantaría enlazar con el trabajo de Tarmo para los detalles, pero no parece haber salido a la calle todavía. Él realmente 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 periódico!

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