Prism: Tür belirtili etkilere sahip saf olmayan işlevsel dil

• Prism, değiştirilebilir değişkenler, istisnalar ve akışlar gibi etkileri gizlemek yerine türlerde görünür kılan; buna karşılık dışarıdan gözlemlenemeyen yerel değişiklikleri Int -> Int gibi saf türler olarak koruyan deneysel bir derleyicidir
• Temelinde cebirsel etki işleyicileri ve row polymorphism bulunur; etkiler fonksiyon türünün satırında birleşir ve işleyiciler yalnızca gerekli etiketleri ele alıp geri kalanını iletir
• Aynı etki sistemi; istisnaları, generator/stream yapıları, lens’leri, var durumunu ve fail/guard akışını ifade eder; bazı yollar ara liste ya da çalışma zamanı bileşimi olmadan lower edilir
• Performans tarafında, etki çağrısı başına allocation’dan kaçınmak için evidence passing ile Perceus referans sayımını birleştirir ve tekil sahipli değerlere yapılan işlevsel güncellemeleri yerinde değişikliğe optimize eder
• Prism; LLVM IR, MLIR, C runtime, Rust yorumlayıcı, Lean 4 modeli ve WASM playground’u birlikte sunar; böylece tür çıkarımı ve lowering sonuçları doğrudan incelenebilir

---

Dışarıdan görünmeyen değişiklikler ve tür belirtili etkiler

• Prism’in çıkış noktası, içeride var ve atama kullanan bir fib fonksiyonunun dış gözlemci açısından yine de saf bir fonksiyon gibi görünebilmesidir
  • Örnek fib, iki değişkeni yerinde günceller ama durumu fonksiyon dışına sızdırmaz
  • Türü Int -> Int olur ve etki türde görünmez
• Prism, son 3 yılda geliştirilen bir kavram kanıtı işlevsel derleyicidir; OCaml 5, Haskell ve Koka çizgisindeki modern tür fikirlerine dayanarak etkileri modeller
• Ana yönelim, etkilerden kaçınmak değil; onları tür sistemine dahil edip derleyicinin maliyeti ortadan kaldıracak şekilde optimize etmesini sağlamaktır

Etkiler arayüz gibi çalışır

• Prism’de etkiler, işlemleri bildirip işleyicilerin bu işlemlere anlam verdiği cebirsel etki işleyicileri yaklaşımıyla ele alınır
  • effect Gen { ctl yield(Int) : Unit }, yield işlemini bildirir
  • fn produce(n) : !{Gen} Unit içindeki !{Gen}, fonksiyonun yield gerçekleştirdiğini türde gösterir
• Aynı üretici bile continuation olan k’nin nasıl ele alındığına göre farklı anlamlarda yorumlanır
  • total, yield değerlerini toplar
  • count, yield sayısını sayar
  • k atılırsa istisna, bir kez çağrılırsa durum ya da generator, birden çok kez çağrılırsa arama davranışı ortaya çıkar
• Amb etkisi örneği, Pisagor üçlülerini aramayı choose ve reject ile ifade eder
  • choose(n), 0..n-1 aralığındaki değerleri sağlar
  • İşleyici, her aday için aynı continuation’ı yeniden başlatarak bir arama ağacı kurar
• OCaml 5’ten farklı olarak Prism, etkileri türlere dahil eder; Haskell’deki monad transformer stack gibi katmanları elle yükseltmek gerekmez
  • Etki satırları çağrılar boyunca yapısal olarak birleşir
  • Bir stack’ten çok etiket kümesi gibi davranır

Tek bir mekanizmayla ifade edilen özellikler

