Prism: bahasa fungsional non-pure dengan efek bertipe

• Prism adalah compiler eksperimental yang tidak menyembunyikan efek seperti variabel mutable, exception, dan stream, melainkan menampilkannya di tipe, sambil tetap mempertahankan perubahan lokal yang tidak dapat diamati dari luar sebagai tipe murni seperti Int -> Int
• Intinya adalah algebraic effect handlers dan row polymorphism, di mana efek digabungkan ke dalam row pada tipe fungsi dan handler hanya menangani label yang diperlukan lalu meneruskan sisanya
• Sistem efek yang sama mengekspresikan exception, generator/stream, lens, state var, serta alur fail/guard, dan beberapa jalur dapat diturunkan tanpa list perantara atau komposisi runtime
• Dari sisi performa, ia menggabungkan evidence passing dan reference counting Perceus untuk menghindari alokasi per pemanggilan efek, serta mengoptimalkan pembaruan fungsional pada nilai dengan kepemilikan unik menjadi perubahan in-place
• Prism juga menyediakan LLVM IR, MLIR, runtime C, interpreter Rust, model Lean 4, dan playground WASM sehingga hasil inferensi tipe dan lowering dapat diperiksa langsung

---

Perubahan yang tidak terlihat dari luar dan efek bertipe

• Titik awal Prism adalah bahwa fungsi fib yang memakai var dan assignment di dalamnya pun dapat terlihat seperti fungsi murni bagi pengamat luar
  • Contoh fib memperbarui dua variabel secara in-place, tetapi tidak mengekspos state ke luar fungsi
  • Tipenya adalah Int -> Int, dan efeknya tidak muncul di tipe
• Prism adalah compiler fungsional proof-of-concept yang dikembangkan selama tiga tahun terakhir, memodelkan efek berdasarkan ide tipe modern dari OCaml 5, Haskell, dan keluarga Koka
• Arah utamanya bukan menghindari efek, melainkan memasukkan efek ke dalam sistem tipe dan mengoptimalkannya agar biaya tersebut dihilangkan oleh compiler

Efek bekerja seperti interface

• Efek di Prism menggunakan pendekatan algebraic effect handlers: operasi dideklarasikan, lalu handler memberi makna pada operasi tersebut
  • effect Gen { ctl yield(Int) : Unit } mendeklarasikan operasi yield
  • fn produce(n) : !{Gen} Unit menandai di tipe bahwa fungsi tersebut melakukan yield
• Bahkan untuk producer yang sama, maknanya ditafsirkan berbeda tergantung bagaimana continuation k ditangani
  • total menjumlahkan nilai yield
  • count menghitung berapa kali yield dipanggil
  • Jika k dibuang hasilnya menjadi exception, jika dipanggil sekali menjadi state atau generator, dan jika dipanggil beberapa kali menjadi perilaku pencarian
• Contoh efek Amb mengekspresikan pencarian triple Pythagoras dengan choose dan reject
  • choose(n) menyediakan nilai dalam rentang 0..n-1
  • Handler melanjutkan continuation yang sama untuk setiap kandidat sehingga membentuk pohon pencarian
• Berbeda dengan OCaml 5, Prism memasukkan efek ke dalam tipe, dan tidak perlu menaikkan lapisan secara manual seperti monad transformer stack di Haskell
  • Effect row digabungkan secara struktural sepanjang pemanggilan
  • Ia bertindak seperti himpunan label, bukan stack

Fitur-fitur yang diekspresikan dengan satu mekanisme

• Exception

  • Di Prism, exception adalah handler yang membuang continuation
  • Klausa final ctl membuang k dan menjadikan nilai di badan klausa tersebut sebagai hasil handler
  • Bukan pendekatan propagasi Result atau menabur ? di call stack
  • Karena exception adalah label di effect row, ia dikomposisikan sebagai exception yang dapat diperluas
  • Setiap kegagalan adalah operasi terpisah, dan row pada tipe fungsi menunjukkan exception yang dapat keluar
  • Dalam contoh Abort dan Timeout, fetch memiliki !{Abort, Timeout}
  • with_default hanya menangani Timeout, mengembalikan fallback "cached", dan setelah ditangani tipenya tinggal !{Abort}
  • Berbeda dari checked exception Java, ini tidak terikat pada hierarki kelas dan bekerja sebagai himpunan struktural yang terbuka

