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

71–80 of 91 posts

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

#71

Post by otabdeveloper4 »

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…

"Turing completeness" is extremely orthogonal to complexity.

Being "Turing complete" only means that your thing supports unlimited recursion; or, in other words, that whatever objects it encodes can be arbitrarily large.

See: https://en.wikipedia.org/wiki/Rule_110

P.S. This also means that, technically speaking, the computers we use aren't Turing complete because they have RAM and storage limits.

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

#72

Post by pornel »

lenkite wrote: post #36
throwaway894345 wrote: post #20

Earlier quoted context omitted.

I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find…

I personally found Go far more unproductive than Python - doing if err!=nil a zillion times and writing the nth for loop..it made me cry worse than cutting fresh onions. Python is not Perfect (bad general-purpose performance), but IMHO honestly a more productive language than Go. And Python has type hinting nowadays which is sweet when you want it. Type hinting is good for self-documenting stable code.

Go's err != nil has nothing to do with types though. It's just its own quirky convention.

Python could similarly declare that exceptions are only for dead-end panics, and all error handling should be done by returning 2-element tuples.

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

#73

Post by simias »

amluto wrote: post #14
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 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.

I think an even better example would be the "entry" keyword which would add multiple entry points to C functions[1]. We dodged a bullet here.

[1] https://stackoverflow.com/questions/254395/whatever-happened...

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

#74

Post by cphoover »

Gibbon1 wrote: post #58
whatshisface wrote: post #30

Earlier quoted context omitted.

What kind of types are you dealing with that makes them so hard to keep track of? Are you talking about strings and integers, or a really really complicated objects and functions thing with functions of functions of functions and that kind of thing?

Today I was refactoring a codebase I maintain. In one domain the program thinks of time in 1/256ths second ticks. And in another it thinks in terms of 1/32768ths of a second. Elsewhere it thinks in terms of ms. Having them all represented as an int is often confusing. For me that wrote the code. God help anyone else.

If there is a practical reason you aren't using a uniform format for time I would consider this a case where compile-time type validation make sense... but for most applications I work on I would argue this is not a concern.

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

#75

Post by dragontamer »

nestorD wrote: post #62
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]:…

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

If you know how to reach Turing completeness in those systems, you wouldn't call any of those "simple".

MtG for instance is considered one of the more complicated card games.

Pokemon Yellow's turing completeness proof involved arbitrary code execution by swapping memory locations around.

Peano axioms / Arithmetic underlies an entire theory of abstract mathematics.

---------------

EDIT: I think decidable is an important attribute of systems that are weaker than Turing Complete. There are still very powerful decidable equations (ex: 3SAT, most famously), which has an answer (either satisfiable, or unsatisfiable), but may need O(2^n) time (or longer) to calculate the result.

Turing Complete is only semi-decidable: if something halts it will halt in finite time. If something won't halt, you'll never know.

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

#76

Post by ObscureScience »

Kranar wrote: post #47
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…

You are correct, furthermore having a Turing complete system does not forbid one from choosing an expressive subset of the system that isn't Turing complete.

That's true, but I you really don't need the computational power, you might want to have that well defined limited semantic to either not accidentally shoot you in foot (the least important), or being able to statically verify it's properties in finite time.

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

#77

Post by cphoover »

pharke wrote: post #69
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 b…

I agree that where strict typing exists it should have the ability to get out of the way as is with languages that support type inference.

Personally I've never found type mismatches to be particularly a large problem, as you can still support input validation where needed, generally at some application message boundary like an http request/response, and the type of bugs caused by mismatched types are easy to diagnose and test for.

The class of bugs that to me are much more difficult to fix unlike type mismatches are not immediately visible or do not give descriptive messages for example race conditions, memory leaks, logical errors, etc...

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

#78

Post by throwaway894345 »

whatshisface wrote: post #30
throwaway894345 wrote: post #20

Earlier quoted context omitted.

I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find…

What kind of types are you dealing with that makes them so hard to keep track of? Are you talking about strings and integers, or a really really complicated objects and functions thing with functions of functions of functions and that kind of thing?

Well, sometimes you get really crazy types, like large implicit unions where many of the variants are dictionaries with specific structures or a class that has an attribute created dynamically. Or when some API says it wants a “file-like object”, does it mean “object with read() method”? Or read() + close()? What about seek()? Etc. But the spirit of my comment was about making sure that the types align—that I’m correctly passing the right kind of data into some function for every function. It’s easy to make type errors, and I know it’s not just me because type errors of various kinds were the number one kind of error in our production logs at our Python shop even though we had high unit test coverage.

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

#79

Post by throwaway894345 »

lenkite wrote: post #36
throwaway894345 wrote: post #20

Earlier quoted context omitted.

I have the inverse experience. I find it far more cognitively burdensome to have to keep track of the types without annotations or assistance from a type checker. Getting rid of the type checker doesn’t make the type go away, it just means the full burden of managing them correctly falls on the programs. And it’s not for lack of effort—I’ve been using Python among other languages for 15 years, but I would still find…

I personally found Go far more unproductive than Python - doing if err!=nil a zillion times and writing the nth for loop..it made me cry worse than cutting fresh onions. Python is not Perfect (bad general-purpose performance), but IMHO honestly a more productive language than Go. And Python has type hinting nowadays which is sweet when you want it. Type hinting is good for self-documenting stable code.

I never minded the boilerplate. Pushing buttons on a keyboard never slowed me down very much, especially compared to finding and fixing bugs or even writing gratuitous test cases to guard against type errors. If I could only press a few buttons per minute or if I could write many test cases per minute I might feel differently.

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

#80

Post by tomsmeding »

twic wrote: post #70
jetrink wrote: post #26

Earlier quoted context omitted.

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, s…

> a very disciplined approach to safety [...] they still share the same code, which is also mutable, so they can communicate through that

Disciplined, maybe; usable/sane, certainly not. Then again, it's INTERCAL, so that was most certainly the intention.

Post reply on HN