• İstisnalar

  • Prism’de istisnalar, continuation’ı atan bir işleyicidir
  • final ctl bölümü, k’yi bırakır ve gövde değerini işleyicinin sonucu yapar
  • Result yaymak ya da çağrı yığınına ? serpiştirmek gibi bir yaklaşım değildir
  • İstisnalar etki satırındaki etiketler olduğundan genişletilebilir istisnalar olarak bileşir
  • Her başarısızlık ayrı bir işlemdir ve fonksiyon türündeki satır dışarı kaçabilecek istisnaları gösterir
  • Abort ve Timeout örneğinde fetch, !{Abort, Timeout} taşır
  • with_default, yalnızca Timeout’u ele alıp fallback olarak "cached" döndürür; işlem sonrası türde sadece !{Abort} kalır
  • Java’daki checked exception’lardan farklı olarak sınıf hiyerarşisine bağlı değildir, açık ve yapısal bir küme gibi çalışır

• Generator’lar ve stream’ler

  • Stream’ler, emit gerçekleştiren üreticilerden, bunu yakalayıp yeniden yayan dönüştürücülerden ve fold eden tüketicilerden oluşur
  • Pipeline, tek bir üreticinin etrafında iç içe geçmiş işleyicilerden oluştuğu için ara listeler yapısal olarak ortaya çıkmaz
  • Örnek: srange(1, n).smap(square).skeep(even).stake(5).ssum()
  • stake(5) gibi erken durdurma, gerekli değerler alındıktan sonra continuation’ı atan bir işleyicidir
  • Stream kütüphanesi, Haskell’in pipes ve conduit paketlerinden etkilenmiştir

• Lens’ler

  • Prism’de lens’ler ayrı bir kütüphane değil, record güncelleme yolları ile bellek modelinin birleşimidir
  • İç içe record yapılarda tek bir yol ifadesiyle derin alanlar birden fazla kez güncellenebilir
  • Örnek: { g | player.pos.x = 30, player.hp = 95, score = 110 }
  • İç içe record’un omurgası yeniden kurulur; ancak değer tekil sahiplikteyse parçalanmış hücreler yeniden kullanılır
  • Bu yapı sayesinde işlevsel güncellemeler pointer yazımına derlenebilir
  • Çalışma zamanında optic türleri allocate edilmez veya birleştirilmez
  • deriving (Lens), score_of, with_score gibi sıradan fonksiyon erişimcileri üretir

• Değiştirilebilir durum

  • var, private effect içindeki get/set işlemlerine desugar edilir
  • Blok sonunda kurulan işleyici bu etkiyi işler
  • Closure kaçış analizi, durumun dışarı sızdığı durumları reddeder
  • Saran fonksiyon boş etki satırını koruyabilir

• Başarısızlık

  • Başarısızlık, anonim Fail etkisiyle ifade edilir ve “bu ifade değer üretemeyebilir” durumu tür sistemi tarafından ele alınır
  • fail(), başarısızlığı tetikler; guard(cond) ise koşul yanlışsa başarısız olur
  • ??, sol taraf başarısız olduğunda fallback kullanır
  • ?., option zinciri boyunca ilerlerken kısa devre yapar
  • Comprehension guard, çökmek yerine başarısız öğeleri budar
  • var da bir işleyici sugar’ı olduğundan transact bloğu canlı değişkenlerin snapshot’unu alıp başarısızlıkta rollback yapabilir

Modern tür özellikleri

• Prism, çoğu kodda tür imzası yazma gereğini azaltmak için Dunfield-Krishnaswami tarzı bidirectional higher-rank tür çıkarımı kullanır
• Daha yüksek dereceli çokbiçimliliğin gerektiği sınırlarda bağlayıcılar forall ile açıkça belirtilir
  • pick(g : forall a. (a) -> a), g’yi hem Bool hem de Int üzerinde uygulayabilir
  • Damas-Milner core’da ise ilk çağrıda a, Bool ile birleştirilir ve ikinci çağrı reddedilirdi
