Got a rule to filter for certain cuss words. At certain times my code it heavily loaded with them, not because the code is bad, but I lack motivation and this is a fun way of dealing with it.
Props to the implementor for sure, but I dunno, if a specification is supposed to solve a problem in a very limited niche, but can actually do something like this, I feel like the spec is actually _too_ flexible.
I feel the same way about "Quake implemented in CSS" demos. Like, very cool, but you actually should not be able to do that...
If anyone has more historical evidence that this is so for CSS, reactions from original authors, etc, or further evidence in the case of TS, I'd be curious to see it.
There isn't really any advantage of artificially limiting the power of type systems. Yes you shouldn't implement Flappy Bird in a type system... but just don't do that. This is obviously for fun.
If you think about it, then it makes quite a lot of sense that a type system aiming to describe the behaviour of a dynamically typed language would end up being this powerful.
Having recently finished I Am A Strange Loop, I'm starting to think it's harder for any formal system to not be Turing-complete than it is for it to be so.
For TypeScript I'm not really sure what you would expect them to change just to avoid being Turing complete. Its Turing completeness is a straightforward consequence of its basic building blocks: iteration, conditional types, and recursive type definitions. Of course TypeScript could go out of its way to avoid Turing completeness by just specifying a maximum recursion depth or something similar, but why?
> specifying a maximum recursion depth or something similar
Doesn't TS do exactly this? It doesn't seem like setting a cap on recursion depth would disqualify something from being Turing complete. Or am I misunderstanding your comment?
Is the recursion limit an implementation detail of the compiler though, or something statically built into the language? If the former there's nothing to prevent the language itself from being Turing complete.
(Similar to how every Turing complete programming language today runs on something technically weaker than a Turing machine due to finite memory.)
Do you mean within a state machine or in practice?
Iteration (loops) are typically represented as jump or branch instructions while recursion requires the creation of a new stack frame on the call stack.
No, in TypeScript's type system. As far as I know, recursion is the only method of iteration but the comment I was replying to seemed to imply otherwise.
Nothing is Turing complete. But it is the stronger form of incomplete where even on a machine with truly unlimited memory it’d still be unable to model some (almost all, formally) executions.
>Turing completeness could be disabled, if it is checked that a type cannot use itself in its definition (or in a definition of an referenced type) in any way, not just directly as it is tested currently. This would make recursion impossible.
Possibly a dumb question but why would Turing incompleteness be desirable in a language whose entire purpose is generating code in a Turing complete language?
I'm not an expert on type theory, but I would guess "Turing complete types" make type checking an undecidable problem, similar to how dependent types make type inference undecidable, since dependent types let you more or less encode arbitrary things into a type (e.g. p is a value of type Prime). That at the very least gives you an infinite search space, and the possibility to encode e.g. a halting property into types.
The problem being discussed is not that typescript the language that compiles to JavaScript is Turing complete, but rather that typescript types the compile time code necessary to validate that typescript are Turing complete. The consequence is compilation speed foot guns, readability and complexity. Not the end of the world, but the sort of thing some people reasonably consider a downside
Not allowing types to be nested within themselves would be a massive downside. You'd lose the ability to model anything tree-like in a reasonable manner. There are some obvious workarounds, but they're so inconvenient that nobody using a scripting language would ever want to be limited to using them.
IMO, TypeScript fails as a developer tool. Developer tools should guide the developer towards making good decisions. TS guides developers towards making poor decisions by facilitating code with complex interfaces.
JavaScript taxes interface complexity through increased cognitive load. Typescript frees developers from that tax and harms architecture in the process.
Funny how business gurus keep saying over and over that incentives are everything and yet when it comes to choosing developer tools for their businesses, they choose tools which promote terrible incentives, instead they choose "that which sounds good"... It's like communism. It sounds good in theory but it fails spectacularly at the incentive layer... It fails at the most important layer.
It's the exact opposite; TypeScript discourages complex interfaces by making them explicit. It's far too easy in a dynamic language for devs to introduce absurdly complex interfaces without understanding the cognitive load it's imposing on other users. In TypeScript, they're forced to type it...which immediately reveals that complexity - if they're able to do it all!
This isn't theoretical; the only reason TypeScript allows for such complex interfaces is precisely because JavaScript devs have created those interfaces, and TypeScript makes a best-effort to make as much JS code type-able as possible.
Isn’t every programming language simply a spec? C and C++ are infamous for just being a spec, with lots of undefined portions resulting in undefined behavior. And if every programming language is a spec, should we inhibit the flexibility of what you can do in them? (I think the answer here is no, but maybe there’s a good reason for limiting what you can do)
Edit: Additionally, it takes very little to define a specification that leads to emergent behavior. That’s not necessarily a bad thing. It’s been awhile, but all you need for a turing machine is a way to store and read memory, and move the tape (instruction pointer) if I remember right. If that’s correct, you can come up with an infinitely complex machine with 3 instructions (provided you have an infinite amount of tape).
TypeScript's specification is very out-of-date. The best "specification" for the language is "whatever the compiler does."
(It's a double-edged sword because it lets the TypeScript compiler move much faster than any other I've seen, but the lack of standardization regularly causes unintended breaking changes, and developing a competing-but-compatible type checker is basically impossible.)
Extremely cool. I'd say you wrote a game engine in Zig and Rust, which allows you to write games entirely in the TypeScript type system, and you wrote Flappy Bird in that engine.
If you want to understand how things like this are implemented in type systems, I'd highly recommend Type-Level TypeScript [0]. I have no affiliation aside from having gone through the course and thoroughly enjoyed it.
TypeScript has such a rich type system that lets you do some crazy things, many of which allow you to have a _very_ ergonomic dev UX while maintaining compile time type safety.
I was actually slightly disappointed that that's how it was accomplished—it's unsurprising to me that someone could write a VM to give runtime meaning to TS types, I find the programs that abuse `tsc` itself to be more interesting.
Here's a similar article that I read recently about using Ocaml's type system to implement a sudoku solver: https://ocamlpro.com/blog/2017_04_01_ezsudoku/ The author defines types to represent a valid sudoku board, and then uses the obscure syntax `-> .` to tell the compiler that a pattern should be unreachable.
There is no compiler error when he compiles an unsolvable input. But when there is a solution, the compiler provides it:
```
Error: This match case could not be refuted.
Here is an example of a value that would reach it:
Grid (A, B, C, D, C, D, A, B, B, A, D, C, D, C, B, A)
```
64 comments
[ 3.7 ms ] story [ 117 ms ] threadThat gave me a hearty chuckle because usually when I write `break` in a for loop, I say in my head the same thing.
Private repos only.
This reminds me of a post the other day about doing more useless things. This is the epitome of that in my mind.
Regardless, really cool project.
I feel the same way about "Quake implemented in CSS" demos. Like, very cool, but you actually should not be able to do that...
(In the case of TS, see https://github.com/microsoft/TypeScript/issues/14833)
If anyone has more historical evidence that this is so for CSS, reactions from original authors, etc, or further evidence in the case of TS, I'd be curious to see it.
Also CSS can't iterate so it's just at the level of arithmetic.
Doesn't TS do exactly this? It doesn't seem like setting a cap on recursion depth would disqualify something from being Turing complete. Or am I misunderstanding your comment?
(Similar to how every Turing complete programming language today runs on something technically weaker than a Turing machine due to finite memory.)
[0] https://herringtondarkholme.github.io/2023/04/30/typescript-...
Iteration (loops) are typically represented as jump or branch instructions while recursion requires the creation of a new stack frame on the call stack.
That sounds like a reasonable resolution.
https://github.com/microsoft/TypeScript/issues/14833
JavaScript taxes interface complexity through increased cognitive load. Typescript frees developers from that tax and harms architecture in the process.
Funny how business gurus keep saying over and over that incentives are everything and yet when it comes to choosing developer tools for their businesses, they choose tools which promote terrible incentives, instead they choose "that which sounds good"... It's like communism. It sounds good in theory but it fails spectacularly at the incentive layer... It fails at the most important layer.
This isn't theoretical; the only reason TypeScript allows for such complex interfaces is precisely because JavaScript devs have created those interfaces, and TypeScript makes a best-effort to make as much JS code type-able as possible.
Edit: Additionally, it takes very little to define a specification that leads to emergent behavior. That’s not necessarily a bad thing. It’s been awhile, but all you need for a turing machine is a way to store and read memory, and move the tape (instruction pointer) if I remember right. If that’s correct, you can come up with an infinitely complex machine with 3 instructions (provided you have an infinite amount of tape).
(It's a double-edged sword because it lets the TypeScript compiler move much faster than any other I've seen, but the lack of standardization regularly causes unintended breaking changes, and developing a competing-but-compatible type checker is basically impossible.)
TypeScript has such a rich type system that lets you do some crazy things, many of which allow you to have a _very_ ergonomic dev UX while maintaining compile time type safety.
[0]: https://type-level-typescript.com/
[0]: https://medium.com/free-code-camp/typescript-curry-ramda-typ...
[1]: https://github.com/millsp/ts-toolbelt
I bought it based on your recommendation, and I'm happy I did. It reminds me of Josh Comeau's articles, but for advanced TypeScript.
> Any application that can be written in JavaScript, will eventually be written in TypeScript types
There is no compiler error when he compiles an unsolvable input. But when there is a solution, the compiler provides it:
``` Error: This match case could not be refuted. Here is an example of a value that would reach it: Grid (A, B, C, D, C, D, A, B, B, A, D, C, D, C, B, A) ```
They could have done exactly the same in JSON instead. Or using arrays like in LISP.
Cool project tho, but it is a very misleading explanation. Or did I miss something?
It reminds me of why I like Haskell, in particular the last exercise on this page: http://learnyouahaskell.com/starting-out#im-a-list-comprehen...
In which you solve a problem declaratively by leveraging Haskell laziness.