TypeScript's Type System Is Turing Complete (2017)(github.com)
github.com
TypeScript's Type System Is Turing Complete (2017)
https://github.com/microsoft/TypeScript/issues/14833
47 comments
You mean zig ? https://ziglang.org/
Check out Circle, a C++ compiler for a superset of C++ that supports regular code at compile time: https://www.circle-lang.org/
You mean like Zig's compile time manipulation of types? It's very powerful but the problem is it makes it harder for IDEs to reason about code.
Ruby's Sorbet? Where type signatures are just Ruby itself with no new syntax. (Not sure if this is what you were looking for though)
Dependently-typed languages often work this way! See for instance "Inductively Defined Propositions" in Coq. (remembering, of course, that propositions are types [2], which proof assistants take quite literally)
[1] https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...
[1] https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...
Lots of other options provided, but it seems like you may be interested in Lisp.
Come back in a few years and I'll link you haskell.org ;)
Check out any dependently typed language.
Idris should also be an example of this.
Jai being developed by Jonathan Blow is like that https://inductive.no/jai/
I really don't like Jai's presentation because there is essentially no text material is available and thus much harder to discuss anything. For the posteriority the actual demonstration is available here [1]; it shows that it is a multi-staged compilation model like Zig, which is very useful and also quite limited.
[1] https://youtu.be/iVN3LLf4wMg?t=1903 (or, seek to 31:43)
[1] https://youtu.be/iVN3LLf4wMg?t=1903 (or, seek to 31:43)
Totally agree. I think that something that has some sort of "partial" evaluation and basically merging values and types would be so powerful and crush many interesting bugs.
Instead of having to do type-level programming, how about relying on the fact that the type checker is also running on a computing machine? The fact that we don't even have super simple stuff like first-class union types (let alone nice type manipulation logic) in most stuff is really painful.
An aside: I think one way Typescript gets away with this (beyond soundness stuff), is that it doesn't have to actually build some high performance evaluation model for its type system. It doesn't care, it's here to check the validity of your code, not to run it! It's a very powerful concept that opened up so much without having to futz about with like... how to efficiently represent all these unions.
How many times have you stared at a thing, think "if I could open up the compiler/type checker at the end, I could totally verify some property of my code, but it is not expressible in the type system"?
Instead of having to do type-level programming, how about relying on the fact that the type checker is also running on a computing machine? The fact that we don't even have super simple stuff like first-class union types (let alone nice type manipulation logic) in most stuff is really painful.
An aside: I think one way Typescript gets away with this (beyond soundness stuff), is that it doesn't have to actually build some high performance evaluation model for its type system. It doesn't care, it's here to check the validity of your code, not to run it! It's a very powerful concept that opened up so much without having to futz about with like... how to efficiently represent all these unions.
How many times have you stared at a thing, think "if I could open up the compiler/type checker at the end, I could totally verify some property of my code, but it is not expressible in the type system"?
This sounds to me like dependently-typed languages might fit the bill. Look at Agda (more fancy-features focused) or Idris (more real-world programming focused).
Their idea is that you can lift value-level computations to the type level one-to-one. This allows you to do tricks with them that are normally only reserved for type-level things: things like equality proofs that are verified at compile time. In fact, the main reason why dependently-typed languages are developed is to exploit the Curry-Howard correspondence saying that every first-order logic statement corresponds to a _type_ in a dependently-typed language, and the validity of the statement is equivalent to the existence of an inhabitant of that corresponding type (= a value that has that type). This allows you to prove arbitrary properties about the functions in your program without ever leaving your programming languages!
Maybe not exactly what you were looking for, but it technically fits your bill :)
Their idea is that you can lift value-level computations to the type level one-to-one. This allows you to do tricks with them that are normally only reserved for type-level things: things like equality proofs that are verified at compile time. In fact, the main reason why dependently-typed languages are developed is to exploit the Curry-Howard correspondence saying that every first-order logic statement corresponds to a _type_ in a dependently-typed language, and the validity of the statement is equivalent to the existence of an inhabitant of that corresponding type (= a value that has that type). This allows you to prove arbitrary properties about the functions in your program without ever leaving your programming languages!
Maybe not exactly what you were looking for, but it technically fits your bill :)
Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theories. System F, which is weaker than dependent type theory corresponds to higher-order logic. First-order logic actually doesn’t actually correspond to a popular type system, though the correspondence of course exists.
Like this?
https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
Without the Google middleware:
Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf (PDF)
Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. 2020. Dependent Type Systems as Macros. Proc. ACM Program. Lang. 4, POPL, Article 3 (January 2020) - https://dl.acm.org/ft_gateway.cfm?id=3371071 (Redirects to download PDF)
> We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages
Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf (PDF)
Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. 2020. Dependent Type Systems as Macros. Proc. ACM Program. Lang. 4, POPL, Article 3 (January 2020) - https://dl.acm.org/ft_gateway.cfm?id=3371071 (Redirects to download PDF)
> We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages
The language in my head has an effect system, a proof assistant, lets you run code at compile time iff you prove it to be total and pure, and lets you generate new code and proofs with it. This is just dependent types (and it's similar to Jai and Rust) but I think you could market them in a more imperative way to make them usable.
Oh and typestates instead of OOP.
Oh and typestates instead of OOP.
As others have mentioned (only partially though, hence this summary), there are several ways (with varying trade-offs) to achieve this.
Multi-stage programming languages have, well, multiple stages of compilation and you can manipulate types as a first-class value in higher stages. This is a natural extension to the type-level evaluation, as the only thing changes is that the type-level evaluation uses the same fragment of language as the value-level evaluation. Of course we would then have a type of types, a type of types of types and so on; some languages do not distinguish them and a single meta-type is used as catch-all. This model is powerful but you wouldn't get stronger guarantees for lower stages; in particular this model is not a substitute for generic types which typically guarantee that every instance of a generic type is instantiable.
(By the way it is a common misconception that being able to use something like `function f<T>() { return T.size; }` is a first-class type; the type parameter T and the lowered value T is a different thing in different stages.)
Dependently typed languages extend the type system itself to handle mixed types and values. This can be much more huge undertaking than multi-staged programming and harder to reconcile with the type inference and other goodies typically available for strong (enough) type systems, but correctly done they can provide a very strong guarantee that was only possible with static analyses to the limited extent. Note that dependent typing is historically associated with proof assistants but still possible without them; its usefulness and usability would be limited though. (You might have guessed but this is why I don't think dependent typing at the current stage is not the future.)
Conventional metaprogramming methods like macros or code generation are huge wrenches always available for throwing. (Multi-stage programming is also a kind of metaprogramming, but not included in the colloquial "metaprogramming".) They would be significantly limited in scope and/or inconvenient to use, but depending on the scope they might be still appropriate.
Multi-stage programming languages have, well, multiple stages of compilation and you can manipulate types as a first-class value in higher stages. This is a natural extension to the type-level evaluation, as the only thing changes is that the type-level evaluation uses the same fragment of language as the value-level evaluation. Of course we would then have a type of types, a type of types of types and so on; some languages do not distinguish them and a single meta-type is used as catch-all. This model is powerful but you wouldn't get stronger guarantees for lower stages; in particular this model is not a substitute for generic types which typically guarantee that every instance of a generic type is instantiable.
(By the way it is a common misconception that being able to use something like `function f<T>() { return T.size; }` is a first-class type; the type parameter T and the lowered value T is a different thing in different stages.)
Dependently typed languages extend the type system itself to handle mixed types and values. This can be much more huge undertaking than multi-staged programming and harder to reconcile with the type inference and other goodies typically available for strong (enough) type systems, but correctly done they can provide a very strong guarantee that was only possible with static analyses to the limited extent. Note that dependent typing is historically associated with proof assistants but still possible without them; its usefulness and usability would be limited though. (You might have guessed but this is why I don't think dependent typing at the current stage is not the future.)
Conventional metaprogramming methods like macros or code generation are huge wrenches always available for throwing. (Multi-stage programming is also a kind of metaprogramming, but not included in the colloquial "metaprogramming".) They would be significantly limited in scope and/or inconvenient to use, but depending on the scope they might be still appropriate.
LISP.
Using the type system to implement a Natural Numbers Object[1] is pretty clever. Doing math with it is not exactly efficient, but it does prove it works.
[1] https://en.wikipedia.org/wiki/Natural_numbers_object
[1] https://en.wikipedia.org/wiki/Natural_numbers_object
I haven’t used ts. It seems to be a way to get semi-strong typing by using a “compiler-like.” Since this is possible, is it also possible (and performant) to convert something like Java or rust or c# to performant JavaScript and get the full power of a strongly typed language?
> Since this is possible, is it also possible (and performant) to convert something like Java or rust or c# to performant JavaScript and get the full power of a strongly typed language?
It is possible! Java has a few compilers (TeaVM, Google Web Toolkit, JSweet). Rust is usually compiled to WASM (like C and C++). I'm not sure about C#, but F# has Fable. OCaml has two, js_of_ocaml and Rescript (formerly Bucklescript).
It is possible! Java has a few compilers (TeaVM, Google Web Toolkit, JSweet). Rust is usually compiled to WASM (like C and C++). I'm not sure about C#, but F# has Fable. OCaml has two, js_of_ocaml and Rescript (formerly Bucklescript).
[deleted]
I sometimes see headlines like this, saying that a given type system is Turing complete but I've never seen the end result of such a statement.
Are there any examples of programs compiled and runnable strictly in the type system of another language?
Are there any examples of programs compiled and runnable strictly in the type system of another language?
Is there a book or a course that one can use to better learn advanced types in TypeScript?
So far I'm limiting myself to basic types and iterfaces because I can't really wrap my mind around more complex stuff.
So far I'm limiting myself to basic types and iterfaces because I can't really wrap my mind around more complex stuff.
I'm also on a learning path, but here are a couple of suggestions..
The TypeScript documentation is excellent: https://www.typescriptlang.org/docs/
"TypeScript Deep Dive" can be read online - I especially liked the practical "TIPs" section.
https://basarat.gitbook.io/typescript/
The TypeScript documentation is excellent: https://www.typescriptlang.org/docs/
"TypeScript Deep Dive" can be read online - I especially liked the practical "TIPs" section.
https://basarat.gitbook.io/typescript/
Try "Effective TypeScript" from O'Reilly, every chapter I've read so far has been informative - even when I thought I knew the topic inside-out - and it's well-written for the subject depth. You can read some of the items on the author's site e.g.
https://effectivetypescript.com/2020/03/09/evolving-any/
https://effectivetypescript.com/2020/03/24/null-values-to-pe...
https://effectivetypescript.com/2020/03/09/evolving-any/
https://effectivetypescript.com/2020/03/24/null-values-to-pe...
I used to think thay I'd like working with advanced type systems with their "If it compiles, it works" guarantee.
However, I recently spent some time working on a TS codebase with libraries like GraphQL Nexus and that changed my mind. The errors become impenetrable pretty quickly.
I'd say a "good enough" type system like Go's is probably better for most teams. Advanced types come with a power that I wouldn't trust most devs, including myself, with.
However, I recently spent some time working on a TS codebase with libraries like GraphQL Nexus and that changed my mind. The errors become impenetrable pretty quickly.
I'd say a "good enough" type system like Go's is probably better for most teams. Advanced types come with a power that I wouldn't trust most devs, including myself, with.
I may be biased from my past experience, but graphql tends to make codebases a nightmare if you aren't the one that initially set up the system and abstractions - it's (IMO) unnecessarily complex and blurs so many boundaries with a pretty poor tradeoff when compared to "normal" APIs.
After Rust, I think typescript is my favourite language to write these days because of how expressive the type system is - my only complaint is that there's no clean way to bind an interface implementation to a pure data shape like you can in rust and you're forced to either use classes or some sort of DIY binding to an object prototype.
As long as types are kept simple (i.e. avoid weird type tricks unless you actually need them) debugging is usually fairly straightforward assuming you have appropriate tooling setup with your editor/ide.
My biggest gripe with Go is that I find myself wanting more expressivity - not just to minimize boilerplate, but to constrain the data flows and how parts of the code are allowed to fit together.
After Rust, I think typescript is my favourite language to write these days because of how expressive the type system is - my only complaint is that there's no clean way to bind an interface implementation to a pure data shape like you can in rust and you're forced to either use classes or some sort of DIY binding to an object prototype.
As long as types are kept simple (i.e. avoid weird type tricks unless you actually need them) debugging is usually fairly straightforward assuming you have appropriate tooling setup with your editor/ide.
My biggest gripe with Go is that I find myself wanting more expressivity - not just to minimize boilerplate, but to constrain the data flows and how parts of the code are allowed to fit together.
> blurs so many boundaries with a pretty poor tradeoff when compared to "normal" APIs.
I'd love to hear more on this, I've been feeling this way for a while when using graphql-code-generator and apollo-client with react. It feels like there's no layer between data coming into the view from the backend.
Because the queries / mutations are strongly typed with typescript, we end up passing the shape of the request around as a Type, so anytime we want to change our queries, we end up having to touch a lot of application code, instead of having a nice layer between that would handle the transformation.
This is exacerbated by the use of apollo-client's `useQuery` and `useMutation` hooks, which really seem to encourage you to make the requests directly from your views.
At first this all feels amazing, but once the codebase is large enough, I am really start to feel like not having a data transformation layer between the requests and the views is insanity, but everything in the documentation and ecosystem seems to encourage you to do it the way I described above.
This may not be at all what you meant, but I'd love to hear your thoughts, I haven't seen anyone else really talk about this.
I'd love to hear more on this, I've been feeling this way for a while when using graphql-code-generator and apollo-client with react. It feels like there's no layer between data coming into the view from the backend.
Because the queries / mutations are strongly typed with typescript, we end up passing the shape of the request around as a Type, so anytime we want to change our queries, we end up having to touch a lot of application code, instead of having a nice layer between that would handle the transformation.
This is exacerbated by the use of apollo-client's `useQuery` and `useMutation` hooks, which really seem to encourage you to make the requests directly from your views.
At first this all feels amazing, but once the codebase is large enough, I am really start to feel like not having a data transformation layer between the requests and the views is insanity, but everything in the documentation and ecosystem seems to encourage you to do it the way I described above.
This may not be at all what you meant, but I'd love to hear your thoughts, I haven't seen anyone else really talk about this.
And nulls. It’s frustrating that Go programs crash so often with code the compiler allowed.
> advanced type systems
This word is unfortunately overloaded; it can mean either more expressive power or more guarantee, of which TypeScript has the former. TypeScript in particular has a very complex type-level evaluation with less guarantee than conventional strong type systems.
This word is unfortunately overloaded; it can mean either more expressive power or more guarantee, of which TypeScript has the former. TypeScript in particular has a very complex type-level evaluation with less guarantee than conventional strong type systems.
> I used to think thay I'd like working with advanced type systems with their "If it compiles, it works" guarantee.
I think honestly TS is a poor representation of this guarantee, it's extremely easy to trick the compiler and it often doesn't offer you the guarantees you think it does. Because of JS being so widespread TS has become a lot of people's interpretation of this idea. It's not to say it's a bad language and can't help a lot on larger JS projects but I think it shouldn't be put into this category of languages.
I think honestly TS is a poor representation of this guarantee, it's extremely easy to trick the compiler and it often doesn't offer you the guarantees you think it does. Because of JS being so widespread TS has become a lot of people's interpretation of this idea. It's not to say it's a bad language and can't help a lot on larger JS projects but I think it shouldn't be put into this category of languages.
> Advanced types come with a power that I wouldn't trust most devs, including myself, with.
It's sad that TS has turned people off an entire paradigm despite it being a terrible representative of said paradigm.
It's sad that TS has turned people off an entire paradigm despite it being a terrible representative of said paradigm.
This is until you work in Go for some time like me and you find things that are unnecessarily unsafe or difficult because of the insufficient type system.
Even worse if it won't bug you when you're coding but it will crash in production.
Typescript is complicated because it was bolted onto Javascript and has to cover its use cases.
A leap from "Typescript is complicated" to "most teams should use Go" is too far fetched. These languages aren't even in the same domain.
Even worse if it won't bug you when you're coding but it will crash in production.
Typescript is complicated because it was bolted onto Javascript and has to cover its use cases.
A leap from "Typescript is complicated" to "most teams should use Go" is too far fetched. These languages aren't even in the same domain.
You might want to check out Elm. It offers that "if it compiles, it works" guarantee, but does so much more simply and with excellent errors.
You do pay for that in terms of having to write some boilerplate and not having some nice abstractions, but it does mean you don't have that issue of impenetrable errors.
You do pay for that in terms of having to write some boilerplate and not having some nice abstractions, but it does mean you don't have that issue of impenetrable errors.
I feel building a few apps in Elm some years ago had a big impact on my programming style. I never used it professionally but was excellent as a learning experience. Similar to how people describe using something like Haskell but with less upfront cost.
The thing is, Typescript is forced to make compromises because one of their goal is to "type the existing Javascript world". Depending on what you consider an "advanced" type system, OCaml and the likes (Hindley-Milner types systems) can be considered as advanced (for example compared to Go) but are way easier to understand and use than TS.
I remember that one of the arguments of Rescript (a descendant of OCaml made to be compiled to JS) was that their type system covers most of the cases with little mental overhead, and for the rest you have the usual escape hatches. However TS won in the JS ecosystem and now it's hard to avoid its complexity sometimes.
Complex types systems also tend to attract people that tend to built towers of abstractions and complexity because they can. It's a bit like pattern abuse in the OO land.
I remember that one of the arguments of Rescript (a descendant of OCaml made to be compiled to JS) was that their type system covers most of the cases with little mental overhead, and for the rest you have the usual escape hatches. However TS won in the JS ecosystem and now it's hard to avoid its complexity sometimes.
Complex types systems also tend to attract people that tend to built towers of abstractions and complexity because they can. It's a bit like pattern abuse in the OO land.
I constantly find myself wishing for something in between Haskell and TS. I want Haskell pattern matching and typeclasses with TypeScript's records / structural types. Haskell's language extensions are nice but not strictly necessary.
I think Purescript would fit the bill: https://www.purescript.org/
Please excuse my shallow comment but I have to ask.
Having used it on several projects, to me, TS is nothing but a great static analysis tool.
Certainly not a fan of what it does to the code I write and its inability to recognise that Object.defineProperties has its uses
Have I been doing it wrong?
Having used it on several projects, to me, TS is nothing but a great static analysis tool.
Certainly not a fan of what it does to the code I write and its inability to recognise that Object.defineProperties has its uses
Have I been doing it wrong?
[deleted]
With today's TypeScript, a lot more crazy stuff is possible now than what was used to demonstrate turing completeness in the issue.
While it was surprising in 2017 that TypeScript types could be used to run turing machines, with the addition of conditional types, proper support for recursively mapped types, string pattern matching and property renaming, it no longer surprises me at all.
Heck, someone implemented a static string parser + compiler + VM on top of TypeScript types.
While it was surprising in 2017 that TypeScript types could be used to run turing machines, with the addition of conditional types, proper support for recursively mapped types, string pattern matching and property renaming, it no longer surprises me at all.
Heck, someone implemented a static string parser + compiler + VM on top of TypeScript types.
[deleted]
Discussed at the time:
TypeScripts Type System Is Turing Complete - https://news.ycombinator.com/item?id=14905043 - Aug 2017 (88 comments)
TypeScripts Type System Is Turing Complete - https://news.ycombinator.com/item?id=14905043 - Aug 2017 (88 comments)
[deleted]
I'm not talking about self-hosted compiler, which TS is already. But basically what runs statically and what is compiled for runtime to be the same language in two contexts.
C++ is moving in that direction with constexpr expansion, but it also has to carry the legacy of macros, its existing type system, templates, and so on.
We need something clean.