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
Liên kết ngoài
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
