Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

sdleffler.github.io

Post reply on HN
Print view View original

61–70 of 91 posts

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

#61

Post by atoav »

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 agree that piling on complexity forever is never a good idea. But to imply this is what happens in Rusts case is a claim that IMO requires citation.

Because being touring complete alone has been reached a while ago. Why even bother developing peogramming languages after that? Probably because just being touring complete alone doesn't necessarily enable you to comfortably and quickly create abstractions and structures that are easy to write, modify and compose to a bigger whole.

The claim that what Rust is doing with its type system isn't useful is one you need to show us examples for. Simply stating something unfavourable about some project out of gut feeling is bad form.

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

#62

Post by nestorD »

c3534l wrote: post #40

The article is fascinating and I love fun stuff like this, but the discussion is a bit off the rails. There are a lot of things that are accidentally Turing complete. Turing complete is not synonymous with complicated and unwieldy to use. I mean, okay, maybe if you are doing the stuff that the author is doing it is complicated and unwieldy - in fact to the point that you would never do it in the first place. But Turi…

To further push the point that many things are Turing complete and that it should not be seen as synonymous with complex, Gwern has a nice list of Surprisingly Turing complete things [0] that includes Peano Arithmetic, Pokemon Yellow and Magic the Gathering.

I personally find lists of programming language that made the conscious decision to not be Turing complete (such as Coq the theorem prover) more intriguing.

[0]: https://www.gwern.net/Turing-complete

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

#63

Post by Ar-Curunir »

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…

Just because something is possible doesn’t mean it’s easy or intuitive to use.

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

#64

Post by volta83 »

jcelerier wrote: post #59
dllthomas wrote: post #11

Earlier quoted context omitted.

Eh, I don't agree, despite being very sympathetic to type system sophistication. The fact that you can get Turing complete behavior in some part of a system with some encoding doesn't mean it's accessible enough that it's relevant when deciding how I am going to accomplish something or (typically) when deciphering what someone else has written.

But as soon as it's turing-complete someone will try to write whatever algorithm with it and you'll have to maintain it.

The type system is turing complete, and its implementation already supports this, since its required for correctness.

People using this feature does not incur any "extra" effort.

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

#65

Post by volta83 »

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!).

Lol no.

The only thing this means is that type checking a Rust program might never terminate.

Nothing more, nothing less.

It might take 10 seconds, it might take 10 days, it might take till the universe freezes.

In practice, the compiler - like pretty much every single compiler with a Turing complete type system - has a recursion limit, that rejects programs that accidentally take too long to type check, but users can increase this limit by adding a source annotation (that's suggested by the compiler).

This is completely orthogonal to whether the programs are valid or not.

If your program is invalid, the compiler will never accept it, no matter how much compute time you throw at it.

Type checking always terminates for valid Rust programs (by definition), so if you throw enough compute at any valid Rust program, the compiler will eventually accept it.

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

#66

Post by konjin »

feoren wrote: post #56
konjin wrote: post #24

Earlier quoted context omitted.

Yes and? I have the full power of the language to force type correctness instead of some janky meta language.

And if you're really good, you'll use that full power to develop a toolset of useful ways to verify that certain properties about your code hold! You'll see common errors and write infrastructure to help your unit tests ensure those errors aren't happening. You might even add annotations into your code as you write it to automatically write those unit tests for you. And you will have invented ... the Inner Type Syste…

Yes, a great thing to do for a dsl that you write in your real language. Not something that a real language should have.

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

#67

Post by pdpi »

jcelerier wrote: post #59
dllthomas wrote: post #11

Earlier quoted context omitted.

Eh, I don't agree, despite being very sympathetic to type system sophistication. The fact that you can get Turing complete behavior in some part of a system with some encoding doesn't mean it's accessible enough that it's relevant when deciding how I am going to accomplish something or (typically) when deciphering what someone else has written.

But as soon as it's turing-complete someone will try to write whatever algorithm with it and you'll have to maintain it.

And you can refuse to merge those changes and promptly kick the idiot who did that from your team. Or maybe, just maybe, it’s that one case where it actually makes sense.

Not all problems are technical. This is the sort of thing that can be solved with people skills.

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

#68

Post by yccs27 »

c3534l wrote: post #40

The article is fascinating and I love fun stuff like this, but the discussion is a bit off the rails. There are a lot of things that are accidentally Turing complete. Turing complete is not synonymous with complicated and unwieldy to use. I mean, okay, maybe if you are doing the stuff that the author is doing it is complicated and unwieldy - in fact to the point that you would never do it in the first place. But Turi…

Yes, there is a big difference between how complex something can theoretically be, and how complex the typical use case is.

There are two main drawbacks to accidental Turing-completeness:

- You can no longer statically analyze the system for properties like termination, because you can't solve the halting problem (at least not without extra bounds).

- Some people will try to abuse turing-completeness to solve their problem, leading to a jumbled mess. If this becomes an accepted way of using your system, it has basically failed.

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

#69

Post by pharke »

cphoover wrote: post #17

One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type…

I think most people, myself included, that dislike verbose type systems aren't opposed to type checking itself. We're just not overjoyed at learning and using a meta-programming language to do it. The argument tends to center around the friction it introduces to the development cycle. Those in favor of these languages often argue that you would need to spend the extra time verifying that the code is correct anyways but I don't think it equals out in the end, it certainly doesn't make things any faster. I'm sure that much more could be done to infer types or automate the process, I'm unsure of why this isn't done in the more popular languages. Maybe it's just a hangover from C++ and we're just repeating bad patterns when there is a better way? It's not like we haven't done that before.

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

#70

Post by twic »

jetrink wrote: post #26
amluto wrote: post #14

Earlier quoted context omitted.

I strongly disagree. Just because a feature doesn’t increase the underlying theoretical complexity doesn’t mean it’s a good idea. As a trivial example C plus “come from” is fundamentally the same language as regular C, and one can trivially translate it to remove come from. That doesn’t mean that adding come from to C would be a good idea.

For anyone confused like me. [1] Incidentally, Googling "C plus come from" only returns two relevant results, the parent comment and a manual for an esoteric programming language called C-INTERCAL that uses the COME FROM statement and compiles to C. [2] 1. https://en.wikipedia.org/wiki/COMEFROM 2. http://catb.org/~esr/intercal/ick.htm

COME FROM is also the foundation of concurrency in some versions of INTERCAL - if there are two COME FROM statements for the same origin, then when execution reaches that point, it forks.

Threaded INTERCAL actually has a very disciplined approach to safety. Each thread gets its own copy of all variables, so threads do not share any mutable data at all. However, they still share the same code, which is also mutable, so they can communicate through that.

Post reply on HN