How did Haskell add Turing-completeness to System F?

Question

I've been reading up on various type systems and lambda calculi, and i see that all of the typed lambda calculi in the lambda cube are strongly normalizing rather than Turing equivalent. This includes System F, the simply typed lambda calculus plus polymorphism.

This leads me to the following questions, for which I've been unable to find any comprehensible answer:

• How does the formalism of (e.g.) Haskell differ from the calculus on which it is ostensibly based?
• What language features in Haskell don't fall within System F formalism?
• What's the minimum change necessary to allow Turing complete computation?

Thank you so much to whomever helps me understand this.

Answer 1

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 in Haskell this single definition is what adds turing completeness

fix :: (a -> a) -> a
fix f = let x = f x in x

Really this function is indicative of a more general idea, by having fully recursive bindings, we get turing completeness. Notice that this applies to types, not just values.

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

With infinite types we can write the Y combinator (modulo some unfolding) and through it general recursion!

In pure System F, we often have some informal notion of definitions, but these are simply shorthands that are to be mentally inlined fully. This isn't possible in Haskell as this would create infinite terms.

The kernel of Haskell terms without any notion of let, where or = is strongly normalizing, since we don't have infinite types. Even this core term calculus isn't really System F. System F has "big lambdas" or type abstraction. The full term for id in System F is

id := /\ A -> \(x : A) -> x

This is because type inference for System F is undecidable! We explicitly notate wherever and whenever we expect polymorphism. In Haskell such a property would be annoying, so we limit the power of Haskell. In particular, we never infer a polymorphic type for a Haskell lambda argument without annotation (terms and conditions may apply). This is why in ML and Haskell

let x = exp in foo

isn't the same as

(\x -> foo) exp

even when exp isn't recursive! This is the crux of HM type inference and algorithm W, called "let generalization".