Bạn viết let x = 42 trong TypeScript hay Rust, không khai báo kiểu, nhưng compiler vẫn biết x là số nguyên. Tính năng này gọi là type inference. Đằng sau nó là một hệ thống ràng buộc tinh vi mà nhiều lập trình viên dùng hằng ngày nhưng ít khi tìm hiểu kỹ.

Bài toán cốt lõi: mỗi biểu thức đều có kiểu

Ý tưởng cốt lõi rất đơn giản: mọi biểu thức trong chương trình đều mang một kiểu dữ liệu, dù lập trình viên có viết ra hay không. Compiler gán cho mỗi biểu thức chưa biết kiểu một "biến kiểu" tạm thời, ví dụ T1, T2. Sau đó nó duyệt cây cú pháp (AST) từ trên xuống, thu thập các ràng buộc. Khi bạn viết x + 1, compiler tạo ràng buộc: T_x = int, vì phép cộng yêu cầu toán hạng là số. Khi bạn gọi f(x) mà f có kiểu string → bool, compiler suy ra T_x = string.

Unification: giải hệ phương trình kiểu

Sau khi thu thập xong, compiler cần giải hệ ràng buộc. Thuật toán cổ điển là unification, do Robinson đề xuất năm 1965. Nguyên tắc hoạt động giống như giải hệ phương trình đại số: nếu T1 = List[T2] và T1 = List[int], thì T2 = int. Unification thay thế từng biến kiểu bằng một kiểu cụ thể, rồi lan truyền thông tin qua toàn bộ chương trình. Nếu hai ràng buộc mâu thuẫn, ví dụ T1 = int và T1 = string, compiler báo lỗi kiểu ngay tại thời điểm biên dịch, không cần chạy chương trình.

Hindley-Milner: nền tảng lý thuyết

Hệ thống type inference mạnh nhất cho ngôn ngữ hàm là Hindley-Milner (HM), được J. Roger Hindley mô tả năm 1969 và Robin Milner tái phát hiện độc lập năm 1978. HM có một tính chất đặc biệt: nó luôn tìm được "kiểu tổng quát nhất" (principal type) mà không cần bất kỳ chú thích nào từ lập trình viên. Ví dụ, hàm identity x = x sẽ được suy luận thành kiểu ∀a. a → a, nghĩa là nó chấp nhận mọi kiểu đầu vào. Thuật toán W của Damas-Milner kết hợp duyệt cây cú pháp với unification, chạy trong thời gian gần tuyến tính với kích thước chương trình trong hầu hết trường hợp thực tế.

Từ ML đến TypeScript: type inference trong thực tế

HM lần đầu được triển khai trong ngôn ngữ ML vào thập niên 1970, sau đó trở thành nền tảng cho Haskell, OCaml, F# và Elm. Nhưng các ngôn ngữ lập trình hiện đại thường mở rộng HM theo nhiều hướng. Rust dùng type inference cục bộ kết hợp với hệ thống ownership, nên đôi khi bạn vẫn phải khai báo kiểu tại ranh giới hàm. TypeScript dùng cơ chế kiểm tra kiểu hai chiều: vừa suy luận từ dưới lên, tức từ giá trị suy ra kiểu, vừa kiểm tra từ trên xuống, tức ngữ cảnh áp đặt kiểu. Cách tiếp cận lai này giúp xử lý các tình huống phức tạp như callback lồng nhau hay kiểu generic, vốn là điểm yếu của HM thuần túy.

Giới hạn và đánh đổi

Type inference không phải phép màu. Khi hệ thống kiểu trở nên phức tạp hơn, chẳng hạn có dependent types hay higher-kinded types, bài toán suy luận có thể trở nên không thể quyết định (undecidable). Ngay cả HM cũng có trường hợp xấu nhất với độ phức tạp hàm mũ, dù điều này hiếm khi xảy ra trong mã thực tế. Đó là lý do Rust và Go vẫn yêu cầu khai báo kiểu ở ranh giới hàm, một sự đánh đổi có chủ đích giữa tiện lợi cho lập trình viên và tốc độ biên dịch. Thông điệp lỗi cũng là một thách thức lớn. Khi unification thất bại, compiler biết hai kiểu mâu thuẫn nhau, nhưng xác định chính xác dòng code nào gây ra lỗi đòi hỏi heuristic phức tạp, và đây vẫn là lĩnh vực nghiên cứu AI đang được ứng dụng để cải thiện.