6 ms·

TypeScript's Type System Is Turing Complete (2017)

49 points by rendall 5y ago

historyloop 5y ago
I wanna see a language where the type system and the actual language are the same language. 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.
- rogerclark 5y ago
  Check out Circle, a C++ compiler for a superset of C++ that supports regular code at compile time: https://www.circle-lang.org/ https://www.circle-lang.org/
- IshKebab 5y ago
  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.
- jatins 5y ago
  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)
- benrbray 5y ago
  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.html https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...
- saagarjha 5y ago
  Lots of other options provided, but it seems like you may be interested in Lisp.
- whateveracct 5y ago
  Come back in a few years and I'll link you haskell.org ;)
- kachnuv_ocasek 5y ago
  Check out any dependently typed language.
- madsbuch 5y ago
  Idris should also be an example of this.
- tylorr 5y ago
  Jai being developed by Jonathan Blow is like that https://inductive.no/jai/ https://inductive.no/jai/
  - lifthrasiir 5y ago
    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 https://youtu.be/iVN3LLf4wMg?t=1903 (or, seek to 31:43)
- rtpg 5y ago
  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"?
- tomsmeding 5y ago
  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 :)
  - carnitine 5y ago
    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.
- rscho 5y ago
  Like this? https://www.google.com/url?sa=t&source=web&rct=j&url=https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf&ved=2ahUKEwicsLid_OHxAhUwuqQKHUtxDAgQFjABegQIAxAG&usg=AOvVaw2dG6VNUS-pOHGw0ojEVXpJ&cshid=1626245610811 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://dl.acm.org/ft_gateway.cfm%3Fid%3D3371071&ved=2ahUKEwjA4NjI_OHxAhX9hf0HHcuuA48QFnoECAUQAQ&usg=AOvVaw1ZdMLu5iXBiZ8q6P7drqEY&cshid=1626245528077 https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
  - lioeters 5y ago
    Without the Google middleware: Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf 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 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
- astrange 5y ago
  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.
- lifthrasiir 5y ago
  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.
- drran 5y ago
  LISP.
- crubier 5y ago
  You mean zig ? https://ziglang.org/ https://ziglang.org/
jatins 5y ago
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.
- whateveracct 5y ago
  > 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.
- mdtusz 5y ago
  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.
  - lucian1900 5y ago
    And nulls. It’s frustrating that Go programs crash so often with code the compiler allowed.
  - ervine 5y ago
    > 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.
beebeepka 5y ago
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?
deleted 5y ago
[deleted]
Gehinnn 5y ago
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.
deleted 5y ago
[deleted]
dang 5y ago
Discussed at the time: TypeScripts Type System Is Turing Complete - https://news.ycombinator.com/item?id=14905043 https://news.ycombinator.com/item?id=14905043 - Aug 2017 (88 comments)
deleted 5y ago
[deleted]
DoomHotel 5y ago
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 https://en.wikipedia.org/wiki/Natural_numbers_object
anhner 5y ago
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.
- lioeters 5y ago
  I'm also on a learning path, but here are a couple of suggestions.. The TypeScript documentation is excellent: https://www.typescriptlang.org/docs/ https://www.typescriptlang.org/docs/ "TypeScript Deep Dive" can be read online - I especially liked the practical "TIPs" section. https://basarat.gitbook.io/typescript/ https://basarat.gitbook.io/typescript/
- spiralx 5y ago
  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/09/evolving-any/ https://effectivetypescript.com/2020/03/24/null-values-to-perimeter/ https://effectivetypescript.com/2020/03/24/null-values-to-pe...
vsnf 5y ago
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?
gentleman11 5y ago
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?
- Zababa 5y ago
  > 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).
  - deleted 5y ago
    [deleted]

49 points by rendall 5y ago

I wanna see a language where the type system and the actual language are the same language. 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.

rogerclark 5y ago
Check out Circle, a C++ compiler for a superset of C++ that supports regular code at compile time: https://www.circle-lang.org/ https://www.circle-lang.org/
IshKebab 5y ago
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.
jatins 5y ago
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)
benrbray 5y ago
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.html https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...
saagarjha 5y ago
Lots of other options provided, but it seems like you may be interested in Lisp.
whateveracct 5y ago
Come back in a few years and I'll link you haskell.org ;)
kachnuv_ocasek 5y ago
Check out any dependently typed language.
madsbuch 5y ago
Idris should also be an example of this.
tylorr 5y ago
Jai being developed by Jonathan Blow is like that https://inductive.no/jai/ https://inductive.no/jai/
- lifthrasiir 5y ago
  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 https://youtu.be/iVN3LLf4wMg?t=1903 (or, seek to 31:43)
rtpg 5y ago
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"?
tomsmeding 5y ago
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 :)
- carnitine 5y ago
  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.
rscho 5y ago
Like this? https://www.google.com/url?sa=t&source=web&rct=j&url=https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf&ved=2ahUKEwicsLid_OHxAhUwuqQKHUtxDAgQFjABegQIAxAG&usg=AOvVaw2dG6VNUS-pOHGw0ojEVXpJ&cshid=1626245610811 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://dl.acm.org/ft_gateway.cfm%3Fid%3D3371071&ved=2ahUKEwjA4NjI_OHxAhX9hf0HHcuuA48QFnoECAUQAQ&usg=AOvVaw1ZdMLu5iXBiZ8q6P7drqEY&cshid=1626245528077 https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...
- lioeters 5y ago
  Without the Google middleware: Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf 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 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
astrange 5y ago
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.
lifthrasiir 5y ago
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.
drran 5y ago
LISP.
crubier 5y ago
You mean zig ? https://ziglang.org/ https://ziglang.org/

jatins 5y ago

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.

whateveracct 5y ago
> 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.
mdtusz 5y ago
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.
- lucian1900 5y ago
  And nulls. It’s frustrating that Go programs crash so often with code the compiler allowed.
- ervine 5y ago
  > 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.

beebeepka 5y ago

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?

deleted 5y ago

[deleted]

Gehinnn 5y ago

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.

deleted 5y ago

[deleted]

dang 5y ago

Discussed at the time: TypeScripts Type System Is Turing Complete - https://news.ycombinator.com/item?id=14905043 https://news.ycombinator.com/item?id=14905043 - Aug 2017 (88 comments)

deleted 5y ago

[deleted]

DoomHotel 5y ago

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 https://en.wikipedia.org/wiki/Natural_numbers_object

anhner 5y ago

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.

lioeters 5y ago
I'm also on a learning path, but here are a couple of suggestions.. The TypeScript documentation is excellent: https://www.typescriptlang.org/docs/ https://www.typescriptlang.org/docs/ "TypeScript Deep Dive" can be read online - I especially liked the practical "TIPs" section. https://basarat.gitbook.io/typescript/ https://basarat.gitbook.io/typescript/
spiralx 5y ago
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/09/evolving-any/ https://effectivetypescript.com/2020/03/24/null-values-to-perimeter/ https://effectivetypescript.com/2020/03/24/null-values-to-pe...

vsnf 5y ago

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?

gentleman11 5y ago

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?

Zababa 5y ago
> 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).
- deleted 5y ago
  [deleted]