31 ms·
TypeScripts Type System Is Turing Complete
- hprotagonist 9y agohttps://www.destroyallsoftware.com/talks/the-birth-and-death-of-javascript https://www.destroyallsoftware.com/talks/the-birth-and-death... Closer and closer to reality. ;)
- lordleft 9y agoCS student here, why is Turing completeness a bad thing in this case?
- cwyers 9y agoThe halting problem, basically. It's possible for something constructed in the type system (not the program that's being typed, like a type declaration) to recurse infinitely and never stop running until terminated. That said, there's some contention in that thread over whether or not Turing completeness has been demonstrated.
- amenghra 9y agoThat can be solved by setting a reasonable upper bound on how many types can be nested. In general, having a turing complete type system isn't a major issue, many languages have that property.
- Gehinnn 9y agoThis is how the TypeScript team fixed this issue: https://github.com/Microsoft/TypeScript/pull/15011 https://github.com/Microsoft/TypeScript/pull/15011
- cestith 9y agoI don't think Turing completeness is necessarily bad here. When speaking of a general-purpose language you usually want it to be Turing complete. However, you may not want a single subsystem of that language to be Turing complete on its own. That's a lot of complexity for one thing. Another reason you might not want a Turing-complete language inside your language is it'd be possible to write type declarations that do things semantically separate from the rest of the code. If you're looking at a program you typically think the only logic embedded in the types is constraining the way data is used in the program. All the code to actually do things with the data is elsewhere. If you have a type system that is by itself Turing complete, it could do any calculation someone wanted to encode into it without assistance from the rest of the source code. That's potentially a security nightmare to audit.
- klodolph 9y agoWe generally want the compiler to finish within a reasonable amount of time and either give a compiled version of the program or an error message. This is literally impossible if the type system is Turing complete, because the type checker could loop forever and you'd be unable to detect the difference between a program that can't be compiled and one that just takes a long time to compile.
- krastanov 9y agoA naive question: Is it only the type inference that will recurse indefinitely? I.e. If you always specify your types and cast them explicitly, is the Turing completeness still an issue?
- klodolph 9y agoType inference is not necessary in general nor does it look like the TypeScript example here uses type inference in any significant way.
- Gehinnn 9y agoThe properties that enable TS' type system to be turing complete are recursive types and indexer types. Indexer types allow you to write `{ foo: string }["foo"]` which results in the type `string`.
- deleted 9y ago[deleted]
- icebraining 9y agoIt's not impossible, the error message will just be "timeout".
- chongli 9y agoThen you get valid programs timing out when they would have compiled otherwise.
- unholiness 9y agoTuring complete systems are highly capable, and thus, are harder to prove anything about. The halting problem notwithstanding, there's first the "there are things that don't halt" problem: that is, you can write a valid TypeScript program that will never finish compiling. Now, this really shouldn't be an issue unless someone is deliberately abusive. Java's generic types are also Turing complete[0], and it hasn't been problematic. Just because an abusive program exists doesn't mean it will be written. But who am I kidding... this is the JavaScript community. I'll give it 2 weeks until someone releases a framework allowing you to write functions that don't compile unless their input is a prime number. [0] https://arxiv.org/pdf/1605.05274.pdf https://arxiv.org/pdf/1605.05274.pdf
- notamy 9y ago> I'll give it 2 weeks until someone releases a framework allowing you to write functions that don't compile unless their input is a prime number. Honestly that seems like it could be pretty useful for making sure that "correct" data is passed at compile-time...
- pmiller2 9y agoI believe "don't compile," in this context, is short for "their compilation doesn't halt." That seems like a bad thing to me. ;)
- myusernameisok 9y agoI don't understand how this is fundamentally different from just doing it in regular javascript. You could write a javascript function that recurses forever on condition x: just write a function that calls itself with the same parameters unless condition x is met. How is it fundamentally different if the type system does it?
- shusson 9y ago> How is it fundamentally different if the type system does it? runtime vs compile time. For example someone could write some TypeScript that would forever compile, which is intuitively unexpected when compiling.
- mhh__ 9y agoOpinions of this differ, see C++ templates etc: Simplistically, this now makes it easier for code to get very complex (a la C++ templates). The question is, should this be in the hands of the language designers or the users of said language?
- munificent 9y agoThe typical answer here is "It means the type checker might run forever". That's a sort of scary worst-case scenario, but I don't think it's that relevant in practice. I think the more motivating reason why this might be a bad thing is it implies the type system is pretty complex and that complexity can be a problem. When users are reading and writing programs, they are running the type system in their head to decide what code to write and reason about how it behaves. If you can create types that cause arbitrary computation to be performed, then you're forcing the user to run a pretty complex simulation in their head. Worse, unlike the dynamic runtime behavior of their program, they need to do that reasoning before they can even begin to run their program. It's not like "well, sure, you can maybe get the program into a weird state". It's "you won't be able to even run the code at all until you understand and fix all the type errors." Given that, it's important to keep the type system simple where you can. The challenge is balancing that with the need to make the type system sophisticated enough to not prevent users from writing programs that are dynamically correct. All type systems are inherently pessimistic — there are programs you can write that would do the write thing but where the type system can't prove that so it generates a "false positive" error. A few of those are tolerable. Most users don't seem to mind adding a seemingly pointless cast here and there, or reorganizing some already-correct code to please the checker. But if they have to do that too much, they start to feel like the language is stupid or getting in their way. See, for example, the perennial complaint about the lack of generics in Go.
- SolarNet 9y agoBecause it was probably accidental. As opposed to using something like Lisp macros, where meta programming doesn't require using the type system language and shoving it into the shape you need, and is basically normal programming. Now that it's been discovered people are going to rely on the quirks that enabled it, and it's now an accidently designed meta programming language inside your type system. See C++ for why that is bad.
- evadne 9y agoRelated: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview
- johnny_reilly 9y agoOh I love this - thanks for sharing!
- geofft 9y agoHas anyone ported Aphyr's type-level 8-queens code (https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview) to this typesystem? I tried porting it to Rust a bit back but got stymied by, uh, the typesystem trying to resolve equality in the wrong direction (by adding type constructors instead of removing them) or something. I guess that's UndecidableInstances maybe?
- lopatin 9y agoGotta mention Shen here, the language with an intentionally Turing complete type system. You can write your types as Horn clauses. http://shenlanguage.org/ http://shenlanguage.org/
- catnaroek 9y agoWhy is this considered newsworthy? How many practical type systems do you know that are not Turing-complete, yet powerful enough as development aids? (Hindley-Milner doesn't count. HM might have decidable type checking, but actual programming languages don't just use HM. In particular, OCaml and GHC Haskell do not have decidable type checking.) Heck, maybe computer scientists ought to do more research into non-Turing-complete development tools.
- munificent 9y ago> How many practical type systems do you know that are not Turing-complete, yet powerful enough as development aids? Dart has a pretty sophisticated type system — generics, generic methods, function types, subtyping, etc. — but isn't Turing-complete as far as I know.
- chombier 9y agoTo me, the issue is not the type system being TC, which may or may not be desirable depending on applications. What is a bit unsettling is that somebody noticed that it was in fact TC: this property should be clear from the type system design and not something to be discovered afterwards.
- naasking 9y ago> In particular, OCaml and GHC Haskell do not have decidable type checking. Pretty sure OCaml type checking is decidable, as is C# and F#, at the very least.
- tome 9y agoCare to mention what about GHC Haskell's type system is not decidable? AFAIK only some extensions like UndecidableInstances can make it undecidable.
- Drup 9y agoOCaml's _type_ system is not turing complete (unless you have a new striking example to provide, but this would be considered a critical soundness bug). There are two undecidable bit in OCaml's typechecker: 1) Checking module types, due to the possibility of naming and manipulating type signatures, in particular in functors. It's extremely hard to hit by accident, since computing in signatures is quite unidiomatic (and unwieldy). 2) Exhaustiveness of pattern matching for GADTs. You can hit that one (although, not "by accident") fairly easily, so the exploration is bounded and always terminate. As for Haskell, the base system for typeclasses is not turing complete, you need a specific combination of extensions which are known to be dangerous together. Finally, to answer the first question ... Most dependently typed languages (Coq, Agda) are not turing complete. People who do research in type systems are usually rather careful about the whole thing.
- lewisl9029 9y agoNot entirely on topic, but I'm curious if anyone could comment on the similarities and differences between TypeScript and Flow in their more recent iterations. I've been doing a bit of research and it seems like they've grown to become fairly similar in terms of syntax and overall capability, but I'd love to hear if anyone has compelling reasons as to why you'd choose one over the other. Lately, I've been evaluating Relay Modern for a new project, and one of its new features is the ability for the Relay Compiler to generate Flow type definitions based on your GraphQL schema, which makes for a very compelling case to choose Flow if I were to go with Relay Modern for the project. Are there similar tools for generating TypeScript or Flow type definitions from GraphQL schemas for use in the Redux + Apollo ecosystem? Also, do either type system have a story for leveraging type definitions to perform generative testing like you could in Clojure with Spec?
- jahewson 9y agoMy personal take on this is that TypeScript has surpassed Flow in its feature set and the availability of typings for existing libraries. The features which previously made Flow unique have been incorporated into TypeScript, two particular favourites of mine being string literal types and tagged unions. You can indeed generate TypeScript types from a GraphQL schema, using apollo-codegen: https://github.com/apollographql/apollo-codegen https://github.com/apollographql/apollo-codegen Generative testing from types in TypeScript isn't something I've seen. With a static type system, if the code compiles then you know it's correct with respect to the types - no amount of automated testing would prove otherwise. In a dynamic language like Clojure where there are no types then you need generated values and tests to try and get some (still incomplete) safety. So you want a rich type system which can capture as much information about your data as possible - TypeScript does a nice job of this, on the whole . Having said that, if you wanted to provide testing data or constraints along side your types, @decorators provide a means of adding custom annotations - so you, or someone could certainly generate test for data beyond the richness of the type system, e.g. a valid email.
- lewisl9029 9y agoThanks for the response. TypeScript definitely seems to be the community favorite, and availability of third-party type definitions is definitely an important concern. Will definitely take a look at apollo-codegen. Though now I'm curious how the two systems differ, if at all, in their handling of third party libraries that _lack_ type definitions? From slackingoff2017's response below, it sounds like Flow might handle this scenario a bit more gracefully by still providing some level of static checks, whereas TypeScript would give up on checking any usages of the library altogether, correct? > Generative testing from types in TypeScript isn't something I've seen. With a static type system, if the code compiles then you know it's correct with respect to the types - no amount of automated testing would prove otherwise. In a dynamic language like Clojure where there are no types then you need generated values and tests to try and get some (still incomplete) safety. So you want a rich type system which can capture as much information about your data as possible - TypeScript does a nice job of this, on the whole . It's certainly true that in a static type system, generative testing can't derive any value from the types alone, and both Flow and TypeScript are static type systems. That was probably the wrong way to frame my question. I guess what I'm trying to ask is if there's a runtime property specifications system for JavaScript, similar to Clojure Spec, that can specify more than just properties of a system that are statically provable, and can test those specifications using a generative approach.
- the_common_man 9y agoHere is the proof https://gist.github.com/hediet/63f4844acf5ac330804801084f87a6d4 https://gist.github.com/hediet/63f4844acf5ac330804801084f87a...
- Gehinnn 9y agoWhen 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 agoA 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 agoIt 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?
- hellofunk 9y agoOkay, but you know what else is Turing complete? BASIC. Bash script. Assembly. In 2017 I'm not sure that something being Turing complete should be considered a shocker, or even that meaningful. Heck, I've seen people write whole programs just using clojure.spec which is supposed to be only for type annotations.