Prism: ngôn ngữ hàm không thuần với hiệu ứng được định kiểu

 (stephendiehl.com)
1 điểm bởi GN⁺ 2 giờ trước | 1 bình luận | Chia sẻ qua WhatsApp
  • Prism là một trình biên dịch thử nghiệm thể hiện các hiệu ứng như biến có thể thay đổi, ngoại lệ và stream ngay trong kiểu thay vì che giấu chúng, đồng thời vẫn giữ các thay đổi cục bộ không thể quan sát từ bên ngoài ở kiểu thuần như Int -> Int
  • Cốt lõi của nó là algebraic effect handlers và row polymorphism, nơi các hiệu ứng được gộp vào hàng của kiểu hàm và handler chỉ xử lý các nhãn cần thiết rồi chuyển tiếp phần còn lại
  • Cùng một hệ thống hiệu ứng có thể biểu diễn ngoại lệ, generator/stream, lens, trạng thái var, luồng fail/guard, và một số đường đi được hạ thấp mà không cần danh sách trung gian hay ghép nối lúc chạy
  • Về hiệu năng, nó kết hợp evidence passing với tham chiếu đếm Perceus để tránh cấp phát cho mỗi lần gọi hiệu ứng, đồng thời tối ưu cập nhật hàm trên các giá trị sở hữu duy nhất thành thay đổi tại chỗ
  • Prism cung cấp LLVM IR, MLIR, C runtime, Rust interpreter, mô hình Lean 4 và playground WASM để có thể trực tiếp kiểm tra suy luận kiểu và kết quả lowering

Thay đổi không lộ ra bên ngoài và hiệu ứng được định kiểu

  • Điểm khởi đầu của Prism là ngay cả hàm fib dùng var và phép gán ở bên trong cũng có thể trông như một hàm thuần đối với người quan sát bên ngoài
    • Ví dụ fib cập nhật hai biến tại chỗ nhưng không để lộ trạng thái ra ngoài hàm
    • Kiểu của nó là Int -> Int, và hiệu ứng không xuất hiện trong kiểu
  • Prism là một trình biên dịch hàm proof-of-concept được phát triển trong 3 năm qua, mô hình hóa hiệu ứng dựa trên các ý tưởng kiểu hiện đại từ OCaml 5, Haskell và họ Koka
  • Hướng đi cốt lõi không phải là tránh hiệu ứng, mà là đưa hiệu ứng vào hệ thống kiểu và tối ưu để trình biên dịch loại bỏ chi phí của chúng

Hiệu ứng hoạt động như interface

  • Hiệu ứng trong Prism khai báo các phép toán, còn handler gán ý nghĩa cho các phép toán đó theo mô hình algebraic effect handlers
    • effect Gen { ctl yield(Int) : Unit } khai báo phép toán yield
    • fn produce(n) : !{Gen} Unit với !{Gen} cho biết trong kiểu rằng hàm thực hiện yield
  • Cùng một producer vẫn có thể được diễn giải với ý nghĩa khác nhau tùy cách xử lý continuation k
    • total cộng các giá trị yield
    • count đếm số lần yield
    • Bỏ k đi thì thành ngoại lệ, gọi một lần thì thành trạng thái hoặc generator, gọi nhiều lần thì thành hành vi tìm kiếm
  • Ví dụ hiệu ứng Amb biểu diễn việc tìm bộ ba Pythagore bằng choose và reject
    • choose(n) cung cấp các giá trị trong phạm vi 0..n-1
    • Handler tiếp tục cùng continuation cho mỗi ứng viên để tạo cây tìm kiếm
  • Khác với OCaml 5, Prism đưa hiệu ứng vào kiểu và không cần tự tay nâng tầng như monad transformer stack của Haskell
    • Hàng hiệu ứng được gộp có cấu trúc khi đi qua các lời gọi
    • Nó hoạt động như một tập hợp nhãn chứ không phải một stack