• Ad-hoc polymorphism, Lean tarzı type class’larla ifade edilir
  • Instance’lar adlandırılmış değerlerdir
  • given Ord(a), bir dictionary ister
  • Birden fazla instance varsa biri canonical olarak işaretlenir, diğerleri using ile açıkça belirtilir
• deriving, Eq, Ord, Show, Lens gibi tekrar eden instance’ları ve alan erişimcilerini üretir
• Pattern matching de sınıflarla bağlantılıdır
  • pattern First(n) for Peek = view peek, sınıf metodunu view olarak kullanan bir pattern’dir
  • head_or, Peek instance’ı bulunan farklı türlerde aynı pattern’i kullanabilir
• show, ayrı bir sınıf olmadan tür odaklı çalışır
  • Derleyici, statik türden yapısal printer üretir
  • Çıktı biçimini belirlemek için çalışma zamanında tür etiketi okunmaz
• Etki satırları da çokbiçimlidir
  • fn twice(f : (Unit) -> Int ! {| e}), argüman olarak alınan fonksiyonun etki satırı e ne olursa olsun sonucu toplar
  • Saf thunk’ta e, boş satır {} ile birleşir
  • Tick ya da Say gibi etkiler üreten thunk’larda ilgili satır olduğu gibi iletilir

Etki maliyetini azaltan derleme yaklaşımı

• Ders kitabı tarzı cebirsel etki uygulamaları, hesabı free monad biçimindeki bir ağaç olarak yeniden kurar ve her işlemde küçük hücreler allocate edebilir
• Prism’in hızlı yolu, Koka çizgisindeki evidence passing yaklaşımıdır
  • Hesabı yeniden kurup işleyici aramak yerine, etkin işleyici bölümleri her işlem noktasına sıradan parametreler gibi geçirilir
  • do op, doğrudan çağrıya lower edilir
  • İşleyici kurulurken yalnızca bir closure allocate edildiğinden maliyet O(handlers) olur ve işlem sayısıyla orantılı büyümez
• Free monad kodlaması fallback olarak kalır
  • Veri yapısı olarak dışarı çıkan hesaplamalar
  • Gerçek multishot resumption
  • Masked handler gibi kalıplar bunun hedefidir
• Stream pipeline’ları için interprocedural flow analysis, gerekli etki evidence’ını fonksiyon sınırlarının ötesine kadar hesaplar
  • Üretici ve dönüştürücüler boyunca evidence thread edilir
  • Tüm zincir tek bir döngüye lower edilir
  • Ara listeler ya da işlem başına hücre allocation’ı yoktur
• Bu yapı, Haskell’deki stream fusion veya Rust iterator adapter’larının tekilleştirilmesine benzer sonuçları bir etki derleyicisinde elde eder

Bellek modeli ve runtime

• Prism, Perceus referans sayımı kullanır
  • Heap hücreleri, statik olarak bilinen noktalarda belirli biçimde serbest bırakılır
  • Pause ya da tracing yoktur
• Frame-limited reuse, pattern match ile az önce parçalanan hücreyi constructor tarafına yeniden verir
  • Tekil sahipli bir liste üzerindeki map, yeni bir liste döndüren saf bir fonksiyon gibi görünse de gerçekte yerinde değiştirilebilir
  • Lens güncellemelerinin pointer yazımına derlenmesi de aynı mekanizmaya dayanır
• Runtime yapısı Lean 4’ün bellek disiplinine benzer, ancak Prism LLVM IR üretir
  • LLVM IR, inkwell üzerinden oluşturulur
  • Aynı program için metin tabanlı MLIR modülü de üretilir
  • Sonuç, clang ile elle yazılmış C runtime’ı prism_rt.c ile link edilir
• prism_rt.c, yaklaşık 2 bin satırlık küçük bir runtime’dır
  • Heap hücreleri { refcount, tag, arity, fields... } biçiminde 4 veya daha fazla word’lük yapılardır
  • Allocator, rc_inc/rc_dec, yerinde yeniden kullanım allocator’ı, bignum ve string primitive’leri içerir
  • Collector thread, card table ya da safepoint yoktur
