Comment by CalChris | Hacker News Reader

Comment by CalChris | Hacker News Reader

Parent Full thread

> I mean sure. I for one advocate using non-Turing complete languages for things that don't need it. However, if you're using a Turing complete language, what's wrong if the type system is Turing complete as well.

Let's unpack that. You advocate using non-Turing complete languages for things that don't need it. Great. Something like DTrace does not need a Turing complete language and D isn't Turing complete. Awesome.

But then you say that if you're using a Turing complete language, what's wrong if the type system is Turing complete as well?

Well, does a Turing complete language, C or Rust, need or in any way benefit from a Turing complete type system? Does a low level systems language, C or Rust, need or benefit from a Turing complete language?

Other than an implementation pun, I don't see any point in this needless complexity. The point of a type system is safety. I don't see how a Turing complete type system gets you to heaven.

> The point of a type system is safety.

Unless I'm missing something, having Turing completeness in a type system doesn't mean it's less safe; it just means the type checker might not terminate. In which case, of course, the code will not compile and thus cannot do anything unsafe (of course the type checker itself might, say, allocate infinite memory and crash your machine... But that's a different story)

It doesn't mean it's more safe. It doesn't mean it's safe. It just means it's complex, needlessly complex.

I wasn't claiming that it makes it more safe. The implication of the post I was responding to, or at least, how I read it, was that a Turing complete type system might compromise safety.

Yes a Turing complete language should have a Turing complete type system. Systems level work has the most to gain from this. Application code can crash with relatively little consequence. System code usually needs to be stable, so enforcing as much as possible at compile time is nice.

Do you believe in unit tests? Ultimately, this is using he taget language to type check itself. If you had a well integrated Turing complete type system (c++ does not), then you could start enforcing some of these at the compilation stage

Have you ported LLDB so that I can debug my Turing complete type system unit tests?

Methinks you are defending pointless complexity. How did we ever write unit tests before this awesomeness was sprung upon us?

Who is going to write unit tests for the Turing complete types?

Reply on news.ycombinator.com