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

41–50 of 91 posts

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

#41

Post by knome »

bodhiandphysics wrote: post #25
Kranar wrote: post #22

Earlier quoted context omitted.

Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article. But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.

Yes (changed the post)... my point is that the program is valid! Rusts type system can fail to stop on valid programs. I’m probably making a mess of all this though and should shut up before I confuse things more!

type systems often feel like a rudimentary typeless haskell or prolog layered as a templating system over the underlying code, particularly if the types are used in generating code for generic types in the underlying typed language.

for any reasonable program, you're not going to run into problems with the turing complete aspects of the type system. it's only when you start cleverly lifting logic into the type system to run in that typeless compile-time space that you'll feel punished by it.

if you want to check if a type adheres to some constraint and then choose between different things to do, and then do that recursively et cetera, sure, you'll blow the template expansion stack.

because you're not longer programming in the typed language, but in the typeless meta-language of its type system.

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

#42

Post by creata »

konjin wrote: post #24
okareaman wrote: post #19

Earlier quoted context omitted.

You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.

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

You also don't have the power to force anything, just the power to check if it's correct in a few of the infinitely many cases.

And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.

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

#43

Post by mannerheim »

viuphiet wrote: post #38
continuational wrote: post #33

Earlier quoted context omitted.

That makes it nearly impossible for the programmer to predict what will type check and what will not.

This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.

I believe Haskell's type system is only Turing complete with UndecidableInstances or other extensions. But these extensions are not uncommon.

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

#44

Post by creata »

ben-schaaf wrote: post #8
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.

The point isn't that there is an infinite loop of types that is rejected, the point is that there must be a finite loop of types that is rejected because it is indistinguishable from an infinite loop of types.

(I think the person you replied to is exaggerating the significance of this, though: it's obviously not a big deal in practice.)

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

#45

Post by [deleted] »

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

[deleted]

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

#46

Post by coolreader18 »

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

The comefrom wiki article led me to an april fool's for adding goto/comefrom to Python[0], and. Wow. It's really gross

[0] http://entrian.com/goto/

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

#47

Post by Kranar »

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.

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

#48

Post by lmm »

slavapestov wrote: post #9
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.

> A terminating type checker is much more valuable than a possibly non-terminating one.

My point is that your type checker is already possibly-non-terminating. That ship has sailed. So you might as well make it the best possibly-non-terminating typechecker that you can.

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

#49

Post by adwn »

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 don't have to think about abstractions as types I only need to think how to solve the problem in front of me.

There's a function in a popular Python scientific library (I can't recall the name of the library or the function, unfortunately), which takes a parameter n and returns a float if n=1, and a list of floats if n!=1. This behavior wasn't documented explicitly – I found out during testing – and is just annoying to deal with when the parameter n isn't a constant.

This wouldn't happen in a statically typed language, because 1) the function's signature would hint at this unexpected behavior, and 2) the designer of that function has to think about the assumptions they make and the guarantees they give, and not just "how to solve the problem in front" of them.

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

#50

Post by lmm »

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?

Strings and integers are rarely just strings and integers. For example, is this "integer" an order ID or a customer ID? Without a type system to tell them apart, mixing them up is a bug waiting to happen.
Post reply on HN