How did Haskell add Turing-completeness to 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 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".