Rust's type system is Turing-complete (2017)

#1

Post by lukastyrychtr » Sat, Mar 13, 2021, 9:37 AM UTC

Rust's type system is Turing-complete (2017)
sdleffler.github.io

Re: Rust's type system is Turing-complete (2017)

#2

Post by dang » Mon, Mar 15, 2021, 11:01 PM UTC

Discussed at the time:

Rust's Type System Is Turing-Complete: Type-Level Programming in Rust - https://news.ycombinator.com/item?id=13843288 - March 2017 (117 comments)

Re: Rust's type system is Turing-complete (2017)

#3

Post by bodhiandphysics » Tue, Mar 16, 2021, 1:29 AM UTC

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

Re: Rust's type system is Turing-complete (2017)

#4

Post by golergka » Tue, Mar 16, 2021, 1:36 AM UTC

bodhiandphysics wrote: post #3

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

Out of curiosity — has there ever been a type system that was discovered to be Turing-complete and then actually have caused a bug for a real application that was caused by the fact that it allowed an invalid program through?

I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.

Re: Rust's type system is Turing-complete (2017)

#5

Post by drdeca » Tue, Mar 16, 2021, 1:37 AM UTC

bodhiandphysics wrote: post #3

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

Can you elaborate on this? I'm not sure what you mean by valid and invalid programs. By "valid", do you mean ones which are well typed under the type system? But then, what does it mean for it to be well typed under the type system, other than that the type system, err, allows it?

edit: by which I mean, the theoretically defined type system, not the actual program implementing it.

Re: Rust's type system is Turing-complete (2017)

#6

Post by lmm » Tue, Mar 16, 2021, 1:37 AM UTC

To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, make sure that you're getting a return on that complexity by ensuring that your type system has the features that you need to do useful things.

Re: Rust's type system is Turing-complete (2017)

#7

Post by amelius » Tue, Mar 16, 2021, 1:49 AM UTC

bodhiandphysics wrote: post #3

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

You mean in case the type-inference doesn't halt?

Aren't such programs not very interesting by definition?

And why would you call them "valid" programs?

Re: Rust's type system is Turing-complete (2017)

#8

Post by ben-schaaf » Tue, Mar 16, 2021, 1:52 AM UTC

bodhiandphysics wrote: post #3

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

> In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.

Re: Rust's type system is Turing-complete (2017)

#9

Post by slavapestov » Tue, Mar 16, 2021, 2:06 AM UTC

lmm wrote: post #6

To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, m…

I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here. Higher-kinded types, dependent types and kind polymorphism don't actually mean your type system becomes undecidable. They do vastly complicate the implementation in other ways, though.

Re: Rust's type system is Turing-complete (2017)

#10

Post by DaiPlusPlus » Tue, Mar 16, 2021, 2:07 AM UTC

bodhiandphysics wrote: post #3

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

> If a type system is Turing complete, than it either has to be inconsistent or incomplete.

How is Turing-completeness related to soundness? I am behind on CS theory, but what little I know about category-theory tells me this isn’t the case.