Các kiểu phụ thuộc và kiểu cấu trúc con

Các kiểu phụ thuộc cho phép các kiểu phụ thuộc vào giá trị, cho phép các đặc tả chính xác, trong khi các kiểu cấu trúc con như kiểu tuyến tính và kiểu affine kiểm soát cách tài nguyên được sử dụng.

Definition

Các kiểu phụ thuộc là các kiểu phụ thuộc vào giá trị, cho phép các thuộc tính chính xác được nêu và kiểm tra ở cấp độ kiểu; các hệ thống kiểu cấu trúc con hạn chế cách các biến (tài nguyên) có thể được sao chép hoặc loại bỏ, với các kiểu tuyến tính yêu cầu mỗi biến được sử dụng chính xác một lần.

Scope

Chủ đề này bao gồm các nguyên tắc phân loại nâng cao vượt ra ngoài các hệ thống thông thường: các kiểu phụ thuộc, trong đó các kiểu có thể đề cập đến các giá trị chương trình, cho phép các kiểu thể hiện các đặc tả đầy đủ và đóng vai trò là bằng chứng; và các kiểu cấu trúc con (tuyến tính, affine, sở hữu), hạn chế các quy tắc cấu trúc của co rút và suy yếu để theo dõi việc sử dụng tài nguyên, bí danh và thời gian tồn tại. Nó kết nối với sự tương ứng Curry-Howard và các trợ lý chứng minh.

Core questions

• Làm thế nào các kiểu có thể phụ thuộc vào giá trị để thể hiện các đặc tả chương trình đầy đủ?
• Sự tương ứng giữa các kiểu phụ thuộc và các bằng chứng xây dựng là gì?
• Các kiểu tuyến tính và affine mô hình hóa tài nguyên, quyền sở hữu và an toàn bộ nhớ như thế nào?
• Những đánh đổi về tính quyết định và khả năng sử dụng của các hệ thống phong phú này là gì?

Key theories

Lý thuyết kiểu trực giác (phụ thuộc)

Lý thuyết kiểu của Martin-Löf thống nhất lập trình và logic xây dựng sao cho các kiểu là mệnh đề và các chương trình là bằng chứng, cung cấp nền tảng cho các ngôn ngữ có kiểu phụ thuộc và các trợ lý chứng minh.

Logic tuyến tính và các kiểu tuyến tính

Logic tuyến tính của Girard tinh chỉnh logic cổ điển và trực giác bằng cách kiểm soát các quy tắc cấu trúc, và Wadler đã chỉ ra cách các kiểu tuyến tính được xây dựng trên đó có thể quản lý an toàn việc cập nhật tại chỗ và sử dụng tài nguyên.

Tĩnh học cho các hệ thống cấu trúc con

Harper phát triển siêu lý thuyết về các hệ thống kiểu cấu trúc con và các hệ thống kiểu nâng cao khác trong một khuôn khổ tĩnh-động thống nhất, làm rõ tính đúng đắn và cách giải thích tài nguyên của chúng.

Clinical relevance

Các kiểu phụ thuộc cung cấp sức mạnh cho các trợ lý chứng minh và phần mềm đã được xác minh, nơi các chương trình đi kèm với các đảm bảo chính xác được máy kiểm tra. Các kiểu cấu trúc con và kiểu sở hữu làm nền tảng cho các ngôn ngữ hệ thống an toàn về bộ nhớ và đồng thời, cho phép quản lý tài nguyên thủ công an toàn mà không cần bộ thu gom rác.

History

Lý thuyết kiểu trực giác của Martin-Löf (những năm 1970-1980) đã thiết lập các kiểu phụ thuộc và quan điểm mệnh đề-như-kiểu, dẫn đến các trợ lý chứng minh như Coq, Agda và Lean. Logic tuyến tính năm 1987 của Girard đã giới thiệu lý luận nhạy cảm với tài nguyên; các kiểu tuyến tính của Wadler đã đưa nó vào thiết kế ngôn ngữ, và các nguyên tắc sở hữu và kiểm tra mượn sau đó đã đưa các ý tưởng cấu trúc con trở thành xu hướng chính trong lập trình hệ thống.

Debates

Tính biểu cảm so với khả năng sử dụng và tính quyết định

Các hệ thống có kiểu phụ thuộc và cấu trúc con có thể thể hiện các đảm bảo rất mạnh, nhưng chúng làm tăng gánh nặng cho các lập trình viên và có thể làm cho việc kiểm tra kiểu không thể quyết định hoặc khó khăn, thúc đẩy cuộc tranh luận về mức độ sức mạnh đáng giá chi phí.

Key figures

• Per Martin-Löf
• Jean-Yves Girard
• Philip Wadler
• Robert Harper

Seminal works

• martinlof1984
• girard1987
• wadler1990
• harper2016

Frequently asked questions

Kiểu phụ thuộc là gì?

Kiểu phụ thuộc là một kiểu mà định nghĩa của nó phụ thuộc vào một giá trị, chẳng hạn như kiểu của các vectơ có độ dài cụ thể, cho phép hệ thống kiểu thực thi các bất biến phong phú mà các kiểu thông thường không thể thể hiện.

Các kiểu tuyến tính đảm bảo điều gì?

Các kiểu tuyến tính yêu cầu mỗi giá trị được sử dụng chính xác một lần, điều này cho phép trình biên dịch an toàn cho phép cập nhật tại chỗ, quản lý tài nguyên và ngăn ngừa các lỗi liên quan đến bí danh mà không cần thu gom rác trong thời gian chạy.