Tôi từng có những trải nghiệm tồi tệ khi mở một hàm có cái tên vô cùng hiền lành trong một codebase hệ thống cũ, lần dò qua ba lớp hàm helper bên dưới, để rồi kinh hoàng phát hiện ra nó đang âm thầm gọi kết nối mạng, ghi dữ liệu xuống cache và đôi khi tự ý cấp phát một buffer bộ nhớ khổng lồ trên heap. Cảm giác đó cực kỳ quen thuộc với bất kỳ ai từng chịu trách nhiệm bảo trì hệ thống: mã nguồn không nói dối bạn, nhưng nó bắt bạn phải đọc hết cả gia phả dòng họ nhà nó thì mới chịu nói ra sự thật.
Chữ ký kiểu truyền thống chỉ cho biết hàm nhận vào tham số kiểu gì và trả về kết quả kiểu gì. Nó hoàn toàn im lặng trước câu hỏi: "Hàm này sẽ làm gì với thế giới vật lý xung quanh trong quá trình tính toán ra kết quả đó?" Một hàm load_config(path) -> Config hoàn toàn có thể đọc ghi file trên đĩa, sử dụng bộ nhớ cache toàn cục, kết nối mạng để tải cấu hình dự phòng, ghi log lỗi ra console và tự sập chương trình (panic) khi mất mạng. Tất cả các hành vi ấy đều hoàn toàn hợp lệ về mặt kiểu dữ liệu đầu vào/đầu ra, nhưng lại khác biệt nhau một trời một vực về mặt chi phí vận hành và rủi ro hệ thống.
Hệ thống effects đưa toàn bộ câu chuyện hành vi ẩn ấy vào trong hợp đồng tĩnh của chữ ký hàm:
fn load_config(path: str) -> Result[Config, IOError]
effect io, alloc
Từ khóa io không nói rõ file nào sẽ được mở. Từ khóa alloc không báo cáo chính xác bao nhiêu byte bộ nhớ sẽ được yêu cầu cấp phát. Nhưng chúng làm một việc có ích hơn nhiều: công bố sòng phẳng loại hành vi phụ mà lời gọi hàm này chắc chắn sẽ gây ra cho hệ thống. Một hàm khác nếu không khai báo các hiệu ứng phụ tương đương trong chữ ký của mình sẽ bị trình biên dịch cấm tuyệt đối không cho phép lén lút gọi hàm load_config này.
Điều này tạo ra một sự thấu hiểu và đồng cảm sâu sắc giữa người thiết kế API và người bảo trì hệ thống. Người viết API buộc phải thừa nhận chi phí vận hành mà mình tạo ra. Người gọi hàm không cần phải nghi ngờ điều tra mọi lớp trừu tượng ẩn. Người duyệt mã (reviewer) chỉ cần nhìn vào sự thay đổi chữ ký effect trong file diff để nhận diện ngay lập tức một sự thay đổi hành vi hệ thống nhạy cảm. Cấu hình nhúng (embedded profile) có thể từ chối biên dịch bất kỳ đoạn mã nào kéo theo effect alloc. Một ca kiểm thử pure (thuần khiết) có thể bảo đảm chắc chắn rằng đường dẫn thực thi của nó không bao giờ vô tình chạm vào các thiết bị vật lý bên ngoài. Trợ lý AI có thể định vị chính xác ranh giới của hiệu ứng phụ thay vì đứng phỏng đoán mò mẫm qua tên hàm.
Nhưng hệ thống effects cũng có thể biến mã nguồn thành một bãi rác chữ nghĩa ồn ào. Nếu mỗi hàm helper nhỏ đều truyền ngược một danh sách dài dằng dặc các effects lên toàn bộ đồ thị lời gọi hàm (call graph), chữ ký hàm sẽ nhanh chóng biến thành một bản khai thuế phức tạp. Nếu cơ chế suy luận (inference) quá mạnh mẽ chạy ngầm, lập trình viên lại hoàn toàn mất đi khả năng kiểm soát xem hiệu ứng phụ xuất hiện từ đâu trong codebase. Nếu taxonomy (phân loại) effects bị phình to quá sớm với hàng loạt từ khóa chi tiết như io, net, time, thread, random, panic, alloc, mut, unsafe..., DUY sẽ trở thành một ngôn ngữ cực kỳ chính xác về mặt lý thuyết toán học nhưng không một lập trình viên thực tế nào muốn viết.
Vì vậy, phiên bản đầu tiên của DUY phải cực kỳ tiết chế. Chúng tôi chỉ chọn ra một vài effects cốt lõi có tác động trực tiếp đến kiến trúc hệ thống để đưa vào kiểm tra tĩnh. Trình biên dịch được phép tự động suy luận effects trong phạm vi thực thi nội bộ của hàm, nhưng bắt buộc phải yêu cầu lập trình viên khai báo tường minh tại ranh giới các API công khai. Hệ thống diagnostics phải chỉ ra chính xác chuỗi lời gọi hàm (call chain) nào đã kéo một effect nhạy cảm vào chương trình. Mục tiêu tối thượng của DUY không phải là biến mọi dòng code thành các công thức toán học khô khan, mà là buộc các chi phí vận hành quan trọng phải chấm dứt việc đóng giả làm vô hình đằng sau các abstraction.
Các nghiên cứu khoa học về row-polymorphic effects trong ngôn ngữ Koka cung cấp cho DUY một nền tảng học thuật tuyệt vời để kế thừa, nhưng DUY bắt buộc phải tự kiểm chứng trải nghiệm lập trình trên chính sản phẩm của mình. Một hệ thống effects đẹp đẽ và bóng bẩy trong các bài báo khoa học chưa chắc đã là một hệ thống dễ chịu trong file log của một kỹ sư đang toát mồ hôi xử lý sự cố hệ thống lúc nửa đêm.
Effects là ngôn ngữ của sự thật, nhưng sự thật ấy bắt buộc phải được diễn đạt bằng một tông giọng mà con người có thể lắng nghe và thấu hiểu. Bài toán tương tự xuất hiện ở thiết kế memory model: phải nghiêm khắc đến mức nào để bảo vệ an toàn bộ nhớ cho lập trình viên, và phải đơn giản đến mức nào để họ không nản lòng vứt bỏ ngôn ngữ trước khi kịp nhận được sự bảo vệ ấy?
Bình luận (0)
Đang tải bình luận...