Prism: टाइप्ड effects वाली एक non-pure functional भाषा

 (stephendiehl.com)
1 पॉइंट द्वारा GN⁺ 2 시간 전 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Prism एक experimental compiler है जो mutable variables, exceptions, और streams जैसे effects को छिपाने के बजाय type में दिखाता है, जबकि बाहर से observe न होने वाले local mutations को Int -> Int जैसे pure type के रूप में बनाए रखता है
  • इसका core algebraic effect handlers और row polymorphism है, जहाँ effects function type की row में जुड़ते हैं और handlers सिर्फ ज़रूरी labels को handle करके बाकी आगे pass करते हैं
  • यही effect system exceptions, generators/streams, lenses, var state, और fail/guard flow को express करता है, और कुछ paths में बिना intermediate lists या runtime composition के lower हो जाता है
  • performance के लिए यह evidence passing और Perceus reference counting को जोड़ता है ताकि हर effect call पर allocation से बचा जा सके, और uniquely owned values की functional updates को in-place mutation में optimize किया जा सके
  • Prism LLVM IR, MLIR, C runtime, Rust interpreter, Lean 4 model, और WASM playground भी देता है, जिससे type inference और lowering results को सीधे देखा जा सकता है

बाहर से अदृश्य mutation और typed effects

  • Prism की शुरुआत इस विचार से होती है कि अंदर var और assignment इस्तेमाल करने वाला fib function भी बाहरी observer को pure function जैसा दिख सकता है
    • उदाहरण fib दो variables को in-place update करता है, लेकिन function के बाहर state expose नहीं करता
    • इसका type Int -> Int है, और effect type में नहीं दिखता
  • Prism पिछले 3 साल में विकसित किया गया एक proof-of-concept functional compiler है, जो OCaml 5, Haskell, और Koka परिवार के modern type ideas पर आधारित होकर effects को model करता है
  • मुख्य दिशा effects से बचना नहीं, बल्कि उन्हें type system में लाना और compiler से उनकी cost optimize कराना है

effects interface की तरह काम करते हैं

  • Prism में effects, operations declare करते हैं और handlers उन operations को meaning देते हैं — यह algebraic effect handlers का तरीका है
    • effect Gen { ctl yield(Int) : Unit } yield operation declare करता है
    • fn produce(n) : !{Gen} Unit में !{Gen} type में यह दिखाता है कि function yield करता है
  • वही producer continuation k को कैसे handle करता है, इसके आधार पर अलग-अलग अर्थ ले सकता है
    • total yield values को जोड़ता है
    • count yield की संख्या गिनता है
    • k को फेंक देने पर exception, एक बार call करने पर state या generator, और कई बार call करने पर search behavior बनता है
  • Amb effect का उदाहरण choose और reject से Pythagorean triples की खोज को express करता है
    • choose(n) 0..n-1 range के values देता है
    • handler हर candidate के लिए उसी continuation को resume करके search tree बनाता है
  • OCaml 5 के विपरीत Prism effects को type में शामिल करता है, और Haskell के monad transformer stack की तरह layers को manually उठाने की ज़रूरत नहीं होती
    • effect rows calls के दौरान structurally merge होती हैं
    • यह stack नहीं बल्कि labels के set की तरह काम करती हैं