• Varsayılan allocator libc malloc’tır; benchmark için opt-in mimalloc ayarı bulunur
• Live-cell oracle, program sonlandığında heap balance’ın 0 olduğunu assert ederek test kümesinin garbage-free özelliğini doğrular

Lean modeli ve backend doğrulaması

• Prism yorumlayıcısı CEK machine ailesindendir ve bu makine Lean 4 modeli models/Prism.lean içine yansıtılmıştır
• Lean 4 modeli, small-step ilişkisinin deterministik olduğuna dair makine tarafından doğrulanmış bir teorem içerir
  • Program tam olarak tek bir sonraki duruma ilerler
• Rust uygulamasındaki yorumlayıcı, differential oracle olarak da kullanılır
  • Corpus içindeki tüm programlar yorumlayıcıdan ve LLVM, MLIR, C-linked binary backend’lerinden geçer
  • Build’in geçmesi için dört çıktının byte-identical olması gerekir
• Determinizm, replayable durable execution için temel oluşturur
  • Girdi sabitlenip yürütme kaydedildiğinde bit-for-bit yeniden oynatma mümkün olur düşüncesi vardır
  • Gelecek sürümlerde, çökme sonrası replay güvenliğini tür özelliği olarak denetleyen bir Prism hedeflenir

WASM playground ve kaynak kodu

• Aynı yorumlayıcı WASM’a derlenmiştir; playground üzerinden kurulum olmadan Prism kodu çalıştırılabilir
• Playground, programları worker içinde çalıştırır
• Düğmelerle çıkarılan tür imzaları, effect row ve lowered core IR dökümü alınabilir
  • var döngülerinin ya da stream pipeline’larının gerçekte hangi biçime lower edildiği görülebilir
• Metindeki örnekler dropdown içinde yer alır
• Tüm kaynak kodu, Lean modeli ve C runtime’ı GitHub üzerindeki prism deposunda bulunur

Uygulama soyu ve projenin niteliği

• Prism’in core IR’ı, Levy’nin Call-by-Push-Value: A Functional/Imperative Synthesis çalışmasına dayanan call-by-push-value çizgisindedir
• Hızlı etki yolu, Xie ve Leijen’in Generalized Evidence Passing for Effect Handlers ve Effect Handlers, Evidently çalışmalarına yakındır
• Bellek modeli, Perceus: Garbage Free Reference Counting with Reuse, Reference Counting with Frame-Limited Reuse, FP^2: Fully in-Place Functional Programming çalışmalarına dayanır
• Etki satırları, row polymorphism ve scoped labels geleneğine uzanır; işleyiciler ise Plotkin ve Pretnar’ın Handlers of Algebraic Effects yaklaşımının Eff ve Koka üzerinden benimsenmiş halidir
• Pattern matching, decision tree ve usefulness matrix tabanlıdır; pattern biçimi, view pattern ile GHC’nin Pattern Synonyms yaklaşımının birleşimidir
• Başarısızlık katmanı, The Verse Calculus yaklaşımının final ctl işleyicisiyle geri kazanılmış biçimidir
• Prism’in yönü, “saf işlevsel” olmaktan çok etkileri görünür kılmak, türlendirmek ve bileşebilir şekilde izlemek fikrine yakındır
• Projenin kendisi pratik bir araçtan çok oyuncak ve sanatsal bir çalışma niteliğindedir; işlevsel programlama fikirlerinin entelektüel güzelliği için yapılmış bir derleyici olarak konumlanır

[GN⁺]

Lobste.rs yorumları

