Existe uma descrição útil de futuros ou promessas em termos de teoria de categorias? Em particular, qual poderia ser o dual categórico do futuro?
fonte
Existe uma descrição útil de futuros ou promessas em termos de teoria de categorias? Em particular, qual poderia ser o dual categórico do futuro?
Por acaso, estou escrevendo um artigo sobre isso agora. Na OMI, uma boa maneira de pensar sobre futuros ou promessas é em termos da correspondência de Curry-Howard para lógica temporal .
Basicamente, a idéia por trás dos futuros é que é uma estrutura de dados que representa um cálculo em andamento e com o qual você pode sincronizar. Em termos de lógica temporal, este é o operador, eventualmente . Isto tem uma estrutura monadic: r e t u r n : Um → ◊ Uma b i n d : ( A → ◊ B ) → ◊ Um → ◊ B em que o r e t u r n
then
O dual ao operador eventualmente é o operador sempre ◻ A da lógica temporal, que diz que a cada instante, você obtém um A . Quando você passa de uma semântica Kripke da lógica temporal (onde você apenas modela a provabilidade) para uma semântica categorial de um cálcio (onde você também modela termos / provas lambda), verifica-se que existem várias maneiras de fazer isso.
A coisa mais simples que você pode fazer é tomar , alegando que uma vez que você tenha um , você sempre o terá. Isso funciona, mas é meio chato, IMO. :)
A coisa mais natural (IMO) a fazer é tomar , o que lhe permite ter uma (potencialmente diferente) A em cada instante. Então, você pode ver o estilo comonádico de programação reativa funcional (FRP) (proposto por Tarmo Uustalu e Varmo Vene ) como o estilo dual a monádico de programação com futuros.
No entanto, o comonádico
Nick Benton e eu defendemos a programação explícita com fluxos em nosso artigo Ultrametric Semantics of Reactive Programs . Posteriormente, Alan Jeffrey sugeriu o uso do LTL como um sistema de tipos em seu artigo LTL types FRP , uma observação que Wolfgang Jeltsch também fez em seu artigo Em direção a uma semântica categórica comum para lógica temporal temporal linear e programação reativa funcional .
A diferença entre a visão de Nick e eu e a de Alan e Wolfgang é melhor compreendida (IMO) comparando-se a construção apresentada em Birkedal et al. primeiros passos de Em Primeiros passos na teoria sintética de domínios guardados: indexação de etapas nos topos de árvores com o papel de Alan. As topos das árvores (preenchem os números naturais ordenados por tamanho) são muito semelhantes à categoria de espaços ultramétricos usados por Nick e eu, mas são muito mais fáceis de comparar com a categoria de Alan (preenchem uma categoria discreta de tempo), uma vez que ambos são pré-opostos categorias.
Se você estiver interessado em futuros especificamente para simultaneidade, talvez seja uma idéia melhor analisar CTL do que para o LTL. AFAIK, atualmente é um território inexplorado!
EDIT: aqui está um link para o rascunho . O artigo trata principalmente da implementação do FRP digitado, portanto o idioma é síncrono. Mas a maior parte da discussão sobre futuros / eventos na seção 3.3 deve se aplicar basicamente a idiomas verdadeiramente concorrentes também.
Try[T]
eFuture[T]
são duplos, mas ainda não entendi o que isso significa / em que sentido.