# What functions can System F not compute?

In this wikipedia article on Turing Completeness it states that:

The untyped lambda calculus is Turing complete, but many typed lambda calculi, including System F, are not. The value of typed systems is based in their ability to represent most typical computer programs while detecting more errors.

What is an example of a total computable function that is uncomputable by system F?

A restriction of System F

because of the fact that:

type checking is undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.

Does this mean that the lambda calculus underlying hindley-milner type systems is not turing complete as well?

If this is true, since haskell is clearly turing complete and we know that it's basis is the lambda calculus and the hindley-milner type system, what features that are not present in the lambda calculus are added in order to make haskell turing complete?

• – cody Feb 17 '15 at 15:39
• Example of feature that makes Haskell turing complete is native code interface. – Trismegistos Feb 17 '15 at 15:43
• @cody thanks for your comment. I'm not familiar with system T. Am I right in assuming it is the system T mentioned here? how does system T compare and contrast to system F? – Mike H-R Feb 17 '15 at 15:44
• NOTE, on googling for system T vs. system F I found something that answers my final subquestion that is rephrased here as: How did haskell add Turing-completeness to System F – Mike H-R Feb 17 '15 at 15:46
• I think @Trismegistos raises an interesting philosophical issue: what exactly is Haskell, where are its boundaries? – Martin Berger Feb 18 '15 at 20:52

System $F$ is quite expressive. As proved by Girard here, the functions of type $\mathbb{N}\rightarrow\mathbb{N}$ (where $\mathbb{N}$ is defined to be $\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$) are exactly the definable functions ($\mathbb{N}\rightarrow\mathbb{N}$) in second order Heyting Arithmetic $\mathrm{HA}_2$. Note that this is the same as the functions definable in second order Peano Arithmetic.

You'll probably want to check Proofs and Types as a more readable reference. Note that this means that a lot of programs can be written in system F, from the Ackermann function to interpreters for Gödel's system $T$. As for any total programing language (with some mild conditions) system $F$ cannot implement a self interpreter, i.e. a function $\mathrm{eval}:\mathbb{N}\rightarrow\mathbb{N}$ which takes as input a code for a term $t$ of system $F$ and returns a (code for a) normal form for $t$. The proof involves a variant of the diagonalizing trick used for undecidability of the halting problem. Andrej explains it beautifully here.

To answer your other questions: The $\lambda$-calculus underlying Hindley-Milner (HM) languages is also not Turing complete. In fact it is significantly weaker than system $F$, closer in expressiveness to the simply typed $\lambda$-calculus.

Haskell is indeed Turing complete. The most distinctive feature enabling this (though there are others) is the presence of unrestricted recursion: the definition of any program (function) can refer to the program itself. This is similar to the addition of a $Y$ combinator, such as is done in the definition of PCF which is simply-typed but retains Turing-completeness with the $Y$ combinator.

Note there are other features which make Haskell Turing complete, but they are not usually taken to be part of the core language, e.g. references to functions, unrestricted datatypes, etc.

• Wow, this is an amazing answer and answers everything perfectly. Thank you! – Mike H-R Feb 17 '15 at 16:06
• "As for any total programing language..." This is not quite correct. There are some self-interpreters for total languages that work by excluding non-terminating programs as ill-typed, by my understanding. See this paper – jmite Jul 20 '17 at 21:30
• @jmite as stated, my claim is correct. That paper is mentioned in the linked discussion, and Andrej has some follow up remarks on his blog: math.andrej.com/2016/01/04/… – cody Jul 21 '17 at 13:36

It is somewhat misleading to say that Haskell's typing system is "the hinley-milner type system". Haskell's types are much more powerful, including, among others, higher-kinded types. Indeed the typing system is so powerful that you can embed Turing-complete programming languages in the typing system, see here. This is not the only reason for Haskell's power, Cody has mentioned some others.

• Thanks. my main exposure to hindley-milner has been through haskell so I guess I may have assumed that higher-kinded types were a part of it. Is hindley-milner simply referring to the type inference (so most likely algorithm W)? or is it something more? I understand that there is the mathematical basis of it in the lambda calculus, I'm just trying to understand where the logical boundaries between the powerful type system of haskell and what a minimal implementation of a "hindley-milner type system" would be. – Mike H-R Feb 18 '15 at 10:52
• N.B. If anyone is interested in the power of the haskell type system, I'd recommend Edward Kmett's video on hask, which delves (deep) into category theory using the haskell type system. – Mike H-R Feb 18 '15 at 10:54
• @MikeH-R Usually we mean that Hindley–Milner is a typing system or, more precisely, a typed $\lambda$-calculus, whereas the $W$ algorithm is a type-inference algorithm for the Hindley–Milner system. What's remarkable about the Hindley-Milner system is that it combines parametric polymorphism with ability to infer the most general type of any given program without type annotations. The Wikipedia article is worth reading. – Martin Berger Feb 18 '15 at 20:57