• Generator dan stream

  • Stream tersusun dari producer yang melakukan emit, transformer yang menangkap lalu memancarkannya lagi, dan consumer yang melakukan fold
  • Karena pipeline berbentuk handler yang dinest di sekitar satu producer, list perantara secara struktural tidak terbentuk
  • Contoh: srange(1, n).smap(square).skeep(even).stake(5).ssum()
  • Penghentian awal seperti stake(5) adalah handler yang membuang continuation setelah memperoleh nilai yang dibutuhkan
  • Library stream ini dipengaruhi oleh pipes dan conduit di Haskell

• Lens

  • Lens di Prism bukan library terpisah, melainkan kombinasi jalur pembaruan record dan model memori
  • Di record bersarang, beberapa field yang dalam bisa diperbarui lewat satu ekspresi path
  • Contoh: { g | player.pos.x = 30, player.hp = 95, score = 110 }
  • Spine record bersarang dibangun ulang, tetapi jika nilainya dimiliki secara unik maka sel yang telah diurai digunakan kembali
  • Struktur ini memungkinkan pembaruan fungsional dikompilasi menjadi penulisan pointer
  • Tidak ada alokasi atau komposisi optic type saat runtime
  • deriving (Lens) menghasilkan accessor fungsi biasa seperti score_of dan with_score

• State mutable

  • var didesugar menjadi operasi get/set dari private effect
  • Handler yang dipasang di akhir blok menangani efek ini
  • Analisis closure escape menolak kasus ketika state dapat lolos ke luar
  • Fungsi yang menaunginya dapat tetap mempertahankan effect row kosong

• Kegagalan

  • Kegagalan direpresentasikan sebagai efek anonim Fail, dan sistem tipe menangani bahwa “ekspresi ini mungkin tidak menghasilkan nilai”
  • fail() melakukan kegagalan, dan guard(cond) gagal ketika kondisi bernilai false
  • ?? memakai fallback ketika sisi kiri gagal
  • ?. menelusuri rantai opsi lalu berhenti singkat
  • Guard pada comprehension memangkas elemen yang gagal alih-alih crash
  • Karena var juga sugar berbasis handler, blok transact dapat mengambil snapshot variabel aktif dan rollback saat gagal

Fitur tipe modern

• Prism memakai inferensi tipe higher-rank bidirectional ala Dunfield-Krishnaswami agar sebagian besar kode tidak perlu menuliskan anotasi tipe
• Pada batas yang memerlukan polimorfisme orde lebih tinggi, binder dinyatakan eksplisit dengan forall
  • pick(g : forall a. (a) -> a) dapat menerapkan g baik ke Bool maupun Int
  • Dalam core Damas-Milner, a akan disatukan menjadi Bool pada pemanggilan pertama sehingga pemanggilan kedua ditolak
• Polimorfisme ad-hoc diekspresikan sebagai type class bergaya Lean
  • Instance adalah nilai bernama
  • given Ord(a) meminta dictionary
  • Jika ada beberapa instance, satu dapat ditandai canonical dan yang lain dinyatakan eksplisit dengan using
• deriving menghasilkan instance dan accessor field yang berulang seperti Eq, Ord, Show, dan Lens
• Pattern matching juga terhubung dengan class
  • pattern First(n) for Peek = view peek adalah pola yang memakai method class sebagai view
  • head_or dapat memakai pola yang sama untuk berbagai tipe yang memiliki instance Peek
• show bekerja secara type-directed tanpa class terpisah
  • Compiler mensintesis printer struktural dari tipe statis
  • Ia tidak membaca tag tipe runtime untuk menentukan cara menampilkan
• Effect row juga polimorfik
  • fn twice(f : (Unit) -> Int ! {| e}) menjumlahkan hasil fungsi argumen apa pun effect row e-nya
  • Untuk thunk murni, e disatukan dengan row kosong {}
  • Untuk thunk yang melakukan efek seperti Tick atau Say, row tersebut diteruskan apa adanya

Cara kompilasi untuk menurunkan biaya efek

• Implementasi algebraic effect yang bersifat textbook dapat menyusun ulang komputasi menjadi pohon berbentuk free monad dan mungkin mengalokasikan sel kecil pada setiap operasi
• Jalur cepat Prism adalah evidence passing ala keluarga Koka
  • Alih-alih menyusun ulang komputasi untuk mencari handler, klausa handler yang aktif diteruskan ke setiap titik operasi seperti parameter biasa
  • do op diturunkan menjadi pemanggilan langsung
  • Saat memasang handler hanya satu closure yang dialokasikan, jadi biayanya O(handlers) dan tidak proporsional terhadap jumlah operasi
