10 ms·

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

by pornel 3y ago

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.

avgcorrection 3y ago
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.)
- insanitybit 3y ago
  I don't think anyone has ever been surprised to find that a type system (with inference) is turing complete.
Ar-Curunir 3y ago
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.
hnfong 3y ago
> 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 https://aphyr.com/posts/342-typing-the-technical-interview
dist1ll 3y ago
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.
bhouston 3y ago
> 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 https://github.com/microsoft/TypeScript/issues/14833 Python's type hints are Turing complete: https://arxiv.org/abs/2208.14755 https://arxiv.org/abs/2208.14755 Java generics are Turing complete: https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274
- dgb23 3y ago
  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/ https://ziglearn.org/chapter-1/ So instead of making it hard to write incorrect programs, Zig makes it easy to write correct programs.
  - bhouston 3y ago
    Here is a really good link that shows the power of Zig's comptime: https://kristoff.it/blog/what-is-zig-comptime/ https://kristoff.it/blog/what-is-zig-comptime/
  - littlestymaar 3y ago
    The problem is that it ends up being dynamically-typed, like C++ templates. See: https://nitter.net/pcwalton/status/1369114008045772804 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 ¯\_(ツ)_/¯
baq 3y ago
it's easier to make something Turing-complete than not... most interesting example is probably rule 110.
- wredue 3y ago
  The point is that it’ll end up that way, so just embrace it from the start.
  - baq 3y ago
    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).
    - wredue 3y ago
      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.
marcosdumay 3y ago
> instead of trying to make it declarative Wait, no. A language being Turing complete and declarative are completely independent things.
- dgb23 3y ago
  That's the point!
packetlost 3y ago
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.
- naasking 3y ago
  Type Systems as Macros: https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-popl2017.pdf https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po...
throwaway894345 3y ago
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.
mlochbaum 3y ago
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 https://github.com/mlochbaum/Singeli And a podcast on it came out Friday: https://www.arraycast.com/episodes/episode62-what-is-singeli https://www.arraycast.com/episodes/episode62-what-is-singeli
- mk12 3y ago
  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.
lenkite 3y ago
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.
itishappy 3y ago
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?
- ynik 3y ago
  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 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 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.
- AprilArcus 3y ago
  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
justinpombrio 3y ago
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/ 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/ 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.
- gpderetta 3y ago
  > 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.
haberman 3y ago
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.
Aardwolf 3y ago
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?
- gpderetta 3y ago
  > 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.
- widdershins 3y ago
  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.
- munificent 3y ago
deleted 3y ago
[deleted]
jjtheblunt 3y ago
Can you show how you'd implement a Turing machine in Rust types? I am not seeing it, so am likely overlooking that.

by pornel 3y ago

avgcorrection 3y ago

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.)

insanitybit 3y ago
I don't think anyone has ever been surprised to find that a type system (with inference) is turing complete.

Ar-Curunir 3y ago

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.

hnfong 3y ago

> 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 https://aphyr.com/posts/342-typing-the-technical-interview

dist1ll 3y ago

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.

bhouston 3y ago

> 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 https://github.com/microsoft/TypeScript/issues/14833 Python's type hints are Turing complete: https://arxiv.org/abs/2208.14755 https://arxiv.org/abs/2208.14755 Java generics are Turing complete: https://arxiv.org/abs/1605.05274 https://arxiv.org/abs/1605.05274

dgb23 3y ago
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/ https://ziglearn.org/chapter-1/ So instead of making it hard to write incorrect programs, Zig makes it easy to write correct programs.
- bhouston 3y ago
  Here is a really good link that shows the power of Zig's comptime: https://kristoff.it/blog/what-is-zig-comptime/ https://kristoff.it/blog/what-is-zig-comptime/
- littlestymaar 3y ago
  The problem is that it ends up being dynamically-typed, like C++ templates. See: https://nitter.net/pcwalton/status/1369114008045772804 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 ¯\_(ツ)_/¯

baq 3y ago

it's easier to make something Turing-complete than not... most interesting example is probably rule 110.

wredue 3y ago
The point is that it’ll end up that way, so just embrace it from the start.
- baq 3y ago
  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).
  - wredue 3y ago
    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.

marcosdumay 3y ago

> instead of trying to make it declarative Wait, no. A language being Turing complete and declarative are completely independent things.

dgb23 3y ago
That's the point!

packetlost 3y ago

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.

naasking 3y ago
Type Systems as Macros: https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-popl2017.pdf https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po...

throwaway894345 3y ago

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.

mlochbaum 3y ago

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 https://github.com/mlochbaum/Singeli And a podcast on it came out Friday: https://www.arraycast.com/episodes/episode62-what-is-singeli https://www.arraycast.com/episodes/episode62-what-is-singeli

mk12 3y ago
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.

lenkite 3y ago

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.

itishappy 3y ago

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?

ynik 3y ago
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 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 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.
AprilArcus 3y ago
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

justinpombrio 3y ago

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/ 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/ 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.

gpderetta 3y ago
> 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.

haberman 3y ago

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.

Aardwolf 3y ago

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?

gpderetta 3y ago
> 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.
widdershins 3y ago
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.
munificent 3y ago

deleted 3y ago

[deleted]

jjtheblunt 3y ago

Can you show how you'd implement a Turing machine in Rust types? I am not seeing it, so am likely overlooking that.