Hệ thống kiểu Hindley–Milner

Hệ thống kiểu Hindley–Milner (HM) là một hệ thống kiểu cổ điển cho phép tính lambda với đa hình tham số (parametric polymorphism). Nó còn được gọi là Damas–Milner hay Damas–Hindley–Milner. Nó được mô tả lần đầu tiên bởi J. Roger Hindley^[1] và sau đó được khám phá lại bởi Robin Milner.^[2] Luis Damas đã đóng góp một phân tích và bằng chứng chính thức chặt chẽ trong luận án tiến sĩ của mình.^[3]^[4]

Trong số các đặc tính đáng chú ý hơn cả của HM là tính đầy đủ và khả năng suy luận ra kiểu tổng quát nhất của một chương trình nhất định mà không cần chú thích kiểu (type annotation) hay gợi ý khác do lập trình viên cung cấp. Giải thuật W là một phương pháp suy luận kiểu (type inference) hiệu quả, thực hiện trong (gần như) thời gian tuyến tính mà vẫn bảo đảm kích thước mã nguồn, khiến nó rất hữu ích trong thực tế để suy luận kiểu của chương trình lớn.^{[note 1]} HM được sử dụng nhiều cho ngôn ngữ hàm. Nó được hiện thực lần đầu như là một phần của hệ thống kiểu trong ngôn ngữ lập trình ML. Kể từ đó, HM đã được mở rộng theo nhiều cách, đáng chú ý nhất là với các ràng buộc kiểu lớp (type class constraint) như trong Haskell.

Introduction

Ghi chú

^ Hindley–Milner is DEXPTIME-complete. Non-linear behaviour does manifest itself, yet only on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community. When the depth of nested let-bindings is bounded—which is the case in realistic programs—Hindley–Milner type inference becomes polynomial.

Tham khảo

^ Hindley, J. Roger (1969). “The Principal Type-Scheme of an Object in Combinatory Logic”. Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.
^ Milner, Robin (1978). “A Theory of Type Polymorphism in Programming”. Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4.
^ Damas, Luis (1985). Type Assignment in Programming Languages (Luận văn). University of Edinburgh (CST-33-85).
^ Damas, Luis; Milner, Robin (1982). Principal type-schemes for functional programs (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. tr. 207–212. Bản gốc (PDF) lưu trữ ngày 22 tháng 3 năm 2022. Truy cập ngày 27 tháng 6 năm 2019.

Mairson, Harry G. (1990). Deciding ML typability is complete for deterministic exponential time. Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL '90. ACM. tr. 382–401. doi:10.1145/96709.96748. ISBN 978-0-89791-343-0.
Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (1990). ML typability is dexptime-complete. Lecture Notes in Computer Science. CAAP '90. 431. tr. 206–220. doi:10.1007/3-540-52590-4_50. ISBN 978-3-540-52590-5.

Liên kết ngoài

[5] Hindley–Milner is DEXPTIME-complete. Non-linear behaviour does manifest itself, yet only on pathological inputs. Thus the complexity theoretic proofs by Mairson (1990) and Kfoury, Tiuryn & Urzyczyn (1990) came as a surprise to the research community. When the depth of nested let-bindings is bounded—which is the case in realistic programs—Hindley–Milner type inference becomes polynomial.

[1] Hindley, J. Roger (1969). “The Principal Type-Scheme of an Object in Combinatory Logic”. Transactions of the American Mathematical Society. 146: 29–60. doi:10.2307/1995158. JSTOR 1995158.

[Milner-2] Milner, Robin (1978). “A Theory of Type Polymorphism in Programming”. Journal of Computer and System Sciences. 17 (3): 348–374. CiteSeerX 10.1.1.67.5276. doi:10.1016/0022-0000(78)90014-4.

[3] Damas, Luis (1985). Type Assignment in Programming Languages (Luận văn). University of Edinburgh (CST-33-85).

[Damas-4] Damas, Luis; Milner, Robin (1982). Principal type-schemes for functional programs (PDF). 9th Symposium on Principles of programming languages (POPL'82). ACM. tr. 207–212. Bản gốc (PDF) lưu trữ ngày 22 tháng 3 năm 2022. Truy cập ngày 27 tháng 6 năm 2019.

[1]

[2]

[3]

[4]

[note 1]