Hệ thống kiểu

Bài này viết về hệ thống kiểu nhìn từ góc độ lập trình máy tính. Đối với một công thức lý thuyết, xem lý thuyết kiểu.

Trong ngôn ngữ lập trình, hệ thống kiểu (tiếng Anh: type system) là một tập các quy tắc gán một thuộc đặc tính gọi là kiểu cho các cấu trúc khác nhau của một chương trình máy tính bao gồm, như biến, biểu thức, hàm hay mô đun.

Những kiểu này chính thức hóa và bắt buộc (một cách ngầm định) các loại mà lập trình viên sử dụng cho cấu trúc dữ liệu và thành phần, ví dụ như: "chuỗi" (string), "mảng số thực" (array of float), "hàm trả về giá trị boolean"). Mục đích chính của hệ thống kiểu là để giảm khả năng lỗi trong chương trình máy tính bằng cách định nghĩa giao diện giữa các phần của chương trình máy tính, và sau đó kiểm tra các bộ phận được kết nối theo một cách nhất quán. Kiểm tra có thể xảy ra tĩnh (vào thời gian biên dịch - compile time), động (vào thời gian chạy -- run time), hay là sự kết hợp của kiểm tra tĩnh và động. Hệ thống kiểu còn có mục đích khác, như cho phép tối ưu hóa trình biên dịch nhất định, cho phép đa điều phối (multiple dispatch), cung cấp một dạng tài liệu,...

Một hệ thống kiểu liên kết mỗi kiểu với một giá trị tính toán, bằng cách kiểu tra dòng của những giá trị đó, cố gắng bảo đảm hay chứng minh rằng không có lỗi kiểu nào có thể xảy ra. Hệ thống kiểu đã cho xác định chính xác những gì cấu thành lỗi kiểu, nhưng nói chung mục đích là để ngăn các toán tử sử dụng được những loại giá trị mà hoạt động tính toán trên đó không có ý nghĩa (lỗi logic); lỗi bộ nhớ cũng sẽ được ngăn chặn. Hệ thống kiểu thường được đặc tả như là một phần của ngôn ngữ lập trình, và xây dựng trong trình thông dịch và trình biên dịch của ngôn ngữ đó; mặc dù hệ thống kiểu của nogon ngữ có thể được mở rộng bởi các công cụ tùy chọn (extended static checking) để thực hiện các loại kiểm tra bổ sung sử dụng cú pháp và ngữ pháp kiểu gốc của ngôn ngữ đó.

Tổng quan về sử dụng

Một ví dụ về hệ thống kiểu đơn giản là về ngôn ngữ C. Một phần của một chương trình C là về định nghĩa hàm. Một hàm được gọi bởi hàm khác. Giao diện của một hàm mô tả tên của hàm và danh sách các giá trị được truyền vào trong mã của nó. Mã của hàm được gọi mô tả tên được gọi, cùng với tên các biến nắm giữ giá trị được truyền vào nó. Trong quá trình thực thi, những giá trị được đặt vào bộ nhớ tạm, rồi thực thi nhảy tới mã của hàm được gọi. Mã của hàm được gọi truy xuất những giá trị đó và sử dụng chúng. Nếu các lệnh bên trong hàm được viết với giả thiết nhận được giá trị số nguyên (integer), nhưng mã được gọi truyền đến một giá trị dấu chấm động (floating-point), như vậy kết quả sai sẽ được trả về bởi hàm được gọi. Bộ biên dịch C kiểm tra kiểu được định nghĩa cho mỗi biến được gửi đi, với kiểu được định nghĩa trong giao diện của hàm được gọi. Nếu các kiểu không khớp, trình biên dịch sẽ trả ra một lỗi biên dịch (compile-time error).

Một trình biên dịch cũng có thể sử dụng kiểu tĩnh của giá trị để tối ưu hóa bộ nhớ cần thiết và chọn lựa giải thuật để hoạt động trên giá trị đó. Trong nhiều trình biên dịch của C, ví dụ như kiểu dữ liệu số thực (float), được biểu diễn bằng 32 bit, theo như đặc tả IEEE cho con số dấu chấm động chính xác đơn. Do vậy họ sẽ dùng các toán tử vi xử lý chuyên cho dấu chấm động (ví dụ như phép cộng, phép nhân dấm chấm động...).

Cơ bản

Hiểu một cách chính thức thì lý thuyết kiểu nghiên cứu về hệ thống kiểu. Một ngôn ngữ lập trình phải có kiểm tra kiểu (type check) bằng cách sử dụng hệ thống kiểu cho dù ở thời gian biên dịch hay thời gian chạy, ghi chú thủ công hay tự động suy ra. Như Mark Manasse đã nói rõ rằng:

Vấn đề cơ bản được chỉ ra bởi lý thuyết kiểu là để bảo đảm chương trình có ý nghĩa. Vấn đề cơ bản gây ra bởi lý thuyết kiểu là các chương trình có ý nghĩa có thể không có ý nghĩa vốn được gán cho chúng. Việc tìm kiếm hệ thống kiểu phong phú hơn là kết quả của sự căng thẳng này.

Cho dù là được tự động bởi trình biên dịch hay được đặc tả bởi lập trình viên, hệ thống kiểu sẽ khiến hành vi chương trình trở nên bất hợp pháp nếu nó nằm ngoài quy tắc hệ thống kiểu. Ưu điểm của hệ thống kiểu đặc tả bởi lập trình viên gồm:

