6 ms·

I wonder how many HN users see that headline and think "cool" vs. how many see it and think "uh-oh".

• bordercases 10y ago
  I'm in the latter camp.
  • tathougies 10y ago
    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
    • Coincoin 10y ago
      Until the code becomes impossible to comprehend as a result.
      • tathougies 10y ago
        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.
        • CalChris 10y ago
          > 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.
          • thinkpad20 10y ago
            > 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)
            • CalChris 10y ago
              It doesn't mean it's more safe. It doesn't mean it's safe. It just means it's complex, needlessly complex.
              • thinkpad20 10y ago
                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.
          • tathougies 10y ago
            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
            • CalChris 10y ago
              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?
            • 10y ago
    • krapht 10y ago
      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.
      • tathougies 10y ago
        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
        • Drup 10y ago
          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=ReferenceManual.Totality http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...
          • tathougies 10y ago
            You are right about agda. Idris however is not total by default.
      • Ar-Curunir 10y ago
        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.
        • krapht 10y ago
          Program correctness (safety) is way more than just the memory access guarantees Rust gives you.
    • digikata 10y ago
      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...
      • tathougies 10y ago
        That's a problem with c++ in particular though. Languages like Idris and and even Haskell make working with the type system a joy.
        • Oxitendwe 10y ago
          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-not-do-by-giving-up-turing-completeness/23916#23916 http://cs.stackexchange.com/questions/19577/what-can-idris-n...
          • mrkgnao 10y ago
            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.
    • buzzybee 10y ago
      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".
      • srssays 10y ago
        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.
      • whateveracct 10y ago
        Turing complete (or more generally, expressive) type systems are not only about metaprogramming!
      • tathougies 10y ago
        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?
• yyhhsj0521 10y ago
  It's cool... but uh-oh, people are going to write obscure libraries using these features (eyeing c++ template).
  • JoshTriplett 10y ago
    > but uh-oh, people are going to write obscure libraries using these features (eyeing c++ template) People do that in C++ because C++ lacks some features they want, and goes a long time between updates. Rust has many built-in metaprogramming features already, and regularly adds more. And if you have something you want to do and can't currently, you can file an RFC. That makes me much less worried about people (ab)using type-level programming to implement weirdness.
• curun1r 10y ago
  I feel like I've been digging a metaphorical hole for the entirety of the time that I've learned about programming. Often times, I'll look up at the surface where I started and feel pretty impressed with myself at the depth and the breadth of my hole. Then someone will pop his/her head up from the bottom of my hole to show me a nugget he/she has unearthed from miles below me. And while it's undoubtedly cool and interesting, it makes me realize just how much farther I can keep digging. It's both inspiring and ego-crushing.
  • bluejekyll 10y ago
    Ditch the ego, focus on the inspiration; you'll be happier.
• pjmlp 10y ago
  I am on the "cool" camp, because I am all for the advance of the programming concepts on mainstream languages. Just because a language allows for doing cool stuff, kind of newspaper quiz, doesn't mean we should write code daily like that. It is up to us to make the better judgement, according to the team skills and project complexity, about what should be used.
• seanmcdirmid 10y ago
  As a language designer, Turing complete type systems are scary to reason about semantically. In the best case, they require magic numbers to restrict recursion, and you have to ensure those numbers are applied everywhere necessary. A source of early scala bugs, for example, was finding another case where recursion limits needed to be added. And this wasn't code that was designed to stress the type system! In the worst case, they just require way too much thought on behalf of users reading and writing the code. Amount up expressiveness often leads to type errors that are not very easy to understand, or lead to type errors that occur under very strange conditions.
  • kibwen 10y ago
    Graydon was originally quite adamant that Rust's type system not be Turing-complete, but he eventually acknowledged how dreadfully hard it is to prevent Turing-completeness from accidentally leaking into a system and gave up that fight.
    • lomnakkus 10y ago
      > [...] how dreadfully hard it is to prevent Turing-completeness from accidentally leaking into a system and gave up that fight. Yeah, that's my impression too. TC doesn't actually require all that much. (Of course, making it pleasant is a whole 'nother matter.)