Hacker News Reader

Comment by tathougies | Hacker News Reader

Can you explain why? A Turing complete type system allows sophisticated constraints to be embedded and programs to be rejected at compile time that would otherwise throw runtime exceptions.

It seems best that errors are caught at compile time

View on HN

In general, metaprogramming capabilities(macros, templates, some forms of late binding) create brittle, high-friction abstractions when applied unjudiciously. They're like writing a customized compiler, except the resulting error messages are all awful or nonexistent and the code can't be debugged as easily.

Thus, even in languages where metaprogramming is a prominent feature(e.g. most Lisps) the culture tends to evolve towards writing in a plain style and sparingly using these abilities because they have so much footgun power.

Now, it's possible that Rust's method of extension doesn't have the same capability to cause harm as something like macros, and is more along the lines of generic types, which have a narrower scope and are more in line with everyday needs. But everyone who's seen it happen is justifiably wary about a proclamation of "this time is different".

In a statically-typed language, the starting point is "nothing typechecks". Then each additional language feature (e.g. generics, records, ADTs, lifetimes) must be implemented as an additional capability of the type checker. This "nothing is allowed unless explicitly permitted" is a necessary condition for soundness.

The most important goal for any programming language is that it is useful, i.e. it can express common patterns without hacks or kludges. Languages that are not useful tend to be forgotten.

However, chasing the dual goals of usefulness and soundness inevitably leads to type-system bloat. If "nothing is allowed unless explicitly permitted" and "everything must be somehow allowed" then it the list of things that are explicitly permitted will end up being very, very long.

Turing complete (or more generally, expressive) type systems are not only about metaprogramming!

Turing complete type systems are not metaprogramming.

You talk about writing a custom compiler / type checker -- this is exactly what unit tests are. Are you against those as well? What's wrong with integrating certain sorts of test into the source itself?

If the type system is Turing-complete, how are you going to test the soundness of your types? Who is going to write unit tests for the types?

From having dipped into C++ at a point in my history, it make me think of C++ templates which were also turing complete. Many of skilled people with templates could go overboard into a point where a significant implementation of the program was in an very separated "template metaprogram space" where it was difficult to manage and debug. You would have to read some primary code, then start doing template transforms in your head to figure out what was actually happening. The compile and run-time errors that could pop out were also terrible and long, giant dumps of template syntax trees..

You can get absolutely phenomenal performance, but any major template capability has a high risk of becoming a DSL with terrible debugging ability and slow comprehensibility.

Judicious use could be very nice though...

That's a problem with c++ in particular though. Languages like Idris and and even Haskell make working with the type system a joy.

Haskell's type system isn't Turing-complete or even particularly sophisticated. There are extensions to its type system implemented in GHC that in theory give you unbounded computation, but a) those aren't actually Haskell and b) nobody does any real work with them and c) it gives up trying to typecheck if it takes too long. I don't know much about Idris but a few seconds of searching tells me its type theory is not Turing-complete either.[1]

[1] http://cs.stackexchange.com/questions/19577/what-can-idris-n...

If you're talking about things like UndecidableInstances or FlexibleContexts, um, they are n't exactly uncommon!

In any case, saying that Haskell 98 is the One True Haskell(TM) isn't accurate. Almost all code (beyond the LYAH level) written today uses a few Haskell 2010 extensions, mostly for ergonomics (things like OverloadedStrings are a good example of this), not to mention all the extensions that make mtl let you write "lift whatever" instead of "lift . lift . lift ..." and infer how "high" you want to go up the monad transformer stack.

UndecidableInstances is used in more libraries than you would think. In general, it doesn't inpact safety although certain programs may fail to compile because the compiler gives up after a while. However, this won't result in the acceptance of ill typed programs. Ultimately, the compiler is just acting like any other language run time -- at some point, your Python interpreter will give up (run time type error), your browser will give up (that annoying stop script pop up), and your operating system will give up (out of memory exception).

Also, your link indicates idris's type system is Turing complete.

>Idris won't reduce partial functions at the type level, in order to keep type checking decidable.

Totality precludes Turing-completeness. Specifically, functions that don't terminate are by definition partial, and if you can't express functions that don't terminate then it isn't Turing-complete.

The "performance" you get by using templates is offset by binary size and/or compilation time. You can't get something for nothing.

Agreed, and then for example when you go to further reexamine performance and maybe try to fit parts of the binaries into cache, then you're trying to possibly optimize at two-different levels at the same time. This isn't to say that Rust will have the same problem, I hope it avoids it entirely. But if the question is why is there a vague feeling of dread when Rust declares a turing complete type system - a C++ template meta-programming ghost is the reason for me.

As tatterdemalion's top comment in this thread states, the deliberate restrictions imposed by the Rust compiler prevent type-level programming from being used for the arcane tasks that TMPL achieves in C++. To say nothing of the fact that Rust has far easier and better ways of achieving metaprogramming than abusing the type system...

Compilation time is a consequence of lack of modules.

In C++11 you can pre-instantiate common used templates (extern template)and hopefully C++20 will finally get modules.

Until then, those that are able to use just VS C++ 2015 and 2017, can make use of incremental linking and experimental modules, to ease the pain a bit.

Non-Turing complete systems can also allow extremely strong constraints to be embedded, while also allowing the type system to be decidable. Remember, while Rust makes a lot of noise about being safe, it isn't Ada Ravenspark, or ATS, or Idris/Agda.

Decidability is not really important for type systems. As long as the type system is sound, you're good. If your compilation is taking too long, I would classify that as a bug.

Thanks for the obvious point that rust isn't agda. However, certainly you can agree that agdas type system is able to capture a strictly greater set of constraints than a typed language without a Turing complete type system

Agda's type system is not turing complete, you can only run on the type-level functions that are proven to be terminating [1] (using well-founded induction or co-induction).

Same for Coq, and probably Idris.

[1]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...

You are right about agda. Idris however is not total by default.

What do Idris and Agda have to do with safety? They have a GC RUNTIME; Rust leverages the type system to get ergonomic, safe and fast code without a runtime.

Program correctness (safety) is way more than just the memory access guarantees Rust gives you.

Idris does not have one exclusively.

Allocations can be removed just like in Rust thanks to uniqueness types:

http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...

Also funny that you mention ergonomics, given that improving the current state is one of the main goals of 2017's roadmap.

Until the code becomes impossible to comprehend as a result.

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.

> 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