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?

In addition, since hindley-milner is:

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?


2 Answers 2


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.

  • 1
    $\begingroup$ Wow, this is an amazing answer and answers everything perfectly. Thank you! $\endgroup$
    – Mike H-R
    Commented Feb 17, 2015 at 16:06
  • $\begingroup$ "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 $\endgroup$ Commented Jul 20, 2017 at 21:30
  • 1
    $\begingroup$ @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/… $\endgroup$
    – cody
    Commented Jul 21, 2017 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.

  • $\begingroup$ 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. $\endgroup$
    – Mike H-R
    Commented Feb 18, 2015 at 10:52
  • $\begingroup$ 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. $\endgroup$
    – Mike H-R
    Commented Feb 18, 2015 at 10:54
  • 1
    $\begingroup$ @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. $\endgroup$ Commented Feb 18, 2015 at 20:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.