Tôi nhớ đọc ở đâu đó rằng Hindley Milner là một hạn chế đối với hệ thống-f. Nếu đúng như vậy, có thể ai đó vui lòng cung cấp cho tôi một số thuật ngữ có thể được gõ vào hệ thống-f nhưng không phải trong HM.Một số loại và/hoặc thuật ngữ nào trong hệ thống-f không thể được thể hiện trong Hindley Milner
Bất kỳ điều gì liên quan đến tính đa hình cao hơn (nghĩa là "hạng nhất"). Ví dụ:
lambda f : (forall A. A -> A). (f Int 1, f String "hello")
Chức năng này sẽ có các loại (forall A. A -> A) -> Int * String, mà không thể diễn tả được trong HM, nơi mà tất cả các chương trình kiểu đa hình phải thuộc diện "prenex" hình thức (tức là lượng hóa chỉ có thể xảy ra ở bên ngoài, không bao giờ lồng).
Không chắc chắn ý của bạn là gì, biểu thức đó không phải là chức năng. Các định nghĩa (ràng buộc thông qua let) có thể được đa hình với HM, nhưng các tham số chức năng có thể không. –