Elixir v1.20 ra mắt: Hệ thống kiểu dần và khả năng phát hiện lỗi tự động

Elixir v1.20, một bản cập nhật lớn của ngôn ngữ lập trình chạy trên máy ảo BEAM, đã chính thức ra mắt. Điểm nhấn quan trọng nhất của phiên bản này là sự hoàn thiện cột mốc phát triển đầu tiên cho hệ thống kiểu dựa trên lý thuyết tập hợp (set-theoretic types). Điều này giúp Elixir thực hiện suy luận kiểu (type inference) và kiểm tra từng chương trình một cách dần dần mà không cần các chú thích kiểu (type annotations) từ lập trình viên.

Theo José Valim, hệ thống mới này giúp Elixir ngày càng báo cáo nhiều "code chết" (dead code) và các lỗi đã được xác nhận (verified bugs) - những lỗi kiểu vi phạm chắc chắn sẽ gây thất bại tại thời điểm chạy. Đặc biệt, hệ thống hoạt động hiệu quả mà không làm tăng gánh nặng cho người phát triển và giữ tỷ lệ báo cáo dương tính giả (false positives) ở mức cực thấp.

Mục tiêu của hệ thống kiểu mới

Hệ thống kiểu được giới thiệu trong Elixir v1.20 tập trung vào ba tiêu chí cốt lõi:

• Đúng đắn (Sound): Các kiểu được suy luận và gán bởi hệ thống phải phù hợp với hành vi thực tế của chương trình.
• Dần dần (Gradual): Elixir bao gồm kiểu dynamic(), được sử dụng khi kiểu của biến hoặc biểu thức được kiểm tra tại thời điểm chạy. Nếu không có dynamic(), hệ thống sẽ hoạt động như một hệ thống kiểu tĩnh (static type system).
• Thân thiện với nhà phát triển: Các kiểu được mô tả và kết hợp bằng các phép toán tập hợp cơ bản: hợp (union), giao (intersection) và phủ định (negation).

Điểm đặc biệt của kiểu dynamic()

Nhiều hệ thống kiểu dần khác thường sử dụng kiểu any(), khiến hệ thống coi "mọi thứ đều ổn" và bỏ qua các vi phạm kiểu. Tuy nhiên, kiểu dần của Elixir gọi là dynamic() và có hai tính chất quan trọng: tính tương thích (compatibility) và khả năng thu hẹp (narrowing).

Tính tương thích (Compatibility)

Trong các hệ thống kiểu tĩnh, việc truyền một biến có thể là integer() hoặc binary() vào một hàm chỉ chấp nhận số nguyên có thể gây lỗi. Tuy nhiên, điều này đôi khi dẫn đến các báo cáo dương tính giả ở những đoạn mã hoàn toàn hợp lệ.

Để giải quyết vấn đề này, Elixir gắn thẻ các biến như vậy là dynamic(integer() or binary()). Khi gọi một hàm với kiểu dynamic(), Elixir chỉ báo cáo vi phạm kiểu nếu các kiểu được cung cấp và các kiểu được chấp nhận là rời nhau (disjoint).

Ví dụ, nếu Map.fetch! yêu cầu một map và biến của bạn chỉ có thể là integer hoặc binary, đây là hai tập hợp rời nhau, dẫn đến vi phạm. Nhưng nếu hàm chấp nhận number (số) và biến của bạn có thể là integer, vì integer là một phần của number, không có vi phạm nào được báo cáo. Cơ chế này giúp Elixir chỉ báo cáo những lỗi đã được xác nhận là sẽ gây lỗi thực sự.

Khả năng thu hẹp (Narrowing)

Nếu chỉ báo cáo lỗi khi các kiểu hoàn toàn rời nhau, hệ thống sẽ bỏ sót nhiều lỗi. Do đó, Elixir triển khai khả năng thu hẹp kiểu dynamic(). Hệ thống sẽ tinh chỉnh kiểu của biến dựa trên cách nó được sử dụng trong chương trình.

Ví dụ, nếu bạn có biến data kiểu dynamic() và trong code bạn truy cập data.a và data.b, Elixir sẽ thu hẹp data thành một map có shape %{..., a: number(), b: number()}. Nếu sau đó bạn cố gắng sử dụng data như một số nguyên, hệ thống sẽ phát hiện xung đột và báo lỗi vi phạm.

Kiểm tra kiểu trong Guards và Pattern Matching

Phần lớn công việc trong bản phát hành này là đưa khả năng kiểm tra và thu hẹp kiểu vào nhiều cấu trúc ngôn ngữ khác nhau, đặc biệt là các câu lệnh bảo vệ (guards) và khớp mẫu (pattern matching).

Hệ thống giờ đây có thể suy luận chính xác kiểu trong các guards phức tạp:

• def example(x, y) when is_list(x) and is_integer(y): Suy luận x là list và y là integer.
• def example(x) when is_map_key(x, :foo): Suy luận x là map có khóa :foo.
• def example(x) when not is_map_key(x, :foo): Suy luận x là map không có khóa :foo, có dạng %{..., foo: not_set()}.

Ngoài ra, việc khớp mẫu trên nhiều mệnh đề (clauses) của hàm cũng giúp thu hẹp kiểu. Nếu mệnh đề đầu tiên xử lý trường hợp nil, hệ thống sẽ biết rằng ở các mệnh đề sau, biến đó không còn là nil nữa.

Cải thiện tốc độ biên dịch

Elixir v1.20 không chỉ mạnh về kiểu dữ liệu mà còn cải thiện tốc độ biên dịch (compilation times), đặc biệt trên các ứng dụng chạy trên máy có nhiều nhân (multi-core). Các chuẩn mực tổng hợp hiện xếp hạng công cụ xây dựng của Elixir là nhanh nhất trong số các ngôn ngữ BEAM.

Bản cập nhật cũng giới thiệu tùy chọn trình biên dịch mới là :module_definition. Tùy chọn này cho phép chỉ định việc định nghĩa module nên được :compiled (biên dịch - mặc định) hay :interpreted (thông dịch). Việc chuyển sang chế độ thông dịch có thể cải thiện thời gian biên dịch trong các dự án lớn mà không ảnh hưởng đến tệp .beam được ghi ra đĩa.

Những bước đi tiếp theo

Câu hỏi lớn nhất đặt ra là khi nào Elixir sẽ giới thiệu các chữ ký kiểu (type signatures) sử dụng kiểu lý thuyết tập hợp. Theo José Valim, vẫn còn cả nghiên cứu và phát triển phía trước.

Chữ ký kiểu sẽ chỉ được giới thiệu khi:

• Hiệu suất của hệ thống kiểu trong v1.20 được tối ưu hóa tối đa.
• Có thể triển khai các kiểu đệ quy (recursive types) hiệu quả.
• Có thể triển khai các kiểu tham số (parametric types) hiệu quả.
• Giải quyết được vấn đề duyệt các cặp key-value của map như một enumerable.

Cho đến lúc đó, người dùng Elixir có thể tận dụng khả năng phát hiện lỗi tự động mới ngay lập tức mà không cần thay đổi code hiện tại của họ.