Sistemas de E / S baseados em reinicialização?

8

Eu fui brincar com retomadas recentemente, principalmente a partir de papel clássico de Abramsky Refazendo alguns caminhos em Álgebra de Processos . Eles são bastante lisos (basicamente soluções para a equação de domínio ) e lembram muito as redes Kahn.R=I(O×R)

Certamente, essa observação não é original para mim - elas formam uma categoria monoidal traçada, e esse fato foi usado por Abramsky e Jagadeesan para dar semântica à lógica linear. De qualquer forma, observe que, se você alimentar uma retomada uma entrada do tipo I , obtém uma saída do tipo O e uma retomada atualizada r ' , que é o que permite modelar o fato de que um nó de fluxo de dados pode mudar à medida que vê entradas entre.rIOr

Como resultado, parece que eles poderiam fornecer uma API agradável para a construção de transdutores de E / S em uma linguagem de ordem superior como ML ou Haskell, mas não consigo encontrar documentos que descrevam isso. Mas eles já existem há décadas, e Gordon Plotkin os inventou, então não é como se eles estivessem na obscuridade. Então, eu queria saber se alguém os tinha visto fazer tanto uso.

Neel Krishnaswami
fonte
2
Enquanto lia a pergunta, pensei comigo mesma: "Aposto que Neel responderá a esta".
Andrej Bauer
Esse pode ser um bom caso de uso para operações e manipuladores no estilo Eff.
Andrej Bauer
@AndrejBauer: Eu sempre penso isso nas perguntas de Neel.
Dave Clarke

Respostas:

7

Isso se parece muito com a API de E / S descrita por Felleisen et al em Um sistema de E / S funcional (ou Fun for Freshman Kids) . Basicamente, você escreve (na configuração mais simples e não distribuída), uma série de manipuladores de eventos, cada um dos quais aceita o estado atual e retorna um estado atualizado. Finalmente, há um to-drawmanipulador, que produz a "saída" para cada estado.

Se reformularmos ligeiramente essa API, poderemos agrupar os manipuladores e o estado atual, e cada vez que um manipulador retorna um novo estado e um novo conjunto de manipuladores. Podemos chamar esse pacote de estado e operações de "objeto". :) Se fizermos do resultado um par desse objeto e da "saída", teremos exatamente o tipo de suposições.

Curiosamente, no artigo, Felleisen et al fazem exatamente isso ao passar para a configuração distribuída - toda operação retorna um par de novo estado e "saída" na forma de mensagens a serem enviadas aos outros participantes no sistema.

Sam Tobin-Hochstadt
fonte
5

Acabei de encontrar este post.

Volte ao início dos anos 80. Friedman et al. Indiana inventaram o conceito de 'motores' no contexto do Esquema 84 (não o Esquema 48). Um mecanismo é aproximadamente um elemento desse tipo:

E = Unit x Nats -> E + O

Você também pode usar I em vez de Unit e a parte x Nats é opcional. Você pode pensar neles como uma forma de suposições e, dependendo dos mecanismos de contexto, é mais prático do que as suposições.

Matthias
fonte
1
Obrigado! O Google me encontrou Haynes e Friedman, " Abstraindo a preempção cronometrada com motores" ( cs.indiana.edu/pub/techreports/TR178.pdf ) e "Engines from Continuations" de Dybvig e Hieb ( citeseerx.ist.psu.edu/viewdoc/ resumo? doi = 10.1.1.64.6124 ) Há outros árbitros que eu perdi?
Neel Krishnaswami