<p>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 <a href="https://mail.haskell.org/pipermail/haskell/2006-August/018355.html">here</a>. This is not the only reason for Haskell's power, Cody has mentioned some others.</p>

CC BY-SA 3.0
2015-02-18T10:52:48.747Z
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
CC BY-SA 3.0
2015-02-18T10:54:29.347Z
N.B. If anyone is interested in the power of the haskell type system, I'd recommend [Edward Kmett's video on hask](https://www.youtube.com/watch?v=Klwkt9oJwg0), which delves (deep) into category theory using the haskell type system.
Mike H-R
CC BY-SA 3.0
2015-02-18T20:57:05.243Z
@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](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system) is worth reading.
Martin Berger
CC BY-SA 3.0
2015-02-18T01:02:25.493Z
2015-02-18T01:02:25.493Z
Martin Berger
<p>System <span class="math-container">$F$</span> is quite expressive. As proved by Girard <a href="http://www.sciencedirect.com/science/article/pii/S0049237X08708437" rel="nofollow noreferrer">here</a>, the functions of type <span class="math-container">$\mathbb{N}\rightarrow\mathbb{N}$</span> (where <span class="math-container">$\mathbb{N}$</span> is defined to be <span class="math-container">$\forall X.\ X\rightarrow (X\rightarrow X)\rightarrow X$</span>) are exactly the definable functions (<span class="math-container">$\mathbb{N}\rightarrow\mathbb{N}$</span>) in second order Heyting Arithmetic <span class="math-container">$\mathrm{HA}_2$</span>. Note that this is the same as the functions definable in <a href="http://en.wikipedia.org/wiki/Second-order_arithmetic" rel="nofollow noreferrer">second order Peano Arithmetic</a>.</p>
<p>You'll probably want to check <a href="http://www.paultaylor.eu/stable/prot.pdf" rel="nofollow noreferrer">Proofs and Types</a> as a more readable reference. Note that this means that <em>a lot</em> of programs can be written in system F, from the Ackermann function to interpreters for Gödel's system <span class="math-container">$T$</span>. As for any total programing language (with some mild conditions) system <span class="math-container">$F$</span> cannot implement a <em>self interpreter</em>, i.e. a function <span class="math-container">$\mathrm{eval}:\mathbb{N}\rightarrow\mathbb{N}$</span> which takes as input a (reasonable) code for a term <span class="math-container">$t$</span> of system <span class="math-container">$F$</span> and returns a (code for a) normal form for <span class="math-container">$t$</span>. The proof involves a variant of the diagonalizing trick used for undecidability of the halting problem. Andrej explains it beautifully <a href="https://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret">here</a>.</p>
<p>To answer your other questions: The <span class="math-container">$\lambda$</span>-calculus underlying Hindley-Milner (HM) languages is also not Turing complete. In fact it is significantly weaker than system <span class="math-container">$F$</span>, closer in expressiveness to the <em>simply typed</em> <span class="math-container">$\lambda$</span>-calculus.</p>
<p>Haskell is indeed Turing complete. The most distinctive feature enabling this (though there are others) is the presence of <strong><a href="http://en.wikipedia.org/wiki/Recursion_%28computer_science%29#Recursive_programs" rel="nofollow noreferrer">unrestricted recursion</a></strong>: the definition of any program (function) can refer to the program itself. This is similar to the addition of a <span class="math-container">$Y$</span> combinator, such as is done in the definition of <a href="http://en.wikipedia.org/wiki/Programming_Computable_Functions" rel="nofollow noreferrer">PCF</a> which is simply-typed but retains Turing-completeness with the <span class="math-container">$Y$</span> combinator.</p>
<p>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.</p>

CC BY-SA 3.0
2015-02-17T16:06:53.137Z
Wow, this is an amazing answer and answers everything perfectly. Thank you!
Mike H-R
CC BY-SA 3.0
2017-07-20T21:30:06.070Z
"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](http://compilers.cs.ucla.edu/popl16/popl16-full.pdf)
Joey Eremondi
CC BY-SA 3.0
2017-07-21T13:36:36.267Z
@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: http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/
cody
CC BY-SA 4.0
2015-02-17T15:59:06.220Z
2024-11-01T18:53:58.903Z
2024-11-01T18:53:58.903Z
cody
<p>In <a href="http://en.wikipedia.org/wiki/Turing_completeness">this wikipedia article on Turing Completeness</a> it states that:</p>

<blockquote>
  <p>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.</p>
</blockquote>

<p>What is an example of a total computable function that is uncomputable by <a href="http://en.wikipedia.org/wiki/System_F">system F</a>?</p>

<p>In addition, since hindley-milner is:</p>

<blockquote>
  <p>A restriction of System F</p>
</blockquote>