• Encoding free monad tetap ada sebagai fallback
  • untuk komputasi yang keluar sebagai struktur data
  • untuk resumption multishot yang sesungguhnya
  • dan untuk pola seperti masked handler
• Pipeline stream menghitung effect evidence yang diperlukan melintasi batas fungsi melalui interprocedural flow analysis
  • Evidence di-thread melalui producer dan transformer
  • Seluruh rantai diturunkan menjadi satu loop tunggal
  • Tidak ada list perantara maupun alokasi sel per operasi
• Struktur ini memberi hasil mirip stream fusion di Haskell atau monomorfisasi adapter iterator Rust, tetapi diperoleh dari compiler efek

Model memori dan runtime

• Prism menggunakan reference counting Perceus
  • Sel heap dibebaskan secara deterministik pada titik yang diketahui secara statis
  • Tidak ada pause atau tracing
• Frame-limited reuse mengembalikan sel yang baru saja diurai lewat pattern match ke sisi konstruktor
  • map pada list dengan kepemilikan unik terlihat seperti fungsi murni yang mengembalikan list baru, tetapi sebenarnya dapat diubah in-place
  • Mekanisme yang sama juga membuat pembaruan lens dapat dikompilasi menjadi penulisan pointer
• Struktur runtime mirip disiplin memori Lean 4, tetapi Prism mengeluarkan LLVM IR
  • LLVM IR dihasilkan melalui inkwell
  • Untuk program yang sama, modul MLIR tekstual juga dihasilkan
  • Hasilnya kemudian di-link oleh clang dengan runtime C tulisan tangan prism_rt.c
• prism_rt.c adalah runtime kecil sekitar 2 ribu baris
  • Sel heap berbentuk struktur 4 word atau lebih: { refcount, tag, arity, fields... }
  • Termasuk allocator, rc_inc/rc_dec, allocator reuse in-place, serta primitive bignum dan string
  • Tidak ada collector thread, card table, atau safepoint
• Allocator default adalah malloc dari libc, dengan konfigurasi mimalloc opt-in untuk benchmarking
• Live-cell oracle melakukan assert bahwa heap balance adalah 0 saat terminasi, sehingga test suite dapat memverifikasi sifat bebas garbage

Model Lean dan verifikasi backend

• Interpreter Prism berasal dari keluarga CEK machine, dan mesin ini tercermin dalam model Lean 4 models/Prism.lean
• Model Lean 4 memiliki teorema terverifikasi secara mekanis bahwa relasi small-step bersifat deterministik
  • Program selalu maju ke tepat satu state berikutnya
• Interpreter yang diimplementasikan di Rust juga dipakai sebagai differential oracle
  • Semua program dalam corpus harus lolos melalui interpreter serta backend LLVM, MLIR, dan binary hasil link C
  • Build hanya lolos bila keluaran keempat hasil tersebut identik byte demi byte
• Determinisme ini menjadi dasar bagi replayable durable execution
  • Gagasannya adalah jika input tetap dan eksekusi direkam, maka replay bit-for-bit dimungkinkan
  • Pada versi mendatang, Prism dibayangkan dapat memeriksa keamanan replay pasca-crash sebagai properti tipe

Playground WASM dan sumber kode

• Interpreter yang sama juga dikompilasi ke WASM sehingga kode Prism dapat dijalankan tanpa instalasi di playground
• Playground menjalankan program di worker
• Tombol-tombolnya dapat menampilkan hasil dump anotasi tipe yang diinferensikan, effect row, dan core IR yang telah diturunkan
  • Ini memungkinkan melihat bentuk lowering sebenarnya dari loop var atau pipeline stream
• Contoh-contoh dalam artikel juga tersedia di dropdown
• Seluruh source code, model Lean, dan runtime C tersedia di prism repository on GitHub

Silsilah implementasi dan karakter proyek

• Core IR Prism adalah keluarga call-by-push-value yang didasarkan pada Call-by-Push-Value: A Functional/Imperative Synthesis karya Levy
• Jalur efek cepatnya dekat dengan Generalized Evidence Passing for Effect Handlers dan Effect Handlers, Evidently karya Xie dan Leijen
• Model memorinya didasarkan pada Perceus: Garbage Free Reference Counting with Reuse, Reference Counting with Frame-Limited Reuse, dan FP^2: Fully in-Place Functional Programming
• Effect row-nya berasal dari keluarga row polymorphism dan scoped labels, sementara handler-nya mengadopsi Handlers of Algebraic Effects karya Plotkin dan Pretnar melalui Eff dan Koka
• Pattern matching-nya berbasis decision tree dan usefulness matrix, dan bentuk pattern merupakan gabungan dari view pattern dan Pattern Synonyms di GHC
• Lapisan kegagalannya adalah bentuk pemulihan dari The Verse Calculus melalui handler final ctl
• Arah Prism lebih dekat ke menjadikan efek terlihat, bertipe, dan dapat dilacak secara komposisional daripada ke “fungsional murni”
• Proyek ini sendiri lebih dekat ke mainan dan karya artistik daripada alat praktis, dan diringkas sebagai compiler yang dibuat demi keindahan intelektual dari ide-ide pemrograman fungsional

