Como os futuros são descritos em termos de teoria de categorias?

Respostas:

25

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 ) UmB em que o r e t u r nA

return:AAbind:(AB)AB
return operação gera um processo que retorna imediatamente o seu argumento, e cria um novo processo que espera por um valor 's, aplica f a esse valor, e em seguida, aguarda o B -valor antes de retornar. Aproposta Promises / A para CommonJSchama a operação de ligação monádicae oScala 2.10 apenas fornece a interface monádica padrão.bindafBthen

O dual ao operador eventualmente é o operador sempre A da lógica temporal, que diz que a cada instante, você obtém um AAAA . 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 umAA , você sempre o terá. Isso funciona, mas é meio chato, IMO. :)A

A coisa mais natural (IMO) a fazer é tomar , o que lhe permite ter uma (potencialmente diferente) AAStreamAA 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.

Neel Krishnaswami
fonte
1
Eu adoraria obter uma cópia disso quando você terminar.
12118 Dave Clarke #
1
AA
Li recentemente que o tipo Scala Try[T]e Future[T]são duplos, mas ainda não entendi o que isso significa / em que sentido.
Giorgio