Rust's type system is Turing-complete (2017)
sdleffler.github.io
sdleffler.github.io
I personally find lists of programming language that made the conscious decision to not be Turing complete (such as Coq the theorem prover) more intriguing.
If you know how to reach Turing completeness in those systems, you wouldn't call any of those "simple".
MtG for instance is considered one of the more complicated card games.
Pokemon Yellow's turing completeness proof involved arbitrary code execution by swapping memory locations around.
Peano axioms / Arithmetic underlies an entire theory of abstract mathematics.
---------------
EDIT: I think decidable is an important attribute of systems that are weaker than Turing Complete. There are still very powerful decidable equations (ex: 3SAT, most famously), which has an answer (either satisfiable, or unsatisfiable), but may need O(2^n) time (or longer) to calculate the result.
Turing Complete is only semi-decidable: if something halts it will halt in finite time. If something won't halt, you'll never know.
It is fondamental but still probably the simplest way to implement natural integers : a natural number is either 0 or one plus a number.
The issue is understanding the implications of those rules. For something like 3SAT, all possible 3SAT puzzles can be solved (aka: either satisfied with an example, or unsatisfied with a "certificate of unsatisfiability").
For problems in the Turing Complete complexity class, the "implications" of the rules you list are semi-decidable.
Ex: Is there an odd-perfect number (https://en.wikipedia.org/wiki/Perfect_number)? Well, all we gotta do is try all numbers. Once we find an odd perfect number, we'll know its possible. But if we never find an odd perfect number, we remain in a state of uncertainty.
Though I guess, a future mathematical proof may prove if an odd perfect number exists or not. So I guess I'm back to the halting theorem as an example. For the halting-theorem: you can "solve" any computer by simply executing the program and waiting for it to end. If it ends, you know its a program that ends.
If it doesn't end... well... semi-decidable. You don't know that it never ends.
-------------
Anyway, if a hypothetical type-system were "only as powerful as 3SAT", then all calculations under that type system would be proven to come to a solution eventually.
EDIT: And even weaker systems, such as "Horn-clause Logic", (which is the basis for Prolog programming language) can have further proofs of efficiency (not only will all systems come to a solution eventually, but we have strong proofs about the number of steps a computer will take to reach that solution).
These attributes are likely useful to elements of programming language design. Sure, we are making a Turing complete language (aka: machine code). But that doesn't mean that all sub-languages in the language need to also be Turing complete. Imagine if "printf" or "scanf" was Turing complete, it'd be a complexity nightmare!!
There are two main drawbacks to accidental Turing-completeness:
- You can no longer statically analyze the system for properties like termination, because you can't solve the halting problem (at least not without extra bounds).
- Some people will try to abuse turing-completeness to solve their problem, leading to a jumbled mess. If this becomes an accepted way of using your system, it has basically failed.
Some pathological valid cases invented by someone trying to break the type checker, might not type check.
I don't think that's true at all, and I think there are two extreme examples that drive the point home:
Consider on the one hand a language where typechecking is entirely terminating so long as you don't use one particular feature; however, that feature is also not very useful in practice (even notwithstanding the potential nontermination) and so it doesn't actually get used by real people writing real code. Adding that feature doesn't improve the language, but I contend that it doesn't make the type checker "much [less] valuable."
On the other hand, consider a language where type checking provably terminates in all cases, but based on subtleties sometimes completes in seconds and sometimes takes decades. I don't think this provides "much more [value]" than a similar system that sometimes fails to terminate only in some of the cases where the other would take (say) more than a week.
My point is that your type checker is already possibly-non-terminating. That ship has sailed. So you might as well make it the best possibly-non-terminating typechecker that you can.
The fact that you can get Turing complete behavior in some part of a system with some encoding doesn't mean it's accessible enough that it's relevant when deciding how I am going to accomplish something or (typically) when deciphering what someone else has written.
People using this feature does not incur any "extra" effort.
Not all problems are technical. This is the sort of thing that can be solved with people skills.
As a trivial example C plus “come from” is fundamentally the same language as regular C, and one can trivially translate it to remove come from. That doesn’t mean that adding come from to C would be a good idea.
Incidentally, Googling "C plus come from" only returns two relevant results, the parent comment and a manual for an esoteric programming language called C-INTERCAL that uses the COME FROM statement and compiles to C. [2]
Threaded INTERCAL actually has a very disciplined approach to safety. Each thread gets its own copy of all variables, so threads do not share any mutable data at all. However, they still share the same code, which is also mutable, so they can communicate through that.
Disciplined, maybe; usable/sane, certainly not. Then again, it's INTERCAL, so that was most certainly the intention.
[1] https://youtu.be/43XaZEn2aLc
[2] The paper it's based on https://homepage.cs.uiowa.edu/~jgmorrs/eecs762f19/papers/fel...
[1] https://stackoverflow.com/questions/254395/whatever-happened...
Because being touring complete alone has been reached a while ago. Why even bother developing peogramming languages after that? Probably because just being touring complete alone doesn't necessarily enable you to comfortably and quickly create abstractions and structures that are easy to write, modify and compose to a bigger whole.
The claim that what Rust is doing with its type system isn't useful is one you need to show us examples for. Simply stating something unfavourable about some project out of gut feeling is bad form.
Being "Turing complete" only means that your thing supports unlimited recursion; or, in other words, that whatever objects it encodes can be arbitrarily large.
See: https://en.wikipedia.org/wiki/Rule_110
P.S. This also means that, technically speaking, the computers we use aren't Turing complete because they have RAM and storage limits.
Rust's Type System Is Turing-Complete: Type-Level Programming in Rust - https://news.ycombinator.com/item?id=13843288 - March 2017 (117 comments)
I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.
This reminds me of that: http://litherum.blogspot.com/2019/03/addition-font.html
You can craft font files that perform arbitrary calculations… if you give the font shaping engine a (practically) unlimited stack, where it usually limits recursion to 6 levels. If you do so, you can make a font that does math (or whatever you want) as part of computing ligatures.
But in practice, you hardly ever hit those kinds of limits unless you're trying to do something silly on purpose. Sure you cannot port Doom to font substitution lookup tables, despite them being Turing complete. But that doesn't make your font shaping engine useless, or even broken.
edit: by which I mean, the theoretically defined type system, not the actual program implementing it.
Aren't such programs not very interesting by definition?
And why would you call them "valid" programs?
I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.
But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.
for any reasonable program, you're not going to run into problems with the turing complete aspects of the type system. it's only when you start cleverly lifting logic into the type system to run in that typeless compile-time space that you'll feel punished by it.
if you want to check if a type adheres to some constraint and then choose between different things to do, and then do that recursively et cetera, sure, you'll blow the template expansion stack.
because you're not longer programming in the typed language, but in the typeless meta-language of its type system.
(I think the person you replied to is exaggerating the significance of this, though: it's obviously not a big deal in practice.)
How is Turing-completeness related to soundness? I am behind on CS theory, but what little I know about category-theory tells me this isn’t the case.
No, you're mixing up concepts (consistency vs. soundness).
If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem.
A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.
The only thing this means is that type checking a Rust program might never terminate.
Nothing more, nothing less.
It might take 10 seconds, it might take 10 days, it might take till the universe freezes.
In practice, the compiler - like pretty much every single compiler with a Turing complete type system - has a recursion limit, that rejects programs that accidentally take too long to type check, but users can increase this limit by adding a source annotation (that's suggested by the compiler).
This is completely orthogonal to whether the programs are valid or not.
If your program is invalid, the compiler will never accept it, no matter how much compute time you throw at it.
Type checking always terminates for valid Rust programs (by definition), so if you throw enough compute at any valid Rust program, the compiler will eventually accept it.
I feel I'm in a minority here... but I like the nimbleness of dynamic languages, or languages where the type system has a minimal presence.
I have the full power of the language to force type correctness instead of some janky meta language.
And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.
If that's the standard for complicated programs, then I really don't understand how types can get confusing; filter doesn't even change the types of its arguments. I guess structs of several promises are a good example because you could mix up which fields contained which future objects, and that code would be distant from the API call to produce the object.
But map, which 90% is used after filter, does.
const foo = client.someRequest()
.filter(item => /* some condition */)
.map(item => /* some transformation */)
someFunction(foo)
The answer is either:
- you implement your own type system (based on json schema?)
- you write the type checks manually in your tests
Every REST/GraphQL APIs relies on a strongly typed schema.
A type system in your programming language is a feature that allows you to "encode" the schema within the language itself.
The most expressive the type system is, the less validation code you need. The less code you have, the easier it is to maintain your code.
You don't like the verbosity? That's what type inference is for, take a look at that Typescript example:
const handlers = {
foo: () => { /* ... */ },
bar: () => { /* ... */ }
}
const action: keyof typeof handlers = someOtherFunc()
handlers[action]()
In one domain the program thinks of time in 1/256ths second ticks. And in another it thinks in terms of 1/32768ths of a second. Elsewhere it thinks in terms of ms.
Having them all represented as an int is often confusing. For me that wrote the code. God help anyone else.
Python is not Perfect (bad general-purpose performance), but IMHO honestly a more productive language than Go.
And Python has type hinting nowadays which is sweet when you want it. Type hinting is good for self-documenting stable code.
Python could similarly declare that exceptions are only for dead-end panics, and all error handling should be done by returning 2-element tuples.
Type systems are very useful to establish the semantics of your operations. For example `int + int` is not the same operation as `string + string`, and definitely not the same as `int + string` (which does not exist in most languages). You could call `+` an addition, but addition only exists for numbers, for strings it is a concatenation.
Is `int + string` the same as `string + int` ? (commutativity)
Is `int + int + string` the same as `(int + int) + string` or `int + (int + string)`? In that case, what does `int + string` returns? (associativity)
Now consider this code:
def foo(a, b):
return a + b
function foo(a: int, b: string) {
return a + b
}
Finally, in math an object does not "have a type" but "belongs to a set/class". For example, "1" is an integer, an odd number, a real, a complex, a scalar, a rank 1 tensor, etc... Saying that "1" is only an integer is incorrect, but that's what most programming language do.
I've tried to design a language where "typeof variable == type" does not exist but instead you have "variable isof type" running the type checking code, example:
class user(v: struct {
name: string,
logged_in: bool
})
class logged_user(u: user) check
# this code is evaluated when 'isof' is called
u.logged_in = true
end
class allowed_user(u: user) check
# =>, <=> operators are logical connectors
# A => B is true if A and B are true or A is false
# A <=> B is true if A and B are both true
u isof logged_in <=> u.name in ['admin', 'root']
end
let alice = { name: 'alice', logged_in: false }
assert alice isof user = true
assert alice isof logged_user = false
assert alice isof allowed_user = false
let bob = { name: 'bob', logged_in: true }
assert bob isof user = true
assert bob isof logged_user = true
assert bob isof allowed_user = false
[1] - https://pest.rs/
I don't have the focus required for that at the moment, but it's still in my TODO list :)
I might publish the parser on github and post it on Hackernews to see if anyone would be interested to help.
NB: the project started with the thought "what my ideal language would look like?"
There's a function in a popular Python scientific library (I can't recall the name of the library or the function, unfortunately), which takes a parameter n and returns a float if n=1, and a list of floats if n!=1. This behavior wasn't documented explicitly – I found out during testing – and is just annoying to deal with when the parameter n isn't a constant.
This wouldn't happen in a statically typed language, because 1) the function's signature would hint at this unexpected behavior, and 2) the designer of that function has to think about the assumptions they make and the guarantees they give, and not just "how to solve the problem in front" of them.
Personally I've never found type mismatches to be particularly a large problem, as you can still support input validation where needed, generally at some application message boundary like an http request/response, and the type of bugs caused by mismatched types are easy to diagnose and test for.
The class of bugs that to me are much more difficult to fix unlike type mismatches are not immediately visible or do not give descriptive messages for example race conditions, memory leaks, logical errors, etc...
It links to Wikipedia (WP), which defines "system" by:
> a computational system (such as an abstract machine or programming language)
there is no better citation[0], because it's not true under some definitions of "computational system", per WP's definition of "computational system" [3]. For example, under the WP definition of "abstract machine", a non-computable function satisfies the definition. Or we can define it as follows: input: strings in an alphabet A, output: {true, false}, operations allowed: check for membership in a language L in alphabet A.
So we see that theoretical formal languages are a subset of computational systems. But there are uncountably many formal languages and only countably many TM. Crucially, we can easily turn each language into one that acts as a universal turing machine while still being distinct. Hence there are uncountably many Turing-complete languages for a given alphabet A[2]
[0]: incidentally, the linked WP page claims slightly differently (unimportantly) that "All known Turing-complete systems are Turing-equivalent, which adds support to the Church–Turing thesis."
[1]: "A typical abstract machine consists of a definition in terms of input, output, and the set of allowable operations used to turn the former into the latter." Absent a more precise definition, I assume the set may include arbitrary mathematical operations (and it is useful to define non-computable abstract machines, and in general usage in the field abstract machines may refer to languages more powerful than Turing machines).
[2]: Sketch: Let U' be a Universal TM in alphabet A (hence U is Turing-complete), let M' denote the language it accepts, and let 0 be a symbol of A. Define M such that if i' in M', then i in M, where i is i' with every symbol duplicated and 0 prefixed (hence if i'="123", i="0112233") Define N such that if i' in complement(M'), then i in N, where i is i' with every symbol duplicated and 0 prefixed. Observe that every language disjoint from N that contains M is Turing-complete (wrt a slightly modified description for TMs and the simulated input than the one for U'). Now, let L be an arbitrary language in A. Define f(L) = { j | j' in L, j is j' with every symbol duplicated }. Then we see that f(L), M, N are all disjoint. And if T, U are distinct languages, so (f(T) union M) and (f(U) union M) are distinct languages that simulate Turing machines (i.e. they are Turing-complete). Hence there are uncountably many Turing-complete languages. There are only countably many Turing machines, hence only countably many Turing-equivalent languages, so in fact most Turing-complete languages are not Turing-equivalent languages.
[3]: of course,
The "All known Turing-complete systems are Turing-equivalent, which adds support to the Church–Turing thesis." thing seems to have an implied "Turing-complete systems that are physically implementable." (I edited the article to add that.)
Thanks for sharing!