3 ms·

When I discussed my discovery with a friend of mine who is doing his PhD, he was not really excited about it and once I showed him the features of TypeScripts t

When I discussed my discovery with a friend of mine who is doing his PhD, he was not really excited about it and once I showed him the features of TypeScripts typesystem, he immediately explained me why it has to be turing complete. So in theory, this result is nothing new and nothing "newsworthy". However, even being myself a CS student close to finishing my BA degree and stronlgy interested in CS theory, I didn't know that result and I couldn't imagine how powerful TS's typesystem is. So, there actually are a lot of people who underestimate the power of typescripts typesystem completely and who could write even safer code if they knew about it. I don't know exactly anymore how I "rediscovered" this turing-completeness-property, but at that time I was developing a "fully" typed SQL builder as an alternative to knex (https://github.com/hediet/ts-typed-sql https://github.com/hediet/ts-typed-sql) and did some research on how to make certain SQL constructs typesafe in TypeScript. For example, one thing I needed, was a type RecordTypeToJson<T> which could recursively transform a sql record type T to a proper json type: https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Types.ts#L68 https://github.com/hediet/ts-typed-sql/blob/master/src/AST/T... Without the devices discovered in the TC-proof I wouldn't have been able to implement that particular type. And once I recognized the power of TS, I found some other useful devices, e.g. how to use overloading to report custom error messages for invalid types (https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Queries/SelectQuery.ts#L89 https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Q...) or how to track whether more than one column is selected (https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Queries/SelectQuery.ts#L57 https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Q...). I hope that these ideas inspire other libraries as well!

bad_user 9y ago
A turing complete system doesn't necessarily mean it's powerful, or useful, it just means that it's equivalent with a turing machine and in the case of type systems, that usually happens because general recursivity is allowed. And that can also mean that it is error prone.
- fauigerzigerk 9y ago
  It doesn't mean useful, but in my opinion it definitely means powerful. Being expressive enough to describe any possible algorithm is a power. No self respecting super hero would deny that, not even TypeScript's worst enemy. But with every power comes a weakness. Compile times can no longer just seem endless. They can actually be endless, and there is no way to prove otherwise. What I find unconvincing about many Turing complete type systems is that pragmatically speaking they are really shitty general purpose programming languages. If we create Turing complete type systems and suffer the consequences, why not go all the way and make it actually practical to write proper meta programs the way Lisp has done?
  - bad_user 9y ago
    I kind of disagree, describing any possible algorithm is not that powerful, given that an actual Turing machine can do it. And along with Turing machines you've got problems, like undecidability and the halting problem.

bad_user 9y ago

A turing complete system doesn't necessarily mean it's powerful, or useful, it just means that it's equivalent with a turing machine and in the case of type systems, that usually happens because general recursivity is allowed. And that can also mean that it is error prone.

fauigerzigerk 9y ago
It doesn't mean useful, but in my opinion it definitely means powerful. Being expressive enough to describe any possible algorithm is a power. No self respecting super hero would deny that, not even TypeScript's worst enemy. But with every power comes a weakness. Compile times can no longer just seem endless. They can actually be endless, and there is no way to prove otherwise. What I find unconvincing about many Turing complete type systems is that pragmatically speaking they are really shitty general purpose programming languages. If we create Turing complete type systems and suffer the consequences, why not go all the way and make it actually practical to write proper meta programs the way Lisp has done?
- bad_user 9y ago
  I kind of disagree, describing any possible algorithm is not that powerful, given that an actual Turing machine can do it. And along with Turing machines you've got problems, like undecidability and the halting problem.