¿Cuál es la multiplicación en la mónada de continuación?

Question

Dado un conjunto $S$ obtenemos un endofunctor $X \mapsto [[X,S],S]$ en $\mathbf{Set}$ . Esto se denomina mónada de continuación para $S$ así que supongo que eso significa que es una mónada. Hay un mapa natural $$\eta_X : X \rightarrow [[X,S],S]$$ que asigna a cada $x \in X$ al "evaluador" correspondiente $\eta_X(x)$ . Explícitamente viene dado por $$\eta_X(x) = (f \mapsto f(x)).$$

Vale, pero ¿cuál es la multiplicación? $$\mu_X : [[[[X,S],S],S],S] \rightarrow [[X,S],S]$$

Esto parece muy complicado; basta con decir el tipo de $\mu_X$ es difícil: "La función $\mu_X$ es una manera de girar (maneras de girar maneras de girar maneras de girar elementos de $X$ en elementos de $S$ en elementos de $S$ en elementos de $S$ en elementos de $S$ ) en (formas de convertir elementos formas de convertir elementos de $X$ en elementos de $S$ en elementos de $S$ )."

Answer 1

Dado $f\in [[[[X,S],S],S],S]$ y $g\in [X,S]$ define $\mu_X(f)(g) = f(\eta_{[X,S]}(g))$ .

¿Por qué es lo correcto? Bueno, el functor $[-,S]$ es (contravariantemente) autoadjunto, con la unidad igual al conit (en la categoría opuesta), y la mónada $[[-,S],S]$ surge de esta unión. Si resuelves lo que dice la definición de mónada inducida por una adjunción en este caso, obtienes la fórmula para el mapa unitario dada en tu pregunta y la fórmula para la multiplicación dada anteriormente.

Un poco de búsqueda sobre este tema me llevó a esta pregunta donde se señala que la tesis doctoral de Hayo Thielecke "Categorical Structure of Continuation Passing Style" podría ser una referencia pertinente.

Answer 2

Creo que primero ayuda pensar las cosas en términos de programación.

Así que tenemos $a$ de tipo $(((X\to S)\to S)\to S)\to S$ y queremos producir algo del tipo $(X\to S)\to S$ .

Muy bien, empezamos asumiendo que tenemos $b$ de tipo $X\to S$ . Ahora tenemos que hacer $S$ .

Podemos obtener un $S$ ya sea por tener un $X$ y aplicando $b$ o tener un $((X\to S)\to S)\to S$ y aplicando $a$ . Lo primero parece imposible, pero lo segundo puede ser factible. $\eta$ a la $b$ que hemos asumido.

Esto nos lleva exactamente a la función que también cita Alex: $$ \mu_X(a)(b) = a(\eta_{X\to S}(b)) $$

Más operativamente, hablando $(X\to S)\to S$ es una especie de promesa débil de un $X$ : algo que nos dará una $S$ si le prometemos que podemos convertir un $X$ en un $S$ para ello. Computacionalmente, esperamos que sea algo que o bien danos un $X$ conviértalo en un $S$ y devolver el $S$ lo consiguió, o acobardarse y darnos un $S$ que se metió de alguna otra manera furtiva. (Aunque no hay garantía que funcione así).

$a$ es entonces una promesa débil de una promesa débil de un $X$ . Pero queremos ser una débil promesa de un $X$ . Así que empezamos a correr $a$ -- si nos lanza un $S$ inmediatamente, entonces bien; lo devolveremos también. Si $a$ invoca su continuación, le dará una promesa débil $a'$ y podemos ejecutar $a'$ y obtener un $S$ (que devolvemos inmediatamente) o un $X$ que introduciremos en nuestra continuación.

Answer 3

Esta construcción no debe aplicarse sólo a la categoría de conjuntos, sino a cualquier categoría cartesiana cerrada. Pero esto nos sitúa en el ámbito de la lógica matemática. Podemos interpretar $X \to S$ como el tipo de implicaciones de $X$ a $S$ . En particular, si $S=0$ es el falsum, se obtiene el tipo de negación $\neg X$ . Utilizando esta interpretación lógica, quizá sea más fácil motivar la estructura de mónada. La unidad no es más que la implicación habitual $X \to \neg \neg X$ a la doble negación. Fíjate que aquí estamos en lógica constructiva.

Ahora, podemos aplicar $Y \to \neg \neg Y$ al caso especial $Y=\neg X$ y obtener $\neg X \to \neg \neg \neg X$ . Y ahora aplicamos $\neg$ en ambos lados (que es contravariante) para obtener $\neg \neg \neg \neg X \to \neg \neg X$ .

Éste era sólo el caso especial $S=0$ pero se puede escribir fácilmente la misma construcción para cualquier $S$ también de forma puramente teórica. El resultado es la fórmula dada por Alex Kruckman.

Answer 4

Una fórmula general para la mónada de continuación (C) multiplicación transformación natural (mult):

Dado un objeto Estado S y un objeto resultado R queremos un mapa desde (C comp C)S = C(C S) = R^(R^(R^(R^S))) a (C S) = R^(R^S) así que construye

    u(at S): (R^S) * (R^(R^(R^(R^S)))) -> R = 
    (R^S) * (R^(R^(R^(R^S)))); unit(at R^S) * id; (R^(R^(R^S)) * (R^(R^(R^(R^S))));
    eval; R 

y tomar su transformada (lambda) para obtener:

    mult(at (C C)S) = \u: R^(R^(R^(R^S))) -> R^(R^S)

Compruebe que el unit y mult las transformaciones naturales hacen de C (como) un monoide:

    (C unit; mult) = (unit C; mult) = id.

Aquí punto y coma significa composición del mapa de izquierda a derecha: a;b significa a seguido de b . Es perfectamente razonable componer un objeto con un mapa (o un mapa con un objeto), ya que un objeto puede interpretarse como su correspondiente mapa de identidad.

Un nombre de functor yuxtapuesto a un nombre de transformación natural es la notación estándar para la composición de una transformación natural y un functor. Así, (C unit) transforma C a (C comp C) al igual que (unit C) ; mult entonces transforma (C comp C ) a C . La mayoría de los autores utilizan la yuxtaposición de nombres de funtores para denotar la composición de funtores, así (C C) = (C comp C) = $(C\circ C)$ .

La notación de transformación lambda:

    given f: f: A*B -> C
    \f : B -> C^A 

Los functores (A * - ) y (-^A) son contiguos.