सिस्टम-एफ में कुछ प्रकार और/या शर्तें क्या हैं जिन्हें हिंडले मिलनर

Question

में व्यक्त नहीं किया जा सकता है मुझे याद है कि हिंडली मिलनर सिस्टम-एफ पर प्रतिबंध था। यदि ऐसा है, तो कृपया कोई मुझे कुछ शर्तों के साथ प्रदान कर सकता है जिसे सिस्टम-एफ में टाइप किया जा सकता है लेकिन एचएम में नहीं।

Answer 1

उच्च रैंकिंग (यानी "प्रथम श्रेणी") पॉलिमॉर्फिज्म शामिल कुछ भी शामिल है। उदाहरण के लिए:

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

इस समारोह प्रकार (forall A. A -> A) -> Int * String, जो एचएम, जहां सभी बहुरूपी प्रकार योजनाओं "prenex" रूप में होना चाहिए में व्यक्त नहीं है के लिए होता है (यानी परिमाणक केवल बाहर की दुनिया में हो सकता है, कभी नहीं नेस्ट)।