Prism: ภาษาฟังก์ชันไม่บริสุทธิ์ที่มีเอฟเฟกต์ระบุในไทป์

 (stephendiehl.com)
1 คะแนน โดย GN⁺ 2 시간 전 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Prism เป็นคอมไพเลอร์เชิงทดลองที่ไม่ซ่อนเอฟเฟกต์อย่างตัวแปรเปลี่ยนค่าได้, exception และสตรีม แต่แสดงไว้ในไทป์ ขณะเดียวกันการเปลี่ยนแปลงเฉพาะที่ซึ่งสังเกตจากภายนอกไม่ได้ยังคงเป็นไทป์บริสุทธิ์อย่าง Int -> Int
  • แกนหลักคือ algebraic effect handlers และ row polymorphism โดยเอฟเฟกต์จะถูกรวมเข้าในแถวของไทป์ฟังก์ชัน และ handler จะจัดการเฉพาะ label ที่ต้องการก่อนส่งส่วนที่เหลือต่อไป
  • ระบบเอฟเฟกต์เดียวกันนี้ใช้แทน exception, generator/stream, lens, สถานะ var, และ flow แบบ fail/guard ได้ โดยบางเส้นทางจะถูก lower ลงโดยไม่ต้องมีลิสต์กลางหรือการประกอบกันตอน runtime
  • ด้านประสิทธิภาพ ใช้ evidence passing ร่วมกับ reference counting แบบ Perceus เพื่อหลีกเลี่ยงการจัดสรรต่อการเรียกเอฟเฟกต์แต่ละครั้ง และ optimize การอัปเดตเชิงฟังก์ชันของค่าที่มีเจ้าของแบบ unique ให้เป็นการแก้ไขในที่เดิม
  • Prism มีทั้ง LLVM IR, MLIR, C runtime, interpreter ภาษา Rust, โมเดล Lean 4 และ playground บน WASM ให้ตรวจสอบ type inference และผลลัพธ์การ lowering ได้โดยตรง

การเปลี่ยนแปลงที่มองไม่เห็นจากภายนอกและเอฟเฟกต์ที่ระบุในไทป์

  • จุดเริ่มต้นของ Prism คือข้อสังเกตว่าแม้ฟังก์ชัน fib ที่ใช้ var และการกำหนดค่าอยู่ภายใน ก็ยังอาจดูเหมือนฟังก์ชันบริสุทธิ์สำหรับผู้สังเกตภายนอกได้
    • ตัวอย่าง fib อัปเดตตัวแปรสองตัวในที่เดิม แต่ไม่เปิดเผยสถานะออกนอกฟังก์ชัน
    • ไทป์คือ Int -> Int และเอฟเฟกต์ไม่ปรากฏในไทป์
  • Prism เป็น คอมไพเลอร์ฟังก์ชันแบบ proof-of-concept ที่พัฒนามา 3 ปี โดย model เอฟเฟกต์บนฐานไอเดียไทป์สมัยใหม่ในสาย OCaml 5, Haskell และ Koka
  • แนวทางหลักไม่ใช่การหลีกเลี่ยงเอฟเฟกต์ แต่คือการใส่เอฟเฟกต์ไว้ในระบบไทป์ แล้วให้คอมไพเลอร์ optimize เพื่อลบต้นทุนออก