एक ही mechanism से व्यक्त होने वाली सुविधाएँ

  • exceptions

    • Prism में exception एक continuation को discard करने वाला handler है
    • final ctl clause k को छोड़ देता है और उस body value को handler result बना देता है
    • यह Result propagate करने या call stack में ? बिखेरने वाला तरीका नहीं है
    • exception effect row का label है, इसलिए यह extensible exceptions की तरह compose होता है
    • हर failure एक अलग operation है, और function type की row यह दिखाती है कि कौन-से exceptions बाहर निकल सकते हैं
    • Abort और Timeout के उदाहरण में fetch का type !{Abort, Timeout} है
    • with_default सिर्फ Timeout को handle करके fallback "cached" लौटाता है, और handle होने के बाद type में सिर्फ !{Abort} बचता है
    • Java के checked exceptions की तरह class hierarchy से बंधा नहीं, बल्कि open structural set की तरह काम करता है

  • generators और streams

    • stream एक ऐसा producer है जो emit करता है, एक transformer जो उसे पकड़कर फिर emit करता है, और एक consumer जो fold करता है
    • pipeline एक single producer के आसपास nested handlers के रूप में बनती है, इसलिए intermediate lists संरचनात्मक रूप से बनती ही नहीं
    • उदाहरण: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • stake(5) जैसा early stop, ज़रूरी values मिलने के बाद continuation को discard करने वाला handler है
    • stream library पर Haskell के pipes और conduit का प्रभाव है

  • lenses

    • Prism में lenses कोई अलग library नहीं, बल्कि record update paths और memory model का संयोजन हैं
    • nested records में एक ही path expression से कई deep fields update किए जा सकते हैं
    • उदाहरण: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • nested record की spine फिर से बनाई जाती है, लेकिन अगर value uniquely owned हो तो टूटे हुए cells को reuse किया जाता है
    • इसी संरचना की वजह से functional update को pointer writes में compile किया जा सकता है
    • runtime पर optic types allocate या compose नहीं किए जाते
    • deriving (Lens) score_of, with_score जैसे सामान्य function accessors बना देता है

  • mutable state

    • var को private effect के get/set operations में desugar किया जाता है
    • block के अंत में install किया गया handler इस effect को process करता है
    • closure escape analysis उस स्थिति को reject करता है जहाँ state बाहर निकल सकती हो
    • enclosing function empty effect row बनाए रख सकता है

  • failure

    • failure को anonymous Fail effect के रूप में व्यक्त किया जाता है, और type system यह संभालता है कि “यह expression value produce न भी कर सके”
    • fail() failure करता है, और guard(cond) condition false होने पर failure करता है
    • ?? बाएँ पक्ष के fail होने पर fallback इस्तेमाल करता है
    • ?. option chain को follow करते हुए short-circuit करता है
    • comprehension guard crash की जगह failed elements को prune करता है
    • क्योंकि var भी handler sugar है, transact block live variables का snapshot लेकर failure पर rollback कर सकता है

modern type features

  • Prism अधिकतर code में type signatures लिखे बिना काम करने के लिए Dunfield-Krishnaswami शैली की bidirectional higher-rank type inference का उपयोग करता है
  • जहाँ higher-order polymorphism ज़रूरी हो, वहाँ forall से binders को explicitly लिखा जाता है
    • pick(g : forall a. (a) -> a) में g को Bool और Int दोनों पर apply किया जा सकता है
    • Damas-Milner core में पहली call पर a का Bool से unify हो जाना दूसरी call को reject कर देता
  • ad-hoc polymorphism को Lean-style type classes से व्यक्त किया गया है
    • instances named values हैं
    • given Ord(a) dictionary की माँग करता है
    • कई instances होने पर एक को canonical चिह्नित किया जाता है और बाकी को using से explicitly चुना जाता है
  • deriving Eq, Ord, Show, Lens जैसी repetitive instances और field accessors generate करता है
  • pattern matching भी classes से जुड़ा हुआ है
    • pattern First(n) for Peek = view peek एक ऐसा pattern है जो class method को view की तरह इस्तेमाल करता है
    • head_or एक ही pattern को कई ऐसे types पर इस्तेमाल कर सकता है जिनके पास Peek instance हो
  • show अलग class के बिना type-directed तरीके से काम करता है
    • compiler static type से structural printer synthesize करता है
    • output format तय करने के लिए runtime type tags नहीं पढ़े जाते
  • effect rows भी polymorphic हैं
    • fn twice(f : (Unit) -> Int ! {| e}) argument function की effect row e चाहे जो हो, result को जोड़ता है
    • pure thunk में e empty row {} से unify हो जाता है
    • Tick या Say जैसे effects करने वाले thunk में वही row आगे pass होती है

