ما هي بعض الأنواع و / أو المصطلحات في SYSTEM-F التي لا يمكن التعبير عنها في Milner Hindley

Question

أتذكر القراءة في مكان ما كان Hindley Milner قيدا على System-F.إذا كان هذا هو الحال، فيمكن أن يوفر لي شخص ما مع بعض المصطلحات التي يمكن كتابتها في System-f ولكن ليس في جلالة الملك.

Answer 1

Anything involving higher-ranked (i.e. "first-class") polymorphism. For example:

lambda f : (forall A. A -> A). (f Int 1, f String "hello")

This function would have the type (forall A. A -> A) -> Int * String, which is not expressible in HM, where all polymorphic type schemes must be in "prenex" form (i.e. the quantifier may only occur on the outside, never nested).