system-f

In a word, general recursion. Haskell allows for arbitrary recursion while System F has no form of recursion. The lack of infinite types means fix isn’t expressible as a closed term. There is no primitive notion of names and recursion. In fact, pure System F has no notion of any such thing as definitions! So … Read more