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

51–60 of 91 posts

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

#51

Post by [deleted] »

dllthomas wrote: post #35
slavapestov wrote: post #9

Earlier quoted context omitted.

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.

> I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. I don't think that's true at all, and I think there are two extreme examples that drive the point home: Consider on the one hand a language where typechecking is entirely terminating so long as you don't use one particular feature; however, that feature is also not very useful in practice (even notwithstanding the pote…

[deleted]

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

#52

Post by Dylan16807 »

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

COMEFROM is also known as aspect oriented programming.

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

#53

Post by dataflow »

continuational wrote: post #33
TheCoelacanth wrote: post #29

Earlier quoted context omitted.

It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.

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

So what? We can't predict how much RAM the user's machine has either, but that doesn't mean we can't write useful programs.

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

#54

Post by the_gipsy »

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?

Usually it's just many small uncomplicated structs.

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

#55

Post by feoren »

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?

Honestly I find this question crazy. Have you never made an asynchronous data call returning an array of objects with properties that are complex types? You're already at Promise>. What if you have to keep track of multiple of those calls at once in a data structure? Have you never used map or filter operations on streams of data? Do you really think functions returning functions is "really really complicated"? It makes me wonder whether you've ever actually worked on a moderately complex system.

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

#56

Post by feoren »

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.

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 System!

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

#57

Post by opnitro »

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.

On this notion, a very good talk "On the expressive power of programming languages"[1][2] which attempts to provide a formal basis for distinguishing between expressive power of turning complete languages.

[1] https://youtu.be/43XaZEn2aLc

[2] The paper it's based on https://homepage.cs.uiowa.edu/~jgmorrs/eecs762f19/papers/fel...

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

#58

Post by Gibbon1 »

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?

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.

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

#59

Post by jcelerier »

dllthomas wrote: post #11
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…

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.

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

#60

Post by jcelerier »

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.

I've written pages and pages of c++ template metaprograms and not once this has ever been an issue
Post reply on HN