• Trừu tượng hóa (abstraction) hay mô đun hóa (modularity) – Các kiểu cho phép lập trình viên suy nghĩ ở mức cao hơn mức bit hoặc byte mà không cần quan tâm đến hiện thực ở mức thấp hơn. Ví dụ, lập trình viên có thể bắt đầu nghĩ về chuỗi (string) như là một tập các giá trị kí tự thay vì một mảng các byte. Cao hơn một chút, kiểu cho phép lập trình viên nghĩ và thể hiện giao diện giữa hai hệ thống con với bất kì kích thước nào. Điều này cho phép nhiều mức độ địa phương hóa để các định nghĩa cần thiết cho tính tương hợp giữa các hệ thống con vẫn thống nhất khi hai hệ thống giao tiếp với nhau.
• Tài liệu hóa (documentation) – Trong các hệ thống kiểu lớn hơn, kiểu có thể đóng vai trò như tài liệu để làm rõ mục đích của lập trình viên. Ví dụ, nếu lập trình viên định nghĩa một hàm trả về kiểu thời gian (timestamp), nó ghi tài liệu hàm với kiểu thời gian được khai báo tường minh trong mã với kiểu số nguyên.

Ưu điểm của hệ thống kiểu đặc tả bởi trình biên dịch gồm:

• Tối ưu hóa (optimization) – Kiểm tra kiểu tĩnh có thể cung cấp thông tin thời gian biên dịch có ích. Ví duk, nếu một kiểu yêu cầu giá trị nằm trong bộ nhớ phải là bộ số của 4 byte, trình biên dịch có thể sử dụng lệnh máy hiệu quả hơn.
• An toàn (safety) – Một hệ thống kiểu cho phép trình biên dịch phát hiện mã vô nghĩa hay có thể là mã không phợp lệ. Ví dụ, chúng ta có thể xác định biểu thức 3 / "Hello, World" là không hợp lệ, vì các quy tắc không xác định được cách chia một số nguyên cho một chuỗi. Kiểu mạnh hường an toàn hơn, nhưng không thể bảo đảm an toàn kiểu (type safety) được.

Kiểm tra kiểu

Quán trình kểm tra và thực thi các ràng buộc của kiểu—kiểm tra kiểu (type checking)— có thể xảy ra ở thời gian biên dịch (kiểm tra tĩnh) hoặc thời gian chạy. Nếu một đặc tả ngôn ngữ yêu cầu các quy tắc kiểu mạnh (ví dụ, chỉ cho phép ít hay nhiều việc chuyển đổi kiểu tự động mà không làm mất thông tin), quá trình đó gọi là kiểu mạnh, còn không, gọi là kiểu yếu. Các thuật ngữ này thường không được dùng theo nghĩa chặt chẽ.

Kiểm tra kiểu tĩnh

Kiểm tra kiểu tĩnh (static type checking) là quá trình xác minh an toàn kiểu của một chương trình dựa vào sự phân tích văn bản (mã nguồn) của chương trình. Nếu một chương trình vượt qua được bộ kiểm tra kiểu tĩnh, khi đó chương trình đảm bảo đáp ứng được một số đặc tính an toàn cho tất cả đầu vào.

Kiểm tra kiểu động và thông tin kiểu thời gian chạy

Kiểm tra kiểu động (dynamic type checking) là quá trình xác minh an toàn kiểu của chương trình vào thời gian chạy.

Kết hợp kiểm tra kiểu tĩnh và động

Một số ngôn ngữ cho phép cả kiểm tra kiểu tĩnh và động, đôi khi gọi là kiểm tra kiểu mềm (soft typing).

Kiểm tra kiểu tĩnh và động trong thực tế

Cần sự đánh đổi nhất định khi lựa chọn giữa kiểm tra kiểu tĩnh và động.

Hệ thống kiểu mạnh và kiểu yếu

Bài chi tiết: Kiểu mạnh và kiểu yếu

An toàn kiểu và an toàn bộ nhớ

Bài chi tiết: An toàn kiểu

Các mức độ kiểm tra kiểu

Một số ngôn ngữ cho phép các mức độ kiểm tra kiểu khác nhau áp dụng cho từng vùng mã khác nhau.

Hệ thống kiểu tùy chọn

Nó được đề xuất chủ yếu bởi Gilad Bracha, cho phép lựa chọn hệ thống kiểu có thể độc lập với lựa chọn ngôn ngữ; như vậy một hệ thống kiểu nên là một mô đun để có thể gắn vào một ngôn ngữ khi cần.

Đọc thêm

• Cardelli, Luca; Wegner, Peter (tháng 12 năm 1985). “On Understanding Types, Data Abstraction, and Polymorphism” (PDF). ACM Computing Surveys. New York, NY, USA: ACM. 17 (4): 471–523. doi:10.1145/6041.6042. ISSN 0360-0300.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.
• Cardelli, Luca (2004). “Type systems”. Trong Allen B. Tucker (biên tập). CRC Handbook of Computer Science and Engineering (PDF) (ấn bản 2). CRC Press. ISBN 158488360X.
• Tratt, Laurence, Dynamically Typed Languages, Advances in Computers, Vol. 77, pp. 149–184, July 2009

Liên kết ngoài

• Smith, Chris, What To Know Before Debating Type Systems