เอฟเฟกต์ทำงานเหมือนอินเทอร์เฟซ

  • เอฟเฟกต์ของ Prism ใช้แนวทาง algebraic effect handlers คือประกาศ operation แล้วให้ handler กำหนดความหมายของ operation นั้น
    • effect Gen { ctl yield(Int) : Unit } ประกาศ operation ชื่อ yield
    • !{Gen} ใน fn produce(n) : !{Gen} Unit แสดงในไทป์ว่าฟังก์ชันทำ yield
  • แม้เป็น producer เดียวกัน ก็ถูกตีความต่างกันได้ตามวิธีจัดการ continuation k
    • total บวกค่า yield
    • count นับจำนวนครั้งของ yield
    • ถ้าทิ้ง k จะกลายเป็น exception, ถ้าเรียกครั้งเดียวจะเป็นสถานะหรือ generator, ถ้าเรียกหลายครั้งจะเป็นพฤติกรรมการค้นหา
  • ตัวอย่างเอฟเฟกต์ Amb ใช้ choose และ reject เพื่อแทนการค้นหา Pythagorean triples
    • choose(n) ให้ค่าช่วง 0..n-1
    • handler จะ resume continuation เดียวกันสำหรับแต่ละ candidate เพื่อสร้าง search tree
  • ต่างจาก OCaml 5, Prism ใส่เอฟเฟกต์ไว้ในไทป์ และไม่ต้องยกเลเยอร์ด้วยมือเหมือน stack ของ monad transformer ใน Haskell
    • effect row จะถูกรวมกันเชิงโครงสร้างผ่านการเรียกต่าง ๆ
    • ทำงานเหมือนชุดของ label มากกว่า stack

ฟีเจอร์ที่แทนได้ด้วยกลไกเดียวกัน

  • Exception

    • ใน Prism exception คือ handler ที่ทิ้ง continuation
    • clause final ctl จะทิ้ง k และใช้ค่าของ body นั้นเป็นผลลัพธ์ของ handler
    • ไม่ใช่วิธี propagate Result หรือโปรย ? ไปตาม call stack
    • เพราะ exception เป็น label ใน effect row จึง compose ได้แบบ exception ที่ขยายได้
    • ความล้มเหลวแต่ละแบบเป็น operation แยกกัน และแถวในไทป์ฟังก์ชันจะแสดง exception ที่อาจหลุดออกไปภายนอก
    • ในตัวอย่าง Abort และ Timeout, fetch มีไทป์ !{Abort, Timeout}
    • with_default จัดการเฉพาะ Timeout แล้วคืน fallback "cached" และหลังจัดการแล้วในไทป์จะเหลือเพียง !{Abort}
    • ต่างจาก checked exception ของ Java ตรงที่ไม่ผูกกับลำดับชั้นของ class แต่ทำงานเป็นชุดโครงสร้างแบบเปิด

  • Generator และ stream

    • Stream ประกอบด้วย producer ที่ทำ emit, transformer ที่จับแล้วปล่อยออกไปอีกครั้ง และ consumer ที่ fold
    • Pipeline อยู่ในรูป handler ซ้อนกันรอบ producer หนึ่งตัว จึง ไม่มีลิสต์กลาง เกิดขึ้นในเชิงโครงสร้าง
    • ตัวอย่าง: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • การหยุดก่อนเวลาอย่าง stake(5) คือ handler ที่ทิ้ง continuation หลังได้ค่าที่ต้องการแล้ว
    • ไลบรารี stream ได้แรงบันดาลใจจาก pipes และ conduit ของ Haskell

  • Lens

    • Lens ของ Prism ไม่ใช่ไลบรารีแยก แต่เป็นการผสมกันของ เส้นทางการอัปเดต record กับโมเดลหน่วยความจำ
    • ใน record ซ้อนกัน สามารถอัปเดต field ลึกหลายตัวด้วย path expression เดียวได้
    • ตัวอย่าง: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • จะสร้าง spine ของ record ซ้อนขึ้นใหม่ แต่ถ้าค่านั้นมีเจ้าของแบบ unique จะนำ cell ที่แยกออกมากลับมาใช้ซ้ำ
    • โครงสร้างนี้ทำให้การอัปเดตเชิงฟังก์ชัน compile เป็นการเขียน pointer ได้
    • ไม่มีการจัดสรรหรือประกอบ optic type ตอน runtime
    • deriving (Lens) สร้าง accessor แบบฟังก์ชันธรรมดา เช่น score_of, with_score

  • สถานะเปลี่ยนค่าได้

    • var ถูก desugar เป็น operation get/set ของ private effect
    • handler ที่ติดตั้งไว้ตอนจบ block จะจัดการเอฟเฟกต์นี้
    • closure escape analysis จะปฏิเสธกรณีที่สถานะหลุดออกไปภายนอก
    • ฟังก์ชันที่ครอบอยู่สามารถคง effect row ว่างไว้ได้

  • Failure

    • Failure แทนด้วยเอฟเฟกต์นิรนาม Fail และระบบไทป์จะจัดการความหมายว่า “expression นี้อาจสร้างค่าไม่ได้”
    • fail() ทำ failure และ guard(cond) จะ failure เมื่อเงื่อนไขเป็นเท็จ
    • ?? ใช้ fallback เมื่อฝั่งซ้าย failure
    • ?. หยุดสั้น ๆ ระหว่างไล่ตาม option chain
    • comprehension guard จะตัดกิ่ง element ที่ failure แทนการ crash
    • เพราะ var ก็เป็น handler sugar เช่นกัน block transact จึง snapshot ตัวแปร live แล้ว rollback ได้เมื่อ failure

