Sistem IO berbasis resume?

8

Saya telah bermain-main dengan resumptions akhir-akhir ini, sebagian besar dari karya klasik Abramsky Retracing Some Paths in Process Algebra . Mereka cukup licin (pada dasarnya solusi untuk persamaan domain ), dan sangat mengingatkan pada jaringan Kahn.R=I(O×R)

Tentu saja, pengamatan ini tidak asli bagi saya --- mereka membentuk kategori monoid yang dilacak, dan fakta ini digunakan oleh Abramsky dan Jagadeesan untuk memberikan semantik pada logika linier. Bagaimanapun, perhatikan bahwa jika Anda memberi makan input tipe , Anda mendapatkan output tipe dan , yang memungkinkan Anda memodelkan fakta bahwa node aliran data dapat berubah saat melihat input masuk.rIOr

Hasilnya, sepertinya mereka bisa memberikan API yang bagus untuk membangun transduser I / O dalam bahasa tingkat tinggi seperti ML atau Haskell, tapi sepertinya saya tidak dapat menemukan makalah yang menggambarkan hal semacam itu. Tapi mereka sudah ada selama beberapa dekade, dan Gordon Plotkin menemukan mereka, jadi itu tidak seperti mereka merana dalam ketidakjelasan. Jadi saya bertanya-tanya apakah ada yang melihat mereka menggunakan seperti itu.

Neel Krishnaswami
sumber
2
Ketika saya membaca pertanyaan itu, saya berpikir, "Saya yakin Neel akan menjawab pertanyaan ini".
Andrej Bauer
Ini mungkin kasus penggunaan yang bagus untuk operasi dan penangan gaya Eff.
Andrej Bauer
@AndrejBauer: Saya selalu memikirkan itu untuk pertanyaan Neel.
Dave Clarke

Jawaban:

7

Ini sangat mirip dengan API I / O yang dijelaskan oleh Felleisen et al dalam Sistem I / O Fungsional (atau Fun for Freshman Kids) . Pada dasarnya, Anda menulis (dalam pengaturan yang lebih sederhana, tidak terdistribusi), serangkaian penangan acara, yang masing-masing menerima keadaan saat ini, dan mengembalikan keadaan yang diperbarui. Akhirnya, ada to-drawhandler, yang menghasilkan "output" untuk setiap negara.

Jika kami menyusun kembali API ini sedikit, kami dapat mengemas penangan dan kondisi saat ini bersama-sama, dan setiap kali penangan mengembalikan negara baru dan satu set penangan baru. Kami mungkin menyebut paket negara dan operasi ini sebagai "objek". :) Jika kita kemudian membuat hasilnya sebagai pasangan dari objek ini, dan "output", maka kita memiliki jenis pengembalian yang tepat.

Menariknya, di koran, Felleisen et al melakukan hal ini ketika pindah ke pengaturan terdistribusi - setiap operasi mengembalikan sepasang status baru dan "output" dalam bentuk pesan yang akan dikirim ke peserta lain dalam sistem.

Sam Tobin-Hochstadt
sumber
5

Baru saja menemukan posting ini.

Kembali ke awal 1980-an. Friedman et al @ Indiana menemukan konsep 'mesin' dalam konteks Skema 84 (bukan Skema 48). Mesin kira-kira merupakan elemen dari jenis ini:

E = Unit x Nats -> E + O

Anda juga dapat menggunakan I sebagai ganti Unit dan bagian x Nat adalah opsional. Anda dapat menganggap ini sebagai bentuk resume, dan tergantung pada konteks mesin lebih praktis daripada resume.

Matthias
sumber
1
Terima kasih! Google menemukan saya Haynes dan Friedman, "Abstraksi Preemption Berwaktu dengan Mesin" ( cs.indiana.edu/pub/techreports/TR178.pdf ), dan "Mesin dari Kelanjutan" dari Dybvig dan Hieb ( citeseerx.ist.psu.edu/viewdoc/ ringkasan? doi = 10.1.1.64.6124 ) Apakah ada referensi lain yang saya lewatkan?
Neel Krishnaswami