Kiểu được chứng minh như thế nào — Hệ thống kiểu của TypeScript và tương ứng Curry–Howard

Tóm tắt:

• Bài viết đưa ra góc nhìn diễn giải hệ thống kiểu của TypeScript không chỉ như một bộ kiểm tra kiểu tĩnh đơn thuần mà như một hệ thống chứng minh của logic học.
• Dựa trên tương ứng Curry–Howard (Type = Proposition, Program = Proof), bài viết giải thích về mặt khái niệm vì sao suy luận kiểu lại khả thi.
• Bài viết liên hệ các tính năng của TypeScript như kiểu hàm, generic, conditional type, type narrowing với suy hàm logic, lượng từ phổ quát và phân tích theo trường hợp.
• Quá trình kiểm tra kiểu được diễn giải như quá trình xác minh quan hệ giữa các mệnh đề chứ không phải áp dụng các quy tắc.
• Bài viết tập trung vào nền tảng thiết kế và cấu trúc toán học của hệ thống kiểu TypeScript hơn là các chi tiết triển khai.

Tóm tắt chi tiết:

1. Bối cảnh: Vì sao suy luận kiểu là khả thi?
   Trong các ngôn ngữ kiểu tĩnh, suy luận kiểu thường được giải thích như một vấn đề triển khai kiểu “trình biên dịch khớp kiểu như thế nào”.
   Bài viết này lùi lại một bước so với cách nhìn đó và đặt câu hỏi vì sao suy luận kiểu về bản chất lại có thể thực hiện được.
   Câu trả lời được đưa ra là góc nhìn xem hệ thống kiểu như một hệ thống chứng minh của logic học.

2. Nền tảng lý thuyết: tương ứng Curry–Howard
   Theo tương ứng Curry–Howard, kiểu (Type) tương ứng với mệnh đề (Proposition), còn chương trình (Program) tương ứng với chứng minh (Proof) của mệnh đề đó.
   Từ góc nhìn này, kiểm tra kiểu được diễn giải là quá trình xác minh xem chương trình có thỏa mãn một mệnh đề nhất định hay không.

3. Sự tương ứng giữa các tính năng của TypeScript và cấu trúc logic
   Bài viết kết nối các tính năng chính của TypeScript như sau.

• Kiểu hàm → suy hàm logic (Implication)
• Generic → lượng từ phổ quát (Universal Quantification)
• Conditional type / type narrowing → phân tích theo trường hợp (Case Analysis)
  Qua đó, bài viết giải thích vì sao một số biểu diễn kiểu nhất định lại tự nhiên,
  và vì sao có những kiểu về mặt cấu trúc khó biểu diễn hơn.

4. Giới hạn của hệ thống kiểu và các lựa chọn thiết kế
   Từ góc nhìn này, các ràng buộc và giới hạn của TypeScript được hiểu không phải là “thiếu tính năng” mà là những lựa chọn thiết kế để duy trì tính nhất quán logic.
   Bài viết tập trung giải thích hệ thống kiểu được hình thành trên nền tảng triết học và toán học nào, hơn là các kỹ thuật hay mẹo áp dụng trong thực tế.

[pjh2568]

Rất thú vị, tôi đã đọc rất vui. Cảm ơn bạn.

[devjeonghwan]

Dù người ta nói đây không phải là linting... nhưng nếu muốn chứng minh việc kiểm tra kiểu là sự thực thi Contract một cách nghiêm ngặt, chẳng phải contract đó phải được cưỡng chế ở cấp độ binary và runtime sao? Nếu không thì tôi nghĩ nó vẫn chỉ là kiểu linting cho type ở trạng thái cú pháp còn lơ lửng mà thôi.

[tsboard]

Nội dung thật ấn tượng. Đây là lần đầu tiên tôi biết rằng có thể nhìn nhận theo góc độ như vậy. Tôi cũng đã chia sẻ liên kết bài blog trong công ty để đồng nghiệp cùng đọc thử. Cảm ơn bạn!