ความสามารถของไทป์สมัยใหม่

  • Prism ใช้ bidirectional higher-rank type inference สาย Dunfield-Krishnaswami เพื่อให้โค้ดส่วนใหญ่ไม่ต้องเขียน type signature
  • ที่ขอบเขตซึ่งต้องใช้พหุรูปอันดับสูง จะระบุ binder ด้วย forall
    • pick(g : forall a. (a) -> a) สามารถใช้ g กับทั้ง Bool และ Int
    • ถ้าเป็น core แบบ Damas-Milner, a จะถูก unify เป็น Bool ตั้งแต่การเรียกครั้งแรก และการเรียกครั้งที่สองจะถูกปฏิเสธ
  • ad-hoc polymorphism แทนด้วย type class สไตล์ Lean
    • instance เป็นค่าที่มีชื่อ
    • given Ord(a) ต้องการ dictionary
    • เมื่อมีหลาย instance ให้ทำเครื่องหมายหนึ่งตัวเป็น canonical และระบุตัวอื่นด้วย using
  • deriving สร้าง instance และ field accessor ที่ซ้ำ ๆ เช่น Eq, Ord, Show, Lens
  • Pattern matching ก็เชื่อมกับ class เช่นกัน
    • pattern First(n) for Peek = view peek คือ pattern ที่ใช้ method ของ class เป็น view
    • head_or สามารถใช้ pattern เดียวกันกับหลายไทป์ที่มี instance Peek
  • show ทำงานแบบ type-directed โดยไม่ต้องมี class แยก
    • คอมไพเลอร์ประกอบ structural printer จากไทป์แบบ static
    • ไม่ได้อ่าน runtime type tag เพื่อกำหนดวิธีพิมพ์
  • Effect row ก็เป็น polymorphic ได้
    • fn twice(f : (Unit) -> Int ! {| e}) รวมผลลัพธ์โดยไม่สนว่า effect row e ของฟังก์ชันที่รับเข้ามาคืออะไร
    • สำหรับ pure thunk, e จะ unify กับแถวว่าง {}
    • สำหรับ thunk ที่ทำเอฟเฟกต์อย่าง Tick หรือ Say ก็จะส่งแถวนั้นต่อไปตามเดิม

วิธี compile เพื่อลดต้นทุนของเอฟเฟกต์

  • การ implement algebraic effects แบบตำรามักสร้าง computation ขึ้นใหม่เป็น tree ในรูป free monad และอาจจัดสรร cell เล็ก ๆ ต่อทุก operation
  • fast path ของ Prism คือ evidence passing ในสาย Koka
    • แทนที่จะสร้าง computation ใหม่เพื่อหา handler จะส่ง clause ของ handler ที่ active อยู่ไปยังจุด operation แต่ละแห่งเหมือนพารามิเตอร์ทั่วไป
    • do op ถูก lower เป็นการเรียกตรง
    • เมื่อติดตั้ง handler จะจัดสรร closure เพียงหนึ่งตัว ต้นทุนจึงเป็น O(handlers) และไม่แปรตามจำนวน operation
  • การเข้ารหัสแบบ free monad ยังคงอยู่เป็น fallback
    • computation ที่หลุดออกไปเป็นโครงสร้างข้อมูล
    • resumption แบบ multishot จริง ๆ
    • pattern อย่าง masked handler
  • Stream pipeline ใช้ interprocedural flow analysis เพื่อคำนวณ effect evidence ที่ต้องใช้ข้ามขอบเขตฟังก์ชัน
    • thread evidence ผ่าน producer และ transformer
    • chain ทั้งหมดถูก lower เป็น loop เดียว
    • ไม่มีลิสต์กลางและไม่มีการจัดสรร cell ต่อ operation
  • วิธีนี้เป็นโครงสร้างที่ให้ผลลัพธ์คล้าย stream fusion ของ Haskell หรือการรวม iterator adapter ของ Rust แต่ทำในคอมไพเลอร์เอฟเฟกต์