<p>because of the fact that:</p>

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

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

<p>If this is true, since <a href="https://www.haskell.org/">haskell</a> 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?</p>

CC BY-SA 3.0
2015-02-17T15:39:28.300Z
Similar to: [http://cstheory.stackexchange.com/questions/3405/an-example-of-a-totally-computable-function-that-is-not-definable-in-system-t](http://cstheory.stackexchange.com/questions/3405/an-example-of-a-totally-computable-function-that-is-not-definable-in-system-t?rq=1)
cody
CC BY-SA 3.0
2015-02-17T15:43:47.520Z
Example of feature that makes Haskell turing complete is native code interface.
Trismegistos
CC BY-SA 3.0
2015-02-17T15:44:57.710Z
@cody thanks for your comment. I'm not familiar with system T. Am I right in assuming it is [the system T mentioned here](http://en.wikipedia.org/wiki/Dialectica_interpretation)? how does system T compare and contrast to system F?
Mike H-R
CC BY-SA 3.0
2015-02-17T15:46:23.483Z
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](http://stackoverflow.com/questions/25255413/how-did-haskell-add-turing-completeness-to-system-f)
Mike H-R
CC BY-SA 3.0
2015-02-17T16:00:33.557Z
Ah, my answer becomes somewhat redundant now.
cody
CC BY-SA 3.0
2015-02-18T20:52:56.527Z
I think @Trismegistos raises an interesting philosophical issue: what exactly is Haskell, where are its boundaries?
Martin Berger
CC BY-SA 3.0
2015-02-19T08:47:08.117Z
@MartinBerger Yes, I though about it too. You can say that native code is not a Haskell. But if not native code you would not be able to write any application because application must communicate with hardware.
Trismegistos
<computability><turing-machines><haskell>
What functions can System F not compute?
Mike H-R
# What functions can System F not compute?

(Asked by: username_0 on 2015-02-17)

In [this wikipedia article on Turing Completeness](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/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](https://www.haskell.org/) 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?

**Tags:** computability, turing-machines, haskell

> **Comments:**
> **username_1**: Similar to: [http://cstheory.stackexchange.com/questions/3405/an-example-of-a-totally-computable-function-that-is-not-definable-in-system-t](http://cstheory.stackexchange.com/questions/3405/an-example-of-a-totally-computable-function-that-is-not-definable-in-system-t?rq=1)  
> **username_2**: Example of feature that makes Haskell turing complete is native code interface.  
> **username_0**: @username_1 thanks for your comment. I'm not familiar with system T. Am I right in assuming it is [the system T mentioned here](http://en.wikipedia.org/wiki/Dialectica_interpretation)? how does system T compare and contrast to system F?  
> **username_0**: 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](http://stackoverflow.com/questions/25255413/how-did-haskell-add-turing-completeness-to-system-f)  
> **username_1**: Ah, my answer becomes somewhat redundant now.  
> **username_3**: I think @username_2 raises an interesting philosophical issue: what exactly is Haskell, where are its boundaries?  
> **username_2**: @MartinBerger Yes, I though about it too. You can say that native code is not a Haskell. But if not native code you would not be able to write any application because application must communicate with hardware.  

---

## 2 answers

### Answer by username_1 on 2015-02-17. Score: 52 | Accepted answer

System $F$ is quite expressive. As proved by Girard [here](http://www.sciencedirect.com/science/article/pii/S0049237X08708437), 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](http://en.wikipedia.org/wiki/Second-order_arithmetic).

You'll probably want to check [Proofs and Types](http://www.paultaylor.eu/stable/prot.pdf) 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 (reasonable) 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](https://cstheory.stackexchange.com/questions/24986/a-total-language-that-only-a-turing-complete-language-can-interpret).

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](http://en.wikipedia.org/wiki/Recursion_%28computer_science%29#Recursive_programs)**: 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](http://en.wikipedia.org/wiki/Programming_Computable_Functions) 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.

> **Comments:**
> **username_0**: Wow, this is an amazing answer and answers everything perfectly. Thank you!  
> **username_4**: "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](http://compilers.cs.ucla.edu/popl16/popl16-full.pdf)  
> **username_1**: @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: http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/  

---

### Answer by username_3 on 2015-02-18. Score: 11

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](https://mail.haskell.org/pipermail/haskell/2006-August/018355.html). This is not the only reason for Haskell's power, Cody has mentioned some others.

> **Comments:**
> **username_0**: 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.  
> **username_0**: N.B. If anyone is interested in the power of the haskell type system, I'd recommend [Edward Kmett's video on hask](https://www.youtube.com/watch?v=Klwkt9oJwg0), which delves (deep) into category theory using the haskell type system.  
> **username_3**: @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](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system) is worth reading.  

---

