<p>Java's type system is <a href="https://arxiv.org/abs/1605.05274" rel="nofollow noreferrer">Turing complete</a>. For whatever reason, I was under the impression that Kotlin's type system (for concreteness, let's say the latest version of the language -- <code>1.5.30</code>) was <em>not</em> Turing complete.</p>
<p>I'm not sure exactly where I got this impression, but this leads to the question: Is Kotlin's type system Turing complete? Specifically, is it Turing complete by the same mechanism used in the paper linked above?</p>
<p>Towards the end of this paper, the author says:</p>
<blockquote>
<p>Does the reduction from Section 5 apply to other languages like
C] and Scala? No. Both of them adopted the recursive–expansive
restriction of (Viroli 2000), as recommended by (Kennedy and
Pierce 2007). Roughly, this restriction is a syntactic check that
succeeds if and only if our Turing tapes are bounded.</p>
</blockquote>
<p>I could not find the referenced paper outside of a pay-wall, so I cannot say exactly what this restriction is, but it leads to the question: Does Kotlin have this restriction, thus not making Kotlin's type system Turing complete (by the same mechanism as Java)?</p>

CC BY-SA 4.0
2021-09-24T07:14:13.983Z
No, it's not like java: the specifications of the language (https://kotlinlang.org/spec/introduction.html) say that the parametric polymorphism is bounded.
Marzio De Biasi
CC BY-SA 4.0
2021-09-24T11:58:06.020Z
@Marzio De Biasi Does that not just mean that generic parameters can be bound by subtype constraints? That's the impression I get here -- and Java has that as well. https://en.m.wikipedia.org/wiki/Bounded_quantification#:~:text=In%20type%20theory%2C%20bounded%20quantification,of%20parametric%20polymorphism%20with%20subtyping.
Nathan BeDell
CC BY-SA 4.0
2021-09-24T11:59:00.067Z
In fact, Java is listed as an example.
Nathan BeDell
<type-systems><genetic-programming>
Is Kotlin's type system Turing complete?
Nathan BeDell
# Is Kotlin's type system Turing complete?

(Asked by: username_0 on 2021-09-24)

Java's type system is [Turing complete](https://arxiv.org/abs/1605.05274). For whatever reason, I was under the impression that Kotlin's type system (for concreteness, let's say the latest version of the language -- `1.5.30`) was *not* Turing complete.

I'm not sure exactly where I got this impression, but this leads to the question: Is Kotlin's type system Turing complete? Specifically, is it Turing complete by the same mechanism used in the paper linked above?

Towards the end of this paper, the author says:

> Does the reduction from Section 5 apply to other languages like
> C] and Scala? No. Both of them adopted the recursive–expansive
> restriction of (Viroli 2000), as recommended by (Kennedy and
> Pierce 2007). Roughly, this restriction is a syntactic check that
> succeeds if and only if our Turing tapes are bounded.

I could not find the referenced paper outside of a pay-wall, so I cannot say exactly what this restriction is, but it leads to the question: Does Kotlin have this restriction, thus not making Kotlin's type system Turing complete (by the same mechanism as Java)?

**Tags:** type-systems, genetic-programming

> **Comments:**
> **username_1**: No, it's not like java: the specifications of the language (https://kotlinlang.org/spec/introduction.html) say that the parametric polymorphism is bounded.  
> **username_0**: @username_1 Does that not just mean that generic parameters can be bound by subtype constraints? That's the impression I get here -- and Java has that as well. https://en.m.wikipedia.org/wiki/Bounded_quantification#:~:text=In%20type%20theory%2C%20bounded%20quantification,of%20parametric%20polymorphism%20with%20subtyping.  
> **username_0**: In fact, Java is listed as an example.  

---

## 0 answers