โมเดลหน่วยความจำและ runtime

  • Prism ใช้ reference counting แบบ Perceus
    • heap cell ถูก free อย่างกำหนดได้ ณ จุดที่รู้แบบ static
    • ไม่มี pause หรือ tracing
  • frame-limited reuse ส่ง cell ที่เพิ่งแยกด้วย pattern match กลับไปยังฝั่ง constructor
    • map บนลิสต์ที่มีเจ้าของแบบ unique ดูเหมือนฟังก์ชันบริสุทธิ์ที่คืนลิสต์ใหม่ แต่จริง ๆ แล้วอาจเปลี่ยนในที่เดิมได้
    • การที่การอัปเดต lens compile เป็นการเขียน pointer ก็ใช้กลไกเดียวกัน
  • โครงสร้าง runtime คล้ายกับวินัยหน่วยความจำของ Lean 4 แต่ Prism ปล่อย LLVM IR
    • LLVM IR สร้างผ่าน inkwell
    • สร้างโมดูล MLIR แบบข้อความสำหรับโปรแกรมเดียวกันด้วย
    • ผลลัพธ์ถูก link ด้วย clang กับ C runtime prism_rt.c ที่เขียนเอง
  • prism_rt.c เป็น runtime ขนาดเล็กราว 2,000 บรรทัด
    • heap cell เป็นโครงสร้างตั้งแต่ 4 word ขึ้นไปในรูป { refcount, tag, arity, fields... }
    • มี allocator, rc_inc/rc_dec, allocator สำหรับ reuse ในที่เดิม, primitive สำหรับ bignum และ string
    • ไม่มี collector thread, card table หรือ safepoint
  • allocator พื้นฐานคือ malloc ของ libc และมีการตั้งค่า mimalloc แบบ opt-in สำหรับ benchmark
  • live-cell oracle จะ assert ตอนจบว่า heap balance เป็น 0 เพื่อให้ test suite ตรวจสอบคุณสมบัติ garbage-free

โมเดล Lean และการตรวจสอบ backend

  • Interpreter ของ Prism อยู่ในตระกูล CEK machine และ machine นี้ถูกสะท้อนไว้ในโมเดล Lean 4 models/Prism.lean
  • โมเดล Lean 4 มี ทฤษฎีบทที่ตรวจสอบด้วยเครื่อง ว่า small-step relation เป็น deterministic
    • โปรแกรมจะดำเนินไปยังสถานะถัดไปได้เพียงหนึ่งสถานะเท่านั้น
  • Interpreter ที่ implement ด้วย Rust ยังถูกใช้เป็น differential oracle ด้วย
    • โปรแกรมทั้งหมดใน corpus ต้องผ่านทั้ง interpreter, LLVM, MLIR และ backend แบบ binary ที่ link กับ C
    • build จะผ่านได้ก็ต่อเมื่อ output ทั้งสี่แบบ byte-identical
  • ความเป็น deterministic เป็นฐานของ replayable durable execution
    • แนวคิดคือถ้าตรึง input และบันทึกการรัน ก็จะ replay ได้แบบ bit-for-bit
    • ในเวอร์ชันอนาคต มีภาพของ Prism ที่ตรวจสอบความปลอดภัยในการ replay หลัง crash เป็นคุณสมบัติระดับไทป์