• Lenslerin efektlerle ne ilgisi olduğunu bilmiyorum. Yazıda lenslerden her söz edildiğinde, “tek numarayı beş farklı şekilde” başlığı altında toplanmış olmaları dışında birbirleriyle alakasız görünüyorlar.
  Ayrıca tick_use() tam olarak ne yapmaya çalışıyor, onu da anlamadım. Okurun, açıklama olmadan böyle dolambaçlı bir örneği anlaması mı bekleniyor? Tip anotasyonları olsaydı yardımcı olurdu.

  • Lensler burada daha ayrıntılı açıklanmış: https://sdiehl.github.io/prism/spec.html#86-optic-paths
    Yine de metaforik düzey dışında lenslerin efektlerle ne ilgisi olduğunu pek göremiyorum. Yazar şöyle yazıyor:

    This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
    Yani metaforun şöyle olduğunu düşünüyorum: monadlar değerdir, ama efektler değer değil, bir tür kontrol yapısıdır. Benzer şekilde lensler değerdir, fakat Prism’in optic paths kavramı değer değil; sabitlenmiş sözdizimine sahip bir kontrol yapısına daha yakındır.

• Anlamak için daha fazla zaman ayırmam gerekecek ama gerçekten güzel görünüyor.

• Gerçekten etkileyici. Hatta bu yüzden Diehl’in yazının sonunda derleyiciyi neden oyuncak diye nitelediğini merak ediyorum. Yeni bir zarafet düzeyini gösteren başarılı bir kavram kanıtı gibi görünüyor.

• call-by-push-value ara gösteriminin pratikte nasıl göründüğünü daha ayrıntılı görmek isterdim. Özellikle join point’leri nasıl ele aldığını merak ediyorum.
  CBPV’ye efekt ekleme teorisini ele alan makaleler vardı. Hesaplamaların efekt tipleri olduğu, değerlerin ise olmadığı söylemi oldukça doğal; ancak bunun Koka’nın kanıt aktarımına doğrudan uygulanacak kadar somutlaştırılmış hâlini görmemiştim, bu yüzden ilginç.
  Genel olarak Koka ile kıyaslandığında nerede konumlandığını bilmek isterdim. FBIP, Perceus ve kanıt aktarımına bakınca Koka çalışmalarından güçlü biçimde esinlendiği açık; aynı zamanda ara gösterimde CBPV kullandığı için belirgin biçimde farklı da. Ancak ne kadar farklı olduğu pek görünmüyor.

• Sürekli zaman ayırıp yapmaya çalıştığım şeye epey benziyor. Güzel!

• Konudan biraz sapacağım ama Stephen’ın “write you a haskell” projesinin birkaç yıl önce durmuş olmasına hep biraz üzülmüştüm. Prism için eğitici düzeyde bir uygulama açıklaması çıksa iyi olurdu.

• Bu dilde neyin “impure” olduğunu merak ediyorum. Bu kelime yalnızca başlıkta geçiyor, metinde tekrar yer almıyor.
  Tüm efektler izleniyor gibi görünüyor; dolayısıyla efektsiz bir fonksiyon hâlâ matematiksel bir fonksiyon. Bir şeyi mi kaçırıyorum?

  • Verilen fib tanımında olduğu gibi, fonksiyon tanımı içinde yerel değiştirilebilir değişkenler kullanmakla ilgili görünüyor. var x impure, değiştirilebilir bir değişken; let x ise saf, değiştirilemez bir değişken.

• Normalde dilin özellikleri olarak ele alınan şeyleri — örneğin X dilindeki yield, Y dilindeki throw gibi — bir başka arayüz olarak uygulamış olması gerçekten harika.
  Yan etkiler, istisnalar ve continuation’lar gibi çeşitli kontrol akışlarını tek bir soyutlama üzerinde kurabilmek, tasarım sorularının tamamına yeni bir gözle bakmanın ilginç bir yolu; bunun daha fazla keşif ve yeniliğe yardımcı olmasını ya da ilham vermesini umuyorum. Önümüzdeki yıllarda ilham almak için tekrar tekrar döneceğim gibi görünüyor.