[GN⁺]

Komentar di Lobste.rs

• Saya tidak mengerti apa hubungan lens dengan effect. Setiap kali tulisan itu menyebut lens, selain dikelompokkan di bawah “satu trik dalam lima cara”, keduanya tampak tidak berkaitan
  Dan saya juga tidak mengerti apa sebenarnya yang ingin dilakukan tick_use(). Apakah penulis mengharapkan pembaca memahami contoh serumit ini tanpa penjelasan? Sepertinya akan membantu kalau ada anotasi tipe

  • Tentang lens dijelaskan lebih lanjut di sini: https://sdiehl.github.io/prism/spec.html#86-optic-paths
    Meski begitu, selain pada level metafora, saya masih tidak melihat jelas apa hubungan lens dengan effect. Penulis menulis begini:

    This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
    Jadi menurut saya metaforanya seperti ini: monad adalah nilai, tetapi effect bukan nilai, melainkan semacam struktur kontrol. Demikian pula lens adalah nilai, tetapi optic paths di Prism bukan nilai; lebih mirip struktur kontrol dengan sintaks yang di-hardcode

• Saya perlu meluangkan lebih banyak waktu untuk memahaminya, tetapi ini benar-benar terlihat indah

• Benar-benar mengesankan. Justru karena itu saya penasaran mengapa Diehl menyebut compiler-nya sebagai mainan di akhir tulisan. Ini tampak seperti proof of concept yang sukses dan menunjukkan tingkat keanggunan baru

• Saya ingin melihat lebih detail seperti apa sebenarnya representasi antara call-by-push-value itu. Khususnya, saya penasaran apakah ia menangani join point
  Sudah ada paper yang membahas teori menambahkan effect ke CBPV. Mengatakan bahwa komputasi memiliki tipe effect sementara nilai tidak, itu cukup alami; tetapi saya belum melihat sesuatu yang diwujudkan cukup konkret untuk langsung diterapkan pada evidence passing ala Koka, jadi ini menarik
  Secara keseluruhan saya ingin tahu posisinya dibandingkan Koka. Dari FBIP, Perceus, dan evidence passing, jelas ini sangat terinspirasi oleh pekerjaan Koka, tetapi pada saat yang sama jelas juga berbeda karena menggunakan CBPV untuk representasi antara. Hanya saja seberapa bedanya belum terlalu terlihat

• Ini terlihat sangat mirip dengan sesuatu yang sudah lama ingin saya luangkan waktu untuk buat. Bagus!

• Sedikit di luar topik, tetapi saya selalu agak menyayangkan proyek Stephen, “write you a haskell”, berhenti beberapa tahun lalu. Untuk Prism, saya berharap ada penjelasan implementasi setingkat tutorial

• Saya penasaran apa yang “impure” dalam bahasa ini. Kata itu hanya muncul di judul dan tidak muncul lagi di isi
  Karena semua effect tampaknya dilacak, fungsi tanpa effect tetap merupakan fungsi matematis. Apakah saya melewatkan sesuatu?

  • Sepertinya berkaitan dengan penggunaan variabel lokal yang mutable di dalam definisi fungsi, seperti pada definisi fib yang diberikan. var x adalah variabel mutable yang impure, sedangkan let x adalah variabel immutable yang pure

• Yang benar-benar keren adalah hal-hal yang biasanya diperlakukan sebagai fitur bahasa, misalnya yield di bahasa X atau throw di bahasa Y, diimplementasikan sebagai satu interface lagi
  Bahwa berbagai alur kontrol seperti side effect, exception, dan continuation bisa dibangun di atas satu abstraksi adalah cara yang menarik untuk melihat ulang seluruh pertanyaan desain, dan saya berharap ini membantu atau mendorong lebih banyak eksplorasi dan inovasi. Sepertinya saya akan kembali melihatnya selama bertahun-tahun ke depan untuk mencari inspirasi