Các tính năng được biểu diễn bằng một cơ chế duy nhất

  • Ngoại lệ

    • Trong Prism, ngoại lệ là một handler loại bỏ continuation
    • Mệnh đề final ctl bỏ k và lấy giá trị của phần thân làm kết quả của handler
    • Không phải cách lan truyền Result hay rải ? khắp call stack
    • Vì ngoại lệ là nhãn trong hàng hiệu ứng nên chúng được hợp thành như ngoại lệ mở rộng được
    • Mỗi lỗi là một phép toán riêng, và hàng trong kiểu hàm hiển thị các ngoại lệ có thể thoát ra ngoài
    • Trong ví dụ Abort và Timeout, fetch có kiểu !{Abort, Timeout}
    • with_default chỉ xử lý Timeout để trả về fallback "cached", và sau khi xử lý thì kiểu chỉ còn !{Abort}
    • Khác với checked exception của Java, chúng không bị trói vào cây phân cấp lớp mà hoạt động như một tập hợp cấu trúc mở

  • Generator và stream

    • Stream được cấu thành từ producer thực hiện emit, transformer bắt lại rồi phát tiếp, và consumer fold chúng
    • Pipeline có dạng lồng handler quanh một producer duy nhất nên về mặt cấu trúc không tạo ra danh sách trung gian
    • Ví dụ: srange(1, n).smap(square).skeep(even).stake(5).ssum()
    • Việc dừng sớm như stake(5) là một handler bỏ continuation sau khi đã lấy đủ giá trị cần thiết
    • Thư viện stream chịu ảnh hưởng từ pipes và conduit của Haskell

  • Lens

    • Lens trong Prism không phải thư viện riêng mà là sự kết hợp giữa đường dẫn cập nhật record và mô hình bộ nhớ
    • Trong record lồng nhau, có thể cập nhật nhiều trường sâu bằng một biểu thức đường dẫn duy nhất
    • Ví dụ: { g | player.pos.x = 30, player.hp = 95, score = 110 }
    • Nó dựng lại spine của record lồng nhau, nhưng nếu giá trị được sở hữu duy nhất thì sẽ tái sử dụng các ô đã tách ra
    • Nhờ cấu trúc này, cập nhật hàm có thể được biên dịch thành phép ghi con trỏ
    • Không cấp phát hay ghép nối optic type ở runtime
    • deriving (Lens) tạo ra các hàm accessor thông thường như score_of, with_score

  • Trạng thái có thể thay đổi

    • var được desugar thành các phép toán get/set của private effect
    • Handler được cài ở cuối khối sẽ xử lý hiệu ứng này
    • Phân tích closure escape sẽ từ chối trường hợp trạng thái thoát ra ngoài
    • Hàm bao ngoài vẫn có thể giữ hàng hiệu ứng rỗng

  • Thất bại

    • Thất bại được biểu diễn bằng hiệu ứng Fail ẩn danh, và hệ thống kiểu xử lý việc “biểu thức này có thể không tạo ra giá trị”
    • fail() thực hiện thất bại, còn guard(cond) thất bại khi điều kiện sai
    • ?? dùng fallback khi vế trái thất bại
    • ?. đi theo chuỗi option rồi dừng ngắn mạch
    • Guard trong comprehension sẽ cắt tỉa phần tử thất bại thay vì làm chương trình crash
    • Vì var cũng là handler sugar, khối transact có thể snapshot các biến đang sống và rollback khi thất bại

Các tính năng kiểu hiện đại

  • Prism dùng suy luận kiểu higher-rank hai chiều theo họ Dunfield-Krishnaswami để phần lớn mã nguồn không cần viết type signature
  • Ở các ranh giới cần đa hình bậc cao, binder được ghi rõ bằng forall
    • pick(g : forall a. (a) -> a) có thể áp dụng g cho cả Bool và Int
    • Với Damas-Milner core, a sẽ bị hợp nhất thành Bool ở lần gọi đầu và lần gọi thứ hai sẽ bị từ chối
  • Đa hình ad-hoc được biểu diễn bằng type class kiểu Lean
    • Instance là các giá trị có tên
    • given Ord(a) yêu cầu một dictionary
    • Khi có nhiều instance, một cái được đánh dấu canonical, còn cái khác được chỉ rõ bằng using
  • deriving sinh ra các instance và field accessor lặp lại như Eq, Ord, Show, Lens
  • Pattern matching cũng gắn với class
    • pattern First(n) for Peek = view peek là một pattern dùng phương thức class làm view
    • head_or có thể dùng cùng pattern đó cho nhiều kiểu có instance Peek
  • show hoạt động theo kiểu type-directed mà không cần class riêng
    • Trình biên dịch tổng hợp printer theo cấu trúc từ kiểu tĩnh
    • Nó không đọc runtime type tag để quyết định cách in
  • Hàng hiệu ứng cũng đa hình
    • fn twice(f : (Unit) -> Int ! {| e}) cộng kết quả bất kể hàng hiệu ứng e của hàm được truyền vào là gì
    • Với thunk thuần, e hợp nhất với hàng rỗng {}
    • Với thunk thực hiện các hiệu ứng như Tick hoặc Say, hàng đó được truyền nguyên vẹn

