Những ý tưởng hay trong ngôn ngữ lập trình: Flow Typing, Borrow Checker và Contract Programming

Trong thế giới ngôn ngữ lập trình, có những tính năng tưởng chừng nhỏ bé nhưng lại thay đổi hoàn toàn cách chúng ta viết và suy nghĩ về mã nguồn. Một bài viết gần đây trên blog cá nhân của Pranoy Dutta đã điểm lại ba ý tưởng mà theo tác giả là "hay" nhất: flow typing, borrow checking và contract programming. Đây đều là những khái niệm đáng để các lập trình viên Việt Nam tìm hiểu, dù bạn đang làm việc với ngôn ngữ nào.

Flow Typing — Kiểu tĩnh nhưng linh động

Ý tưởng đầu tiên mà tác giả bắt gặp lần đầu ở ngôn ngữ Crystal. Đây là một ngôn ngữ biên dịch có kiểm tra kiểu tĩnh, nhưng cú pháp lại rất giống Ruby. Điều khiến Crystal mang cảm giác của một ngôn ngữ động nằm ở chỗ: một biến có thể được gán cho nhiều kiểu khác nhau trong suốt vòng đời của nó, khác với hầu hết các ngôn ngữ kiểu tĩnh mà tác giả từng dùng.

Ví dụ điển hình: một biến ban đầu là Int32, sau đó trong một nhánh điều kiện nào đó lại được gán thành String. Điều thú vị là trình biên dịch không gán cứng một kiểu duy nhất cho biến, mà hiểu rằng kiểu của nó là hợp của mọi khả năng — tức Int32 | String. Khi bạn gọi một phương thức chỉ có ở String lên biến đó, trình biên dịch sẽ buộc bạn phải thêm kiểm tra như is_a?(String) để thu hẹp kiểu trước.

Đây là ví dụ tuyệt vời về việc dùng suy luận kiểu tinh vi để khiến ngôn ngữ biên dịch mang cảm giác động mà không phải trả giá nhiều về hiệu năng lúc chạy.

Đáng chú ý là TypeScript cũng có flow typing và type narrowing, nên nếu bạn đang làm việc với JavaScript/TypeScript, bạn có thể đã quen với sức mạnh này.

Borrow Checking — Chặn data race ngay khi biên dịch

Rust là ngôn ngữ lập trình hệ thống đảm bảo an toàn bộ nhớ mà không cần bộ thu gom rác (garbage collector). Một trong những lỗi nguy hiểm nhất trong lập trình song song là data race — khi nhiều luồng cùng đọc và ghi vào một vùng nhớ mà không có đồng bộ.

Borrow checker là cơ chế giúp Rust ngăn chặn data race ngay từ lúc biên dịch, dựa trên hai quy tắc:

• Mọi tham chiếu (borrow) không được sống lâu hơn phạm vi của chủ sở hữu
• Bạn chỉ có thể có hoặc đúng 1 tham chiếu có thể thay đổi (&mut T), hoặc 1 hay nhiều tham chiếu bất biến (&T) — không thể có cả hai

Quy tắc này hẳn khiến nhiều người liên tưởng đến khóa đọc–ghi (readers-writer lock), nơi cho phép nhiều luồng đọc hoặc một luồng ghi duy nhất. Lý do là để ngăn data race, ta chỉ cần đồng bộ thao tác đọc so với thao tác ghi. Tác giả đánh giá borrow checker là một giải pháp thanh lịch cho bài toán data race, một dạng trừu tượng không tốn chi phí lúc chạy, chỉ đánh đổi bằng kiểm tra lúc biên dịch và độ phức tạp tăng thêm.

Contract Programming — Bất biến được viết thành cú pháp

Cuối cùng là contract programming, được ngôn ngữ D hỗ trợ ở mức cú pháp. Nếu bạn từng dùng câu lệnh assert, bạn đã chạm đến ý tưởng này: mọi chương trình đều có những bất biến cần được duy trì, chẳng hạn "ngày này luôn nằm sau ngày kia" hay "cây này luôn cân bằng".

D phân biệt rõ hai ngữ nghĩa:

• assert dùng cho việc vi phạm bất biến nội tại của chương trình — nếu bị kích hoạt, đó là lỗi đúng đắn (correctness bug)
• enforce dùng khi có vấn đề từ bên ngoài như dữ liệu người dùng nhập sai hay lỗi môi trường — nó sẽ ném ra ngoại lệ

Ngoài ra, D còn hỗ trợ cú pháp cho điều kiện tiên quyết (pre-condition) và điều kiện hậu quyết (post-condition) ở cấp hàm. Ví dụ, hàm daysInFebruary có hậu điều kiện rằng nó chỉ được trả về 28 hoặc 29 — bất kỳ giá trị nào khác đều là lỗi logic.

Ở cấp lớp, D có khối invariant để đảm bảo dữ liệu của đối tượng luôn nhất quán. Tác giả lấy ví dụ một lớp BankAccount với số dư không bao giờ được âm: khối invariant() được kiểm tra tự động, còn các phương thức như deposit hay withdraw có thể khai báo điều kiện tiên quyết và hậu quyết riêng. Cách viết này sạch sẽ và dễ bảo trì hơn nhiều so với việc rải các hàm kiểm tra nhất quán ở đầu và cuối mỗi phương thức.

Với lập trình viên Việt Nam, ba ý tưởng này đáng để tham khảo ngay cả khi bạn chưa dùng Crystal, Rust hay D. Hiểu về flow typing sẽ giúp bạn viết TypeScript tốt hơn; hiểu borrow checking sẽ giúp bạn tránh các lỗi đồng bộ trong Go, Java hay C++; và tư duy contract programming có thể áp dụng trong bất kỳ ngôn ngữ nào qua các thư viện kiểm tra và viết test kỹ lưỡng.