WASM playground และซอร์ส

  • Interpreter เดียวกันถูก compile เป็น WASM และรันโค้ด Prism ได้โดยไม่ต้องติดตั้งผ่าน playground
  • Playground รันโปรแกรมใน worker
  • มีปุ่มให้ dump type signature ที่ infer ได้, effect row และ lowered core IR
    • สามารถดูได้ว่า loop var หรือ stream pipeline ถูก lower เป็นรูปแบบใดจริง ๆ
  • ตัวอย่างในบทความรวมอยู่ใน dropdown
  • ซอร์สทั้งหมด, โมเดล Lean และ C runtime อยู่ใน prism repository on GitHub

สายการ implement และลักษณะของโปรเจกต์

  • core IR ของ Prism อยู่ในสาย call-by-push-value โดยอิงจาก Call-by-Push-Value: A Functional/Imperative Synthesis ของ Levy
  • fast path ของเอฟเฟกต์ใกล้เคียงกับ Generalized Evidence Passing for Effect Handlers, Effect Handlers, Evidently ของ Xie และ Leijen
  • โมเดลหน่วยความจำอิงจาก Perceus: Garbage Free Reference Counting with Reuse, Reference Counting with Frame-Limited Reuse, FP^2: Fully in-Place Functional Programming
  • Effect row อยู่ในสาย row polymorphism และ scoped labels ส่วน handler เป็นรูปแบบที่รับ Handlers of Algebraic Effects ของ Plotkin และ Pretnar ผ่าน Eff และ Koka
  • Pattern matching อิงจาก decision tree และ usefulness matrix ส่วนรูปแบบ pattern เป็นการผสมกันของ view pattern กับ Pattern Synonyms ของ GHC
  • ชั้น failure เป็นรูปแบบที่นำ The Verse Calculus กลับมาใช้ผ่าน handler final ctl
  • ทิศทางของ Prism ใกล้เคียงกับ การทำให้เอฟเฟกต์มองเห็นได้, ระบุไทป์ได้ และติดตามการประกอบกันได้ มากกว่า “ฟังก์ชันบริสุทธิ์”
  • ตัวโปรเจกต์เองถูกสรุปว่าเป็นของเล่นและงานเชิงศิลป์มากกว่าเครื่องมือใช้งานจริง เป็นคอมไพเลอร์ที่สร้างขึ้นเพื่อความงามทางปัญญาของไอเดีย functional programming

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2 시간 전
ความคิดเห็นบน Lobste.rs

  • ไม่เข้าใจว่าเลนส์เกี่ยวข้องอะไรกับเอฟเฟกต์ ทุกครั้งที่บทความพูดถึงเลนส์ นอกจากถูกจัดไว้ใต้หัวข้อ “ทริกเดียวในห้าวิธี” แล้ว ก็ดูไม่เกี่ยวข้องกันเลย
    แล้วก็ไม่เข้าใจด้วยว่า tick_use() ตั้งใจจะทำอะไรกันแน่ คาดหวังให้ผู้อ่านเข้าใจตัวอย่างที่บิดซับซ้อนแบบนี้โดยไม่มีคำอธิบายหรือ? ถ้ามี คำกำกับชนิดข้อมูล ก็น่าจะช่วยได้

    • มีอธิบายเรื่องเลนส์เพิ่มเติมที่นี่: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      ถึงอย่างนั้นก็ยังมองไม่ค่อยออกว่าเลนส์เกี่ยวข้องอะไรกับเอฟเฟกต์ นอกจากในเชิงอุปมา ผู้เขียนเขียนไว้ว่า:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      กล่าวคือ คิดว่าอุปมาเป็นแบบนี้: โมนาดเป็นค่า แต่เอฟเฟกต์ไม่ใช่ค่า เป็นโครงสร้างควบคุมชนิดหนึ่ง ในทำนองเดียวกัน เลนส์เป็นค่า แต่ optic paths ของ Prism ไม่ใช่ค่า ค่อนข้างใกล้เคียงกับโครงสร้างควบคุมที่มีไวยากรณ์แบบฮาร์ดโค้ด

  • คงต้องใช้เวลาทำความเข้าใจมากกว่านี้ แต่ดู สวยงามจริง ๆ

  • น่าประทับใจมาก ยิ่งทำให้อยากรู้ว่าทำไม Diehl ถึงเรียกคอมไพเลอร์นี้ว่าเป็น ของเล่น ตอนท้ายบทความ ดูเหมือนเป็น proof of concept ที่ประสบความสำเร็จและแสดงให้เห็นความงดงามในระดับใหม่

  • อยากเห็นรายละเอียดเพิ่มเติมว่า intermediate representation แบบ call-by-push-value หน้าตาจริง ๆ เป็นอย่างไร โดยเฉพาะอยากรู้ว่าจัดการจุดรวมทางเดิน (join point) อย่างไร
    เคยมีบทความวิชาการที่พูดถึงทฤษฎีการใส่เอฟเฟกต์ให้ CBPV การบอกว่าการคำนวณมีชนิดเอฟเฟกต์แต่ค่าไม่มีนั้นค่อนข้างเป็นธรรมชาติ แต่ยังไม่เคยเห็นอะไรที่ทำให้เป็นรูปธรรมพอจะนำไปใช้กับการส่งผ่านหลักฐานของ Koka ได้โดยตรง จึงน่าสนใจ
    โดยรวมแล้วอยากรู้ว่าเมื่อเทียบกับ Koka แล้วอยู่ตรงไหน เมื่อดู FBIP, Perceus และการส่งผ่านหลักฐาน ก็ชัดเจนว่าได้รับแรงบันดาลใจอย่างมากจากงานของ Koka และในขณะเดียวกันการใช้ CBPV เป็น intermediate representation ก็ทำให้แตกต่างอย่างแน่นอน เพียงแต่ยังมองไม่ออกว่าต่างกันมากแค่ไหน

  • ดูคล้ายกับสิ่งที่ผมพยายามหาเวลาทำมานานมาก ดีเลย!

  • ออกนอกประเด็นเล็กน้อย แต่ผมรู้สึกเสียดายมาตลอดที่โปรเจกต์ “write you a haskell” ของ Stephen หยุดไปเมื่อหลายปีก่อน สำหรับ Prism ถ้ามี คำอธิบายการทำงานระดับทิวทอเรียล ก็คงดี

  • สงสัยว่าอะไรในภาษานี้ที่ “ไม่บริสุทธิ์” คำนั้นปรากฏแค่ในชื่อเรื่อง แล้วในเนื้อหาก็ไม่กลับมาอีก
    ดูเหมือนว่าเอฟเฟกต์ทั้งหมดถูกติดตามอยู่ ดังนั้นฟังก์ชันที่ไม่มีเอฟเฟกต์ก็ยังเป็นฟังก์ชันทางคณิตศาสตร์อยู่ ผมพลาดอะไรไปหรือเปล่า?

    • น่าจะเกี่ยวกับการใช้ ตัวแปรเปลี่ยนค่าได้แบบโลคัล ภายในนิยามฟังก์ชัน เช่นนิยาม fib ที่ให้มา var x เป็นตัวแปรเปลี่ยนค่าได้ที่ไม่บริสุทธิ์ ส่วน let x เป็นตัวแปรไม่เปลี่ยนค่าแบบบริสุทธิ์

  • เจ๋งมากที่นำสิ่งที่ปกติมักถูกมองเป็น ฟีเจอร์ ของภาษา เช่น yield ในภาษา X หรือ throw ในภาษา Y มาทำเป็นอินเทอร์เฟซอีกแบบหนึ่ง
    การที่สามารถสร้างโฟลว์ควบคุมหลายแบบอย่าง side effects, exceptions, continuations บน abstraction เดียวกันได้ เป็นวิธีมองคำถามด้านการออกแบบใหม่ทั้งชุดที่น่าสนใจ และหวังว่าจะช่วยหรือกระตุ้นให้เกิดการสำรวจและนวัตกรรมมากขึ้น คิดว่าคงจะกลับมาดูเพื่อหาแรงบันดาลใจอีกหลายปีข้างหน้า