effect cost घटाने वाली compilation technique

  • textbook algebraic effect implementations computation को free monad जैसी tree संरचना में बदल सकती हैं और हर operation पर छोटे cells allocate कर सकती हैं
  • Prism का fast path Koka-शैली का evidence passing है
    • computation को reconstruct करके handler खोजने के बजाय active handler clauses को हर operation site तक सामान्य parameters की तरह pass किया जाता है
    • do op सीधे function call में lower हो जाता है
    • handler install करते समय सिर्फ एक closure allocate होती है, इसलिए cost O(handlers) रहती है, operations की संख्या के अनुपात में नहीं
  • free monad encoding fallback के रूप में बनी रहती है
    • data structure में escape होने वाली computations
    • असली multishot resumption
    • masked handler जैसे patterns इसके target हैं
  • stream pipelines में interprocedural flow analysis ज़रूरी effect evidence को function boundaries के पार तक compute करता है
    • producer और transformer के बीच evidence thread किया जाता है
    • पूरी chain single loop में lower हो जाती है
    • न intermediate lists बनती हैं, न per-operation cell allocation
  • यह संरचना Haskell की stream fusion या Rust iterator adapters के monomorphization जैसे परिणाम effect compiler में हासिल करती है

memory model और runtime

  • Prism Perceus reference counting का उपयोग करता है
    • heap cells statically known points पर deterministically free होते हैं
    • कोई pause या tracing नहीं है
  • frame-limited reuse pattern match से अभी-अभी टूटे हुए cell को constructor side में वापस दे देता है
    • uniquely owned list पर map pure function की तरह नई list लौटाता हुआ दिखता है, लेकिन वास्तव में in-place mutate हो सकता है
    • lens updates का pointer writes में compile होना भी इसी mechanism का हिस्सा है
  • runtime structure Lean 4 की memory discipline जैसी है, लेकिन Prism LLVM IR emit करता है
    • LLVM IR inkwell के जरिए generate होता है
    • उसी program के लिए text MLIR module भी generate होता है
    • result को clang से hand-written C runtime prism_rt.c के साथ link किया जाता है
  • prism_rt.c लगभग 2000 lines का छोटा runtime है
    • heap cells का रूप { refcount, tag, arity, fields... } वाले 4 या अधिक word structure जैसा है
    • इसमें allocator, rc_inc/rc_dec, in-place reuse allocator, bignum और string primitives शामिल हैं
    • कोई collector thread, card table, या safepoint नहीं है
  • default allocator libc malloc है, और benchmarking के लिए opt-in mimalloc config उपलब्ध है
  • live-cell oracle program समाप्ति पर heap balance 0 होने की assert करता है, जिससे test suite garbage-free गुण की जाँच करता है

Lean model और backend verification

  • Prism interpreter CEK machine परिवार का है, और यह machine Lean 4 model models/Prism.lean में reflect की गई है
  • Lean 4 model में small-step relation deterministic होने का machine-checked theorem है
    • program ठीक एक ही next state में आगे बढ़ता है
  • Rust implementation का interpreter differential oracle के रूप में भी इस्तेमाल होता है
    • corpus के सभी programs interpreter, LLVM, MLIR, और C-linked binary backends से गुजरते हैं
    • build pass होने के लिए चारों outputs byte-identical होने चाहिए
  • determinism replayable durable execution की नींव बनता है
    • विचार यह है कि input fix करके execution record किया जाए तो bit-for-bit replay संभव हो
    • future versions में crash के बाद replay safety को type property की तरह check करने वाला Prism कल्पित है

WASM playground और source

  • यही interpreter WASM में compile किया गया है, इसलिए playground में बिना installation के Prism code चलाया जा सकता है
  • playground programs को worker में चलाता है
  • buttons के जरिए inferred type signatures, effect rows, और lowered core IR dump किए जा सकते हैं
    • इससे देखा जा सकता है कि var loops या stream pipelines वास्तव में किस रूप में lower होते हैं
  • लेख के examples dropdown में शामिल हैं
  • पूरा source, Lean model, और C runtime prism repository on GitHub में उपलब्ध हैं

