¿Cómo se describen los futuros en términos de teoría de categorías?

¿Existe una descripción útil de futuros o promesas en términos de teoría de categorías? En particular, ¿cuál podría ser el dual categórico del futuro?

Resulta que ahora estoy escribiendo un artículo sobre esto. En mi opinión, una buena manera de pensar sobre futuros o promesas es en términos de la correspondencia de Curry-Howard para la lógica temporal .

Básicamente, la idea detrás de los futuros es que es una estructura de datos que representa un cálculo que está en progreso y sobre el cual puede sincronizar. En términos de lógica temporal, esto es, finalmente, el operador . Tiene una estructura monádica: r e t u r n : A → ◊ A b i n d : ( A → ◊ B ) → ◊ A → ◊ B en el que la r e t u r $\Diamond A$

$$\begin{array}{lcl} \mathrm{return} & : & A \to \Diamond A \\ \mathrm{bind} & : & (A \to \Diamond{B}) \to \Diamond{A} \to \Diamond{B} \end{array}$$ $\mathrm{return}$desova de operación de un proceso que inmediatamente devuelve su argumento, y crea un nuevo proceso que espera a un valor 's, se aplica f a ese valor, y luego espera a que el B -valor antes de regresar. La propuesta Promises / A para CommonJS llama a la operación de enlace monádico , y Scala 2.10 simplemente le da la interfaz monádica estándar .$\mathrm{bind}$$a$$f$$B$then

La doble al operador el tiempo es el operador siempre ◻ Una de lógica temporal, que dice que a cada instante, se obtiene una A . Cuando pasa de una semántica de Kripke de lógica temporal (donde solo modela la demostrabilidad) a una semántica categorial de un cálculo λ (donde también modela términos / pruebas lambda), resulta que en realidad hay múltiples formas de hacerlo.$\Diamond{A}$$\Box{A}$$A$$\lambda$

Lo más simple que puede hacer es tomar , con el argumento de que una vez que tiene una A , siempre la tiene. Esto funciona, pero es un poco aburrido, en mi opinión. :)$\Box{A} \triangleq A$$A$

$\Box{A} \triangleq \mathsf{Stream}\;A$$A$

$\lambda$

Nick Benton y yo hemos argumentado a favor de la programación explícita con transmisiones en nuestro documento Semántica ultramétrica de programas reactivos . Posteriormente, Alan Jeffrey sugirió usar LTL como un sistema de tipos en su papel LTL type FRP , una observación que Wolfgang Jeltsch también hizo en su artículo Towards a Common Semical Canticics for Linear-Time Temporal Logical and Functional Reactive Programming .

La diferencia entre la opinión que adoptamos Nick y yo, y la que adoptan Alan y Wolfgang se entiende mejor (OMI) al comparar la construcción dada en los primeros pasos de Birkedal et al. En la teoría del dominio protegido sintético: indexación por pasos en los topos de árboles con el papel de Alan. El topos de los árboles (presheaves sobre los números naturales ordenados por tamaño) es muy similar a la categoría de espacios ultramétricos que usamos Nick y yo, pero mucho más fácil de comparar con la categoría de Alan (presheaves en una categoría de tiempo discreta), ya que ambos son presheaf categorías.

Sin embargo, si está interesado en futuros específicamente para la concurrencia, podría ser una mejor idea mirar CTL en lugar de LTL. AFAIK, ¡ese es un territorio actualmente inexplorado!

EDITAR: aquí hay un enlace al borrador . El documento trata principalmente sobre la implementación de FRP mecanografiado, por lo que el lenguaje es sincrónico. Pero la mayor parte de la discusión sobre futuros / eventos en la sección 3.3 debería aplicarse básicamente a lenguajes realmente concurrentes también.