Rust’s type system ended up being Turing-complete anyway. It seems like it fell into the same trap as C++ templates: it’s an accidental programming language in a programming language, but with way worse syntax.
The lesson for language designers may be that every useful type system is doomed be Turing complete, so you may embrace it from the start, instead of trying to make it declarative.
> Rust’s type system ended up being Turing-complete anyway. It seems like it fell into the same trap as C++ templates: it’s an accidental programming language in a programming language, but with way worse syntax.
Most anything in software can easily end up Turing-complete though. It isn't that high of a bar unfortunately. I think most mature type and template systems end up as Turing-complete. To single out Rust for this is to ignore that this is just standard fare for mature typing systems.
TypeScript's types are Turing complete: https://github.com/microsoft/TypeScript/issues/14833
Python's type hints are Turing complete: https://arxiv.org/abs/2208.14755
Java generics are Turing complete: https://arxiv.org/abs/1605.05274
The point is that Zig basically circumvents issues surrounding that, by introducing "comptime", where you can just write regular Zig to achieve the same things.
The article showcases a nice example of having this very direct power.
But it really comes up more often than you think as soon as you actually have it.
It's easy in Zig to allocate precisely based on computed values and then have the sizes as part of your types etc. It all falls out of some simple ideas and it's all just regular Zig code.
"Types in Zig are values of the type type" from: https://ziglearn.org/chapter-1/
So instead of making it hard to write incorrect programs, Zig makes it easy to write correct programs.
Here is a really good link that shows the power of Zig's comptime:
https://kristoff.it/blog/what-is-zig-comptime/
The problem is that it ends up being dynamically-typed, like C++ templates. See: https://nitter.net/pcwalton/status/1369114008045772804
> So instead of making it hard to write incorrect programs, Zig makes it easy to write correct programs.
Well maybe in theory, but the current state of Zig is that it makes it hard to write programs no matter how correct because the compiler keeps crashing ¯\_(ツ)_/¯
What are you talking about? The tagged versions are usually quite stable and also plan bug fix follow ups.
If you follow master, you’ll occasionally run in to crashes, which is true of any developing language. If you don’t want that, follow tagged versions.
I am certainly sometimes envious of comptime and what it makes practical, but it’s worth noting that it results in dynamically-typed generics, whereas Rust goes for statically-typed generics, which is in keeping with its goals. There are some significant general maintainability improvements in statically-typed generics; when you use dynamic generics, subtle changes in one place can cause obscure compile errors in a completely different and seemingly unrelated place (commonly called post-monomorphisation errors); this doesn’t happen with static generics.
So… I’m not sold on your wording that it’s circumventing issues, as it’s choosing a different set of trade-offs. In shedding types-are-a-language-of-their-own, you also shed confidence about what’s a breaking change, and make call sites more fragile. Decide for yourself whether it’s worth it.
is there anything fundamental about using the same language at compile time to generate fully static typing that is boiled away? I don't know, but it doesn't seem so?
I'm still in the honeymoon phase with this language and learning, but I agree it's a trade off.
For example your LSP isn't going to help you as much while you edit code.
However being able to express arbitrary compile time constraints and pre-compute stuff without having to go through a code generation tool is really powerful. You can actually use all the knowledge you have ahead of time as long as you can express it in Zig.
So far it seems like Zig is carving out a very strong niche for itself.
What do you mean by dynamically-typed generics and statically typed generics here? I've looked up "post-monomorphization errors" and found some things about assertions about generic types failing because of the choices made by the user who passed in types or constants that do not work with the generic code. It seems like Zig libraries have the option of generating the errors at the right place if they place their assertions in the function that returns the type to the user, but they also have the option of generating the errors in the wrong place if they place their assertions in methods of the type.
> So… I’m not sold on your wording that it’s circumventing issues, as it’s choosing a different set of trade-offs. In shedding types-are-a-language-of-their-own, you also shed confidence about what’s a breaking change, and make call sites more fragile. Decide for yourself whether it’s worth it.
Client code can just look at all the members of all the structs so there's not really much hope for enforcing that changes cannot break any client code using compiler-adjacent tooling.
It’s easiest to see the distinction in otherwise-similar systems, so I’ll choose Rust generics (statically-typed) and C++ templates (dynamically-typed).
In Rust, the generic constraints (the traits that the type must satisfy) are a contract, part of the signature. The caller must satisfy them, and then the callee knows nothing else about the type it has received. Therefore, changes inside the body of the generic method will never† cause any code that uses the function to stop compiling.
In C++, templates don’t have that, so you have to seek knowledge of what conditions your type must satisfy some other way, and it’s easy to accidentally depend on additional details (since it’s not statically checked), so that changes in the template that you thought were harmless actually break someone else’s code somewhere else that uses your template in ways you didn’t expect.
https://gist.github.com/brendanzab/9220415 has a decent example, though it’s from 2014 and refers to Zero and One traits that were removed from the standard library before Rust 1.0, and the compiler messages would be better today as well.
—⁂—
† In practice there’s at least one way of leaking details, so post-monomorphisation errors that aren’t compiler bugs can actually happen, though it’s very rare: if you return an `impl Trait`, the body leaks whether it implements auto traits like Send.
>instead of making it hard to write incorrect programs, Zig makes it easy to write correct programs.
Or May be rephrasing it ( To avoid the word "instead" which may anger Rust supporters );
Rust Makes it hard to write incorrect programs, Zig makes it easy to write correct programs.
I think this single sentence captures the philosophical difference between Rust and Zig. And of course there is no right or wrong in philosophy.
I fully agree. It’s an interesting trade off that is worth thinking about.
> Most anything in software can easily end up Turing-complete though.
not really, if you actually pay attention when youre designing the type system:
https://arxiv.org/pdf/2005.11710.pdf
"if you actually pay attention" or, in other words, if you produce novel research into the area that's worthy of publishing, and noting that this is only just the start and has its own limitations:
> The cost is that of requiring a whole program analysis and disallowing programs that would result in infinite instantiations (Section 5.3). Clearly, this is the beginning of the story, not the end.
My experience with Turing-completeness in any custom DSL or similar is that you will generally get Turing-complete systems unless you work really really hard to avoid them. And it only takes one wrong move by anything anywhere in the system, and you'll end up with Turing-completeness.
Instead of trying to avoid Turing-completeness, just expect it, embrace it and instead deal with its consequences to contain the fallout.
> Instead of trying to avoid Turing-completeness, just expect it, embrace it and instead deal with its consequences to contain the fallout.
this seems like such a cop out. its like saying "oh failure is a given, so don't even try to succeed". at least currently, Go generics are NOT Turing complete. the generics were designed in part specifically to avoid that. so just because Rust (and others) failed, doesn't mean its impossible.
> this seems like such a cop out. its like saying "oh failure is a given, so don't even try to succeed".
It is a pragmatic cop-out yes. I found it is easier to make progress by assuming that you'll get to Turing Complete rather than investing in the time to avoid it. I found that the downsides of Turing Completeness are usually overhyped or primarily theoretical.
> so just because Rust (and others) failed, doesn't mean its impossible.
It definitely is not impossible. But I don't know if it is worth it.
In the end I want fast compile times, type safety, easy to maintain code and good error messages. I do not care if the type system is Turing Complete.
> In the end I want fast compile times, type safety, easy to maintain code and good error messages. I do not care if the type system is Turing Complete.
I think the problem is some languages with Rust go too far with generics, which probably triggers the turing complete. for example, this is valid Rust code:
but you have to follow the code all the way to "do_work" before you ever find the type of anything. Go does not allow this. you need to either declare a concrete type:
or a explicit generic type:
I think Rust is lose lose, because the underlying type implementation is Turing complete, and I would argue the code is actually less readable because of the overuse of type inference.
> I think Rust is lose lose, because the underlying type implementation is Turing complete
I am not a Rust coder so I can't really comment.
Currently, I do TypeScript, which also has a Turing complete type system, and I love it. Of course all things in moderation. Even though I could make a completely obtuse type design for projects, I try to not write code that others can not understand.
I don't think most people care at all that their type system is turing complete. It basically never comes up.
Agreed. Adding to this point, why should I care? Am I missing anything obvious on why you don't want it?
Not really. In theory it means your compiler might never terminate... that does not usually happen.
"It isn't that high of a bar unfortunately." --> "It isn't that high of a bar."
100 times this. C++ is progressively making more and more of the language and stdlib available at compile time (constexpr, consteval, constinit). Once this is accomplished, there will be two very complicated Turing-complete programming languages available at compile time, one that is convenient to program (C++) and one that is not (C++ templates).
Zig jumps straight to the finish line by making the main language available at compile time out of the gate, and by using it as the "generics language", Zig's generics are both simpler and more powerful.
author here. That's a really good observation kornel. Rust's philosophy of avoiding post-monomorphization errors at all costs is usually sung in high praises (followed by a ridicule of C++ template errors) - but it comes at a cost. And when you stray away from the declarative way and start plastering const generic bounds everywhere you really feel the pain.
Anyways, I think engaging in this topic as a community is super important. Cause that's the only way to push PLs forward and explore this massive space.
I did this! Singeli is an Elixir-like compile-time language where types and variables are first-class values, on top of C-ish semantics that are meant to be more like "portable assembly". It's designed for high-performance code where you have to be able to control the specific instructions, but the overall strategy could be useful in other domains too.
https://github.com/mlochbaum/Singeli
And a podcast on it came out Friday:
https://www.arraycast.com/episodes/episode62-what-is-singeli
I listened to that, it was good! I was surprised there is an entire podcast about array programming. Looking forward to future episodes, and also to trying AoC with BQN again in a few months.
> instead of trying to make it declarative
Wait, no. A language being Turing complete and declarative are completely independent things.
That's the point!
> Rust’s type system ended up being Turing-complete anyway. It seems like it fell into the same trap as C++ templates
I hear it is a common trap.
https://aphyr.com/posts/342-typing-the-technical-interview
That something can be Turing-complete in the worst case doesn’t mean that you hit those worst-cases on a frequent, or even occasional basis.
Agreed. The strong agree is that Rust's type system---and many other languages' type systems---is a parallel language to its runtime language. Parameterized types are like functions; instantiating a type parameter is like a function call; `impl ... where` does pattern matching. You get a pure functional language based on pattern matching and implemented with memoization. These type systems are often Turing complete on purpose, but yet it's surprisingly hard to get an infinite loop. Like, both Rust's and Java's type systems are Turing complete, yet I've never hit an infinite compilation loop in either by accident.
For more on type systems as programming languages: https://ductile.systems/oxidizing-the-technical-interview/ plus its links at the top.
What I would like to see is a programming language where the runtime language and the comptime language are the same, or nearly the same, and where the comptime language is type safe. Zig isn't this: its `comptime` language is essentially dynamically typed. In Zig, if a function `f` takes a `comptime` argument `t: Type`, it can call `.print()` on it, and the compiler will just assume that that's fine. If you call `f`, you had better read the docs because the type system won't tell you that `t` needs to have an `print()` method. If you're calling `f` directly, that's pretty straightforward, but the trouble comes when you actually call `h`, and `h` looks at the value of some string and based on that decides to call `g`, and `g` calls `f`, and the docs for `h` weren't entirely clear, so now you're seeing an error in `h`, which you didn't even call. Instead, if `f` is going to call `.print()` on a `t`, then its argument `t` can't just be a `Type`, the compiler should check that it's a `Type with method .print()->String`. This requirement would then flow to `g` and `h`, so the type signature for `h` is guaranteed to tell you that `t` is required to have an `print()` method.
For more on merging runtime and comptime languages in a type safe way, see 1ML: https://people.mpi-sws.org/~rossberg/1ml/
EDIT: Deleting my criticism of C++ templates lest it distract from the more substantial things I had to say above.
> What I would like to see is a programming language where the runtime language and the comptime language are the same, or nearly the same, and where the comptime language is type safe
I have aproximately 0 knowledge of it, but I think TemplateHaskell should do that.
Nope. Haskell's type system guarantees that code you construct in Template Haskell is well-formed, but the code you construct is only type checked once, at the end. So if you have a function that constructs code, and the code it constructs has a type error in it, you won't find out unless you call the function. Just like Zig.
> What I would like to see is a programming language where the runtime language and the comptime language are the same, or nearly the same, and where the comptime language is type safe.
MetaOCaml might the closest one.
> and where the comptime language is type safe
You need dependent types in order to do this, which means doing away with Turing-completeness. (Moreover, the principle 'Type is of type Type' as found in Zig comptime leads to type-unsafety. So you need to replace that with some notion of universes.)
Well, you can have dependent types but limit their expressiveness. Rust, for example, has dependent (comptime) types, but they're very extremely limited:
I imagine having arbitrary comptime code, but more limited use of comptime values in type position.
Also, do you know the exact issue with "Type is of type Type"? I know that can lead to _non-termination_, and non-termination completely breaks proof assistants. For example, you can prove `False` with:
But if you're not building a proof assistant, a function like `make_false()` is fine. Does it lead to any additional problems?
Surely they knew that it would become a programming language in its own right. That's the fate of all such statically typed languages which give you type-level power but that aren't dependently typed. (Of course dependently typed languages might end up with other languages like its own tactics language.)
I don't think anyone has ever been surprised to find that a type system (with inference) is turing complete.
I think there's still value in pushing people towards something declarative. For example, a static type system might have an `any` type for things that aren't expressible statically but that doesn't mean type system designers should embrace dynamic typing from the start instead of trying to make it static. Similarly, it makes sense to have panics/exceptions in a language as an escape hatch for errors where the application can't reasonably do anything gracefully, but it's (arguably) a bad experience to take that to the extreme and panic for all errors.
I think there's value in accounting for the possibility that there will be edge cases that preclude hard-and-fast rules like "purely static" or "purely declarative", but I dislike the philosophy of projecting the 1% use case (e.g., "dynamic" or "turing complete") onto the 99% use case (where e.g., static and declarative would be ideal). I like when languages design for the 99% case and allow for escape hatches for the remaining 1% with the understanding that these escape hatches are intended to be used judiciously.
To put it differently, embrace that there may be escape hatches in the initial design, but prefer to think of them as "escape hatches" with the entailed understanding that they should be rarely used.
This is sort of the approach that I've considered. Type systems are just predefined code/behavior baked into a language, but there's technically nothing stopping you from arbitrarily extending the compiler like Lisps do with macros to support a type system that's written in the language itself.
Type Systems as Macros:
https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po...
Genuine question:
How do type system that are so abstract and complex to become turing complete help?
I definitely find it extremely helpful to be able to write containers of any type (like std::vector<T>), that saves a ton of code duplication, but beyond that what more is needed and why? What we're competing with here is: just write a function that operates on the data types you want and gets the job done.
You're writing code for the CPU that has to actually do something, on actual known types.
What programming task is simplified by having an "any" type or a type system that allows you to write pong-played-turn-by-turn-using-compiler-error-messages? It's cool that you can have an "any" type just like universal sets in set theory, but what real-life programming scenario does this simplify (you can already write containers that can contain anything you want without using such as thing as an "any" type)?
At least not the kind of programming tasks I do, but admittely I think fairly low level and prefer my types to have exact known amounts of bits, known signed integer convention and endianness so I can efficiently use shifts and get the bits I need, preferably with as little undefined behavior as possible.
Asked differently: If one were to design a programming language that only has basic types (primitives, structs/classes, ...) and templates to allow functions/classes to operate on any type (but not more than that; substitute template type with the actual type, compile this, nothing more), what feature will users of the language be missing and complain about?
> You're writing code for the CPU that has to actually do something, on actual known types.
(Partial) specialization, which is a feature used to get templates to do actual something on actual types is what principally allows templates to be turing complete.
It's about when you want to enable optimisations or conveniences depending on the parameterized type.
For example, in the std::vector<T> type, if T supports being moved, you want to use that when growing your vector for performance. If T doesn't support being moved, you will have to copy it instead.
Boom: you've ended up with template metaprogramming.
> Asked differently: If one were to design a programming language that only has basic types (primitives, structs/classes, ...) and templates to allow functions/classes to operate on any type (but not more than that; substitute template type with the actual type, compile this, nothing more), what feature will users of the language be missing and complain about?
This is a really good question. There are some languages that work as you describe: SML and some others in that family. There are generic functions and types, but the type parameters are basically just placeholders. You can't do anything with a value whose type is a type parameter, except store it and pass it to things that also take type parameters.
That gives you enough to write a nice reusable vector type. But it doesn't let you easily write a nice reusable hash table. You can, but users have to pass in an explicit hash function that accepts the key type every time they create a hash table.
It might be nice if a type itself could indicate whether it's hashable and, if so, what it's hash function is. Then, if you create a hash table with that key type, it automatically uses the hash function defined by that type.
Now you need some sort of constraints or type bounds in your generics. That's what traits in Rust and bounds in Java and C# give you. (The literature calls it "bounded quantification".) It's a big jump in complexity. But it does mean that now you can call functions/methods on arguments/receivers whose type is a type parameter, and those calls can be type checked.
Bounds are themselves types, so what kinds of types can you use in bounds? Can they be generic? If so, what kinds of type arguments are allowed? Can you use type parameters from the surrounding type?
For example, which of these are OK and which aren't (using Java-ish syntax):
Any kind of bounded quantification will give you 1-3. What about 4 and 5? This is called "F-bounded quantification". Why would you want such a thing?
Collections with fast look-up are important, which is why we extended our generics to enable us to write nice reusable hash tables. But some data types aren't easily hashed but can be easily ordered. A sorted collection is faster than an unsorted one.
How would we write a generic sorted collection? We could require you to always explicitly pass in an ordering function for any given element type, but it would be nice if the element type itself could supply is order function.
You could define a "Comparable" interface that a type can implement to support comparing an instance against another object of some type, like:
And then implement it on your type, like:
In our sorted collection, elements all have the same type, so the bound that we need looks like:
Notice that we have "T" inside the bound. That's F-bounded quantification.
Using type parameters inside a bound isn't the only place recursive types like this show up. Let's say you wanted to make a generic type comparable. You'd do something like:
Now here, the implements clause is using not just the type parameter of the enclosing type, but the entire type.
We had a couple of fairly modest goals:
* Be able to create reusable hash tables where the hash function is inferred from the key type.
* Be able to create reusable sorted collections where the comparison function is inferred from the element type.
And in order to get there, we needed generics, bounds, and even F-bounded quantification.
Adding even a little more usefulness to our collection types will quickly have us reaching for variance annotations, associated types, and even more exotic stuff.
> It might be nice if a type itself could indicate whether it's hashable and, if so, what it's hash function is. Then, if you create a hash table with that key type, it automatically uses the hash function defined by that type.
> Now you need some sort of constraints or type bounds in your generics. That's what traits in Rust and bounds in Java and C# give you.
Isn't having a function "Hash", called in your template, that takes your type as argument (and give compiler error if the function doesn't exist for this type, as a consequence of substituting in your type) sufficient for this?
In other words, duck typing
Yes, C++'s duck typing approach is one solution to this.
It takes the solution out of the type system, which keeps the type system simpler.
But it effectively turns your compiler into an interpreter, and an interpreter which may fail.
One way to think of C++'s notoriously huge, incomprehensible template compile time errors is that they are effectively stack traces of the template expansion interpreter running at compile time. When you see one of those errors, you have to figure out which chain of compile-time execution led to it.
Everything that's frustrating about dynamically typed errors that makes users reach for static types is exactly true of C++'s template system as well. (And, conversely, everything that's powerful and simple about dynamic types is true of C++'s template system.)
It's actually even worse in C++ because of SFINAE. The "interpreter" running at compile time in C++ doesn't just abort on the first error. It's like an interpreter for a dynamically typed language that also supports overloading. Any time a function has an error, the interpreter backtracks and tries the next overload. If all overloads fail, then it keeps unwinding.
So what you get isn't just a call stack on a template expansion error, it's a call tree of every place it tried to get to that failed.
This was a fantastic write up. Very interesting, thanks so much!
Fascinating! Now I'm curious, what causes this? Where does Turing completeness come from?
Polymorphism? Inference? Higher-kinded types? (Probably not that last one, I don't think Rust has them.)
Put another way, what would it take a for a type system to NOT become Turing complete?
Turing completeness doesn't have to come from a single feature, it often comes from a combination of features.
e.g. the interaction between subtyping (e.g. inheritance) and generics (with variance) is tricky: https://www.cis.upenn.edu/~bcpierce/papers/variance.pdf
It can be highly nontrivial to tell if a language actually has a Turing complete type system: the 2007 Kennedy&Pierce paper made it likely that java was turing complete; but it took until 2016 until it was finally proven that to be turing complete (https://arxiv.org/abs/1605.05274).
> What would it take a for a type system to NOT become Turing complete?
An analysis of all possible interactions between all features in the type system, building a formal proof that the type system is not turing complete. This is not really realistic for the style of complex generic type systems that programmers are now used to, it would need to be a vastly simpler language.
All you need is a way to branch and a way to loop, so anything with conditional types and recursive types will be Turing Complete
Basically design in dependent types into the language right from the beginning (like Iris) - such that types are first class and can be computed and manipulated like any other language construct.
it's easier to make something Turing-complete than not... most interesting example is probably rule 110.
The point is that it’ll end up that way, so just embrace it from the start.
the lisp way. the problem is it results in software which is difficult to reason about due to all the compile-time execution, even if you have state-of-the-art compile-time debuggers (if any language has them, it is lisp).
I haven’t so far found any zig code terribly hard to reason about, and it’s important to know that compile time type crafting (currently) doesn’t support decls. Although you can madness your way around that, theres idiomatic ways to manage this.
Comptime is definitely very powerful, and even the top people using zig frown upon “magic”.
But to be completely honest, “magic” shit just happens all the time if you enable it. Rust macro abuse to get “magic” comes to mind. If it happens in rust, it’ll certainly happen in zig.
Can you show how you'd implement a Turing machine in Rust types?
I am not seeing it, so am likely overlooking that.