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

81–90 of 91 posts

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

#81

Post by cphoover »

linkdd wrote: post #32
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 we should strive for strong type systems with a lot of type inference. I especially like Typescript for that. Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbe…

Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.

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

#82

Post by TheCoelacanth »

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.

Not really, I can predict that anything I will actually do that has valid types will type check.

Some pathological valid cases invented by someone trying to break the type checker, might not type check.

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

#83

Post by linkdd »

cphoover wrote: post #81
linkdd wrote: post #32

Earlier quoted context omitted.

I think we should strive for strong type systems with a lot of type inference. I especially like Typescript for that. Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbe…

Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.

I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser.

[1] - https://pest.rs/

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

#84

Post by cphoover »

linkdd wrote: post #83
cphoover wrote: post #81

Earlier quoted context omitted.

Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.

I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser. [1] - https://pest.rs/

Thanks

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

#85

Post by andrepd »

coolreader18 wrote: post #46
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

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/

Amazing

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

#86

Post by nestorD »

dragontamer wrote: post #75
nestorD wrote: post #62

Earlier quoted context omitted.

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 complica…

While I do agree for MtG and Pokemon Yellow (their main value as examples is that they are fun and inexpected), Peano arithmetic is simple.

It is fondamental but still probably the simplest way to implement natural integers : a natural number is either 0 or one plus a number.

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

#87

Post by cphoover »

linkdd wrote: post #83
cphoover wrote: post #81

Earlier quoted context omitted.

Interesting... What framework did you use to write your parser? I've been curious about tinkering with some exploratory language design myself.

I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser. [1] - https://pest.rs/

BTW you should finish your project. You built the parser already!

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

#88

Post by whatshisface »

feoren wrote: post #55
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?

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 m…

>Have you never used map or filter operations on streams of data?

If that's the standard for complicated programs, then I really don't understand how types can get confusing; filter doesn't even change the types of its arguments. I guess structs of several promises are a good example because you could mix up which fields contained which future objects, and that code would be distant from the API call to produce the object.

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

#89

Post by linkdd »

cphoover wrote: post #87
linkdd wrote: post #83

Earlier quoted context omitted.

I used the pest[1] library in Rust, it uses something a bit like an EBNF syntax to write the grammar and generate a PEG parser. [1] - https://pest.rs/

BTW you should finish your project. You built the parser already!

I wanted to use the LLVM Rust bindings to generate LLVM IR, but I still need to do some more reading on how to represent high-level constructs in such a low-level language. Also, generics and type inference is hard to implement! :p

I don't have the focus required for that at the moment, but it's still in my TODO list :)

I might publish the parser on github and post it on Hackernews to see if anyone would be interested to help.

NB: the project started with the thought "what my ideal language would look like?"

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

#90

Post by dragontamer »

nestorD wrote: post #86
dragontamer wrote: post #75

Earlier quoted context omitted.

> 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 complica…

While I do agree for MtG and Pokemon Yellow (their main value as examples is that they are fun and inexpected), Peano arithmetic is simple. It is fondamental but still probably the simplest way to implement natural integers : a natural number is either 0 or one plus a number.

The general thing about complexity (be it 3SAT or Turing Completeness) is that the underlying rules are extremely simple.

The issue is understanding the implications of those rules. For something like 3SAT, all possible 3SAT puzzles can be solved (aka: either satisfied with an example, or unsatisfied with a "certificate of unsatisfiability").

For problems in the Turing Complete complexity class, the "implications" of the rules you list are semi-decidable.

Ex: Is there an odd-perfect number (https://en.wikipedia.org/wiki/Perfect_number)? Well, all we gotta do is try all numbers. Once we find an odd perfect number, we'll know its possible. But if we never find an odd perfect number, we remain in a state of uncertainty.

Though I guess, a future mathematical proof may prove if an odd perfect number exists or not. So I guess I'm back to the halting theorem as an example. For the halting-theorem: you can "solve" any computer by simply executing the program and waiting for it to end. If it ends, you know its a program that ends.

If it doesn't end... well... semi-decidable. You don't know that it never ends.

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

Anyway, if a hypothetical type-system were "only as powerful as 3SAT", then all calculations under that type system would be proven to come to a solution eventually.

EDIT: And even weaker systems, such as "Horn-clause Logic", (which is the basis for Prolog programming language) can have further proofs of efficiency (not only will all systems come to a solution eventually, but we have strong proofs about the number of steps a computer will take to reach that solution).

These attributes are likely useful to elements of programming language design. Sure, we are making a Turing complete language (aka: machine code). But that doesn't mean that all sub-languages in the language need to also be Turing complete. Imagine if "printf" or "scanf" was Turing complete, it'd be a complexity nightmare!!

Post reply on HN