Cách biên dịch để giảm chi phí hiệu ứng

  • Cách cài đặt algebraic effects kiểu giáo khoa tái cấu trúc phép tính thành cây dạng free monad và có thể cấp phát các ô nhỏ cho mỗi phép toán
  • Đường đi nhanh của Prism là evidence passing theo họ Koka
    • Thay vì tái cấu trúc phép tính rồi đi tìm handler, các nhánh handler đang hoạt động được truyền tới từng điểm thao tác như tham số thông thường
    • do op được hạ thành lời gọi trực tiếp
    • Khi cài handler chỉ cần cấp phát một closure nên chi phí là O(handlers), không tỉ lệ với số lần thao tác
  • Mã hóa free monad vẫn được giữ làm fallback
    • Dành cho các phép tính thoát ra thành cấu trúc dữ liệu
    • true multishot resumption
    • và các mẫu như masked handler
  • Pipeline stream dùng phân tích luồng liên thủ tục để tính evidence hiệu ứng cần thiết xuyên qua biên hàm
    • Evidence được luồn qua producer và transformer
    • Toàn bộ chuỗi được hạ thành một vòng lặp duy nhất
    • Không có danh sách trung gian hay cấp phát ô cho mỗi thao tác
  • Cấu trúc này cho phép trình biên dịch hiệu ứng đạt kết quả tương tự stream fusion của Haskell hoặc việc đơn thể hóa iterator adapter của Rust

Mô hình bộ nhớ và runtime

  • Prism dùng tham chiếu đếm Perceus
    • Các ô heap được giải phóng một cách xác định tại các điểm biết trước về mặt tĩnh
    • Không có pause hay tracing
  • Frame-limited reuse đưa các ô vừa được tách bởi pattern match trở lại phía constructor
    • map trên danh sách sở hữu duy nhất trông như một hàm thuần trả về danh sách mới nhưng thực tế có thể trở thành thay đổi tại chỗ
    • Việc cập nhật lens được biên dịch thành ghi con trỏ cũng dựa trên cùng cơ chế này
  • Cấu trúc runtime tương tự kỷ luật bộ nhớ của Lean 4, nhưng Prism phát ra LLVM IR
    • LLVM IR được tạo thông qua inkwell
    • Nó cũng sinh mô-đun MLIR dạng văn bản cho cùng một chương trình
    • Kết quả được liên kết bằng clang với C runtime viết tay prism_rt.c
  • prism_rt.c là một runtime nhỏ khoảng 2 nghìn dòng
    • Ô heap có cấu trúc từ 4 word trở lên dạng { refcount, tag, arity, fields... }
    • Bao gồm allocator, rc_inc/rc_dec, allocator tái sử dụng tại chỗ, primitive cho bignum và chuỗi
    • Không có collector thread, card table hay safepoint
  • Allocator mặc định là libc malloc, và có cấu hình mimalloc opt-in cho benchmark
  • Live-cell oracle assert rằng heap balance bằng 0 khi kết thúc để test suite xác minh tính chất không sinh garbage

Mô hình Lean và kiểm chứng backend

  • Interpreter của Prism thuộc họ CEK machine, và cỗ máy này được phản ánh trong mô hình Lean 4 models/Prism.lean
  • Mô hình Lean 4 có định lý được kiểm chứng bằng máy rằng quan hệ small-step là xác định
    • Chương trình luôn tiến tới đúng một trạng thái kế tiếp
  • Interpreter viết bằng Rust cũng được dùng làm differential oracle
    • Mọi chương trình trong corpus đều chạy qua interpreter cùng các backend LLVM, MLIR và binary liên kết C
    • Build chỉ thành công khi đầu ra của cả bốn kết quả giống nhau từng byte
  • Tính xác định là nền tảng cho replayable durable execution
    • Ý tưởng là nếu cố định đầu vào và ghi lại quá trình chạy thì có thể phát lại bit-for-bit
    • Ở các phiên bản tương lai, Prism hướng tới việc kiểm tra tính an toàn replay sau crash như một thuộc tính kiểu