implementation lineage और project का स्वभाव

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2 시간 전
Lobste.rs पर टिप्पणियाँ

  • समझ नहीं आता कि lenses का effects से क्या संबंध है। लेख में जब भी lenses का ज़िक्र आता है, “एक trick को पाँच तरीकों से” के तहत रखे जाने के अलावा वे आपस में असंबंधित लगते हैं
    और tick_use() आखिर करना क्या चाहता है, यह भी समझ नहीं आता। क्या लेखक उम्मीद कर रहे हैं कि पाठक बिना व्याख्या के ऐसा उलझा हुआ example समझ लेंगे? type annotations होते तो मदद मिलती

    • lenses के बारे में यहाँ और बताया गया है: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      फिर भी रूपक के स्तर से आगे lenses का effects से क्या संबंध है, साफ़ नहीं दिखता। लेखक ने लिखा है:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      यानी रूपक शायद यह है: monads values होते हैं, लेकिन effects values नहीं, बल्कि एक तरह की control structure हैं। इसी तरह lenses values होते हैं, लेकिन Prism के optic paths values नहीं हैं; वे hardcoded syntax वाली control structure के ज़्यादा करीब हैं

  • इसे समझने में और समय लगाना पड़ेगा, लेकिन यह सच में सुंदर दिखता है

  • वाकई प्रभावशाली है। बल्कि इसी वजह से सोचता हूँ कि Diehl लेख के अंत में compiler को toy क्यों कहते हैं। यह elegance के नए स्तर को दिखाने वाला सफल proof of concept लगता है

  • मैं और विस्तार से देखना चाहूँगा कि call-by-push-value intermediate representation असल में कैसी दिखती है। खासकर यह कि join points को कैसे handle किया जाता है
    CBPV में effects जोड़ने की theory पर papers रहे हैं। यह कहना काफी natural है कि computations के पास effect types होते हैं और values के पास नहीं, लेकिन Koka की evidence passing पर सीधे लागू करने लायक इतना concrete रूप मैंने नहीं देखा, इसलिए यह दिलचस्प है
    कुल मिलाकर, Koka की तुलना में इसकी स्थिति क्या है, यह जानना चाहूँगा। FBIP, Perceus, और evidence passing को देखकर साफ़ है कि यह Koka के काम से काफी प्रेरित है, और साथ ही intermediate representation में CBPV का इस्तेमाल करने से यह निश्चित रूप से अलग भी है। बस कितना अलग है, यह साफ़ नहीं दिखता

  • यह काफी हद तक उस चीज़ जैसा दिखता है जिसे बनाने के लिए मैं लगातार समय निकालने की सोच रहा था। अच्छा है!

  • विषय से थोड़ा हटकर, Stephen का “write you a haskell” project कुछ साल पहले रुक गया था, इसका मुझे हमेशा थोड़ा अफसोस रहा। Prism के लिए tutorial-level implementation explanation आए तो अच्छा होगा

  • इस language में “impure” क्या है, यह जानना चाहता हूँ। यह शब्द सिर्फ title में आता है और body में फिर नहीं दिखता
    लगता है सभी effects track किए जाते हैं, इसलिए effect-free functions अभी भी mathematical functions हैं। क्या मैं कुछ miss कर रहा हूँ?

    • लगता है यह function definitions के अंदर local mutable variables इस्तेमाल करने से जुड़ा है, जैसे दिए गए fib definition में। var x impure mutable variable है, और let x pure immutable variable है

  • आम तौर पर languages की features मानी जाने वाली चीज़ें—जैसे X language का yield, Y language का throw—इन्हें एक और interface के रूप में implement किया गया है, यह सच में शानदार है
    side effects, exceptions, continuations जैसे कई control flows को एक abstraction के ऊपर बना पाना design questions को पूरी तरह नए तरीके से देखने का दिलचस्प तरीका है, और उम्मीद है कि यह और exploration और innovation में मदद करेगा या उन्हें प्रेरित करेगा। लगता है आने वाले कई सालों तक inspiration लेने के लिए मैं इसे फिर-फिर देखता रहूँगा