Playground WASM và mã nguồn

  • Cùng interpreter đó được biên dịch sang WASM để chạy mã Prism không cần cài đặt trong playground
  • Playground chạy chương trình trong worker
  • Có thể bấm nút để dump type signature suy luận được, effect row và core IR sau lowering
    • Có thể xem vòng lặp var hoặc pipeline stream thực sự được hạ thành dạng gì
  • Các ví dụ trong bài đều có trong menu dropdown
  • Toàn bộ mã nguồn, mô hình Lean và C runtime nằm trong prism repository on GitHub

Dòng dõi triển khai và tính chất dự án

Bài viết liên quan

1 bình luận

 
GN⁺ 2 giờ trước
Các ý kiến trên Lobste.rs

  • Không rõ lens có liên quan gì đến effect. Mỗi lần bài viết nhắc đến lens, ngoài việc chúng được gom dưới kiểu “một mẹo theo năm cách” thì trông chẳng liên quan gì đến nhau
    Và cũng không hiểu tick_use() rốt cuộc định làm gì. Tác giả kỳ vọng độc giả tự hiểu một ví dụ rối như vậy mà không cần giải thích sao? Có chú thích kiểu thì hẳn đã hữu ích

    • Về lens thì có giải thích thêm ở đây: https://sdiehl.github.io/prism/spec.html#86-optic-paths
      Dù vậy, ngoài mức ẩn dụ ra thì vẫn khó thấy lens có liên quan gì đến effect. Tác giả viết như sau:

      This is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.
      Tức là có thể hiểu ẩn dụ là: monad là giá trị, còn effect không phải là giá trị mà là một dạng cấu trúc điều khiển. Tương tự, lens là giá trị, còn optic paths của Prism không phải là giá trị, mà gần với cấu trúc điều khiển có cú pháp được hard-code hơn

  • Cần dành thêm thời gian để hiểu, nhưng thật sự trông rất đẹp

  • Thật sự ấn tượng. Chính vì vậy mà tôi lại tò mò vì sao Diehl ở cuối bài gọi compiler là đồ chơi. Nó trông như một proof of concept thành công, cho thấy một mức độ tao nhã mới

  • Muốn xem chi tiết hơn biểu diễn trung gian call-by-push-value thực tế trông như thế nào. Đặc biệt tò mò liệu nó có xử lý join point hay không
    Đã có các bài báo bàn về lý thuyết gắn effect vào CBPV. Nói rằng computation có effect type còn value thì không là khá tự nhiên, nhưng tôi chưa thấy thứ gì được cụ thể hóa đủ để áp dụng trực tiếp vào evidence passing của Koka, nên điều này khá thú vị
    Nhìn chung muốn biết nó được định vị thế nào so với Koka. Nhìn vào FBIP, Perceus và evidence passing thì rõ ràng nó được truyền cảm hứng mạnh từ công trình Koka, đồng thời việc dùng CBPV cho biểu diễn trung gian cũng khiến nó khác biệt rõ rệt. Chỉ là chưa thấy rõ khác đến mức nào

  • Trông rất giống thứ mà tôi cứ định dành thời gian để làm thử. Hay đấy!

  • Hơi lạc đề một chút, nhưng tôi luôn thấy hơi tiếc vì dự án “write you a haskell” của Stephen đã dừng lại vài năm trước. Với Prism, hy vọng sẽ có phần giải thích triển khai ở cấp độ tutorial

  • Tôi tò mò trong ngôn ngữ này thì điều gì là “không thuần”. Từ đó chỉ xuất hiện trong tiêu đề và không thấy nhắc lại trong nội dung
    Có vẻ mọi effect đều được theo dõi, nên các hàm không có effect vẫn là hàm toán học. Tôi có bỏ sót gì không?

    • Có vẻ liên quan đến việc dùng biến cục bộ khả biến bên trong định nghĩa hàm, như định nghĩa fib được đưa ra. var x là biến khả biến không thuần, còn let x là biến bất biến thuần

  • Thật sự rất hay ở chỗ những thứ thường được xem là tính năng của ngôn ngữ, ví dụ yield trong ngôn ngữ X hay throw trong ngôn ngữ Y, lại được triển khai như một interface nữa
    Việc có thể xây dựng nhiều luồng điều khiển như side effect, exception, continuation trên cùng một abstraction là một cách thú vị để nhìn lại toàn bộ các câu hỏi thiết kế, và tôi hy vọng nó sẽ hỗ trợ hoặc khơi gợi thêm nhiều khám phá và đổi mới. Có lẽ tôi sẽ còn quay lại xem trong nhiều năm tới để lấy cảm hứng