Ha! More performant than I'd have guessed. I tried commenting `PrintBoard<EvolveN<GosperGliderGun, 100>>` in and out and it took about 3 seconds (in the ts playground).
Because it's all just types, there's nothing _to_ run. Instead, you'll want to hover your cursor over the `PGunX` types at the end of the file in the playground; this will cause the TS editor to compute that type and it should display a string corresponding to the board state.
In the typescript playground, the best way to see the output of any evolution number is to have it autocomplete a string literal!
Uncomment one of the PGunXX types that you want to see, then below it type this:
const boardstr: PGun10 = ``;
Then put the cursor inside the two backticks and press Control+Space for intellisense autocomplete, and press enter on the first entry there. Then intellisense will put the computed board into a string literal, looking like:
You can also use twoslash[1] caret comments in the playground to display type representations inline, even for uninitialized/declared values, so eg something like this should work:
Any sufficiently capable type system will make it possible to implement a form of functional programming.
These advanced type systems are essentially a form of pre-compile time scripting to assert certain guarantees about user defined types. It's the same mechanism that makes C++ templates turing complete.
In the case of TypeScript, most of the magic and crazy hacks are dependent on Template Literal Types [0], which is what allows inference based on arbitrary strings. Once you have that abstraction, you can just keep adding complexity to it.
Thanks. The Shen language takes this to its logical conclusion (pun intended) and implements a fully Turing complete type system. Types are specified with sequents which are essentially Prolog relations using a slightly different notation.[1]
Typescript has conditional types, which means it can be used as a programming language itself. In theory you can write any arbitrary program - game of life is just an example. You have to define numbers and arithmetics from scratch though, so it is not very practical.
Conditional types are probably rarely used in practial code, but it opens the door for a lot of geekery.
It's just a demonstration of how to encode the transition rules for Conway's game of life as a set of types, aka logical constraints. TypeScript's type system has unification, same as in Prolog, and since Prolog is basically Turing complete so is TypeScript's type system.
this is exactly what I want from the Types as Comments proposal[0] as I think it's the only way that types can feasibly become part of the language. It's hard to imagine how all of the concepts TS introduces via special syntax can be covered otherwise.
That is a great idea. It also crystalizes the syntax so organisations other than MS can invest in building tooling as the target wont be as fast moving.
That proposal aims to allow type annotations as part of JS, but to do that the parser needs to know when a type annotation starts (easy) and ends (hard), the only realistic ways that can be done at the moment is explicitly supporting all of the syntax TS introduces (which is bad for other type checkers) or restricting to a limited subset which would mean a lot of what TS supports would not be allowed, negating the usefulness of the proposal.
What I'm saying is that if instead we said that all type annotations must follow existing JS grammar rules, with perhaps a couple of small additions, then we'd be able to support all sorts of complex type annotations in JS directly, using existing syntax. This would mean that TS's grammar would end up changing a bit, but that's a small price to pay for ongoing interoperability.
For example, instead of
type UserProperties = keyof typeof User;
which is tied to TS's arbitrary syntax, and not supported in Flow, use
I recently had the insight- surely induced by reading something on HN or listening to some podcast- that types are simply functions from the set of all possible "values" to a logical value...
Yeah, a type is really just a set (in the mathematical sense). And a set can be defined by a function to {0, 1}. I don’t know if this function has a formal name, byt you can think of it as a “is this value a member of the set?” function.
Love it! Reminds me of the hilarious "Typing the technical interview" [1] and "Typescripting the technical interview" [2], a couple of my favorite blog posts of all time.
47 comments
[ 4.6 ms ] story [ 119 ms ] threadAny sufficiently advanced type system is indistinguishable from an interpreter!
[1] https://www.destroyallsoftware.com/talks/the-birth-and-death...
Playground: https://www.typescriptlang.org/play?#code/PTAEHkCUEkHFoHIEEA...
Uncomment one of the PGunXX types that you want to see, then below it type this:
Then put the cursor inside the two backticks and press Control+Space for intellisense autocomplete, and press enter on the first entry there. Then intellisense will put the computed board into a string literal, looking like:These advanced type systems are essentially a form of pre-compile time scripting to assert certain guarantees about user defined types. It's the same mechanism that makes C++ templates turing complete.
[0] https://www.typescriptlang.org/docs/handbook/2/template-lite...
If feeling adventurous, read e.g. https://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=...
that's a great quote.
1: https://shenlanguage.org/OSM/Recursive.html
IIRC the type checker is literally a Prolog.
Conditional types are probably rarely used in practial code, but it opens the door for a lot of geekery.
In college I did it in assembler (a couple hundred bytes of code) on a PDP11/34 and displayed the results on an oscilloscope screen :)
https://github.com/microsoft/TypeScript/issues/14833
type MyType<T> = someFunc(T)
Of course these functions might be typed too…
[0] https://tc39.es/proposal-type-annotations
What I'm saying is that if instead we said that all type annotations must follow existing JS grammar rules, with perhaps a couple of small additions, then we'd be able to support all sorts of complex type annotations in JS directly, using existing syntax. This would mean that TS's grammar would end up changing a bit, but that's a small price to pay for ongoing interoperability.
For example, instead of
which is tied to TS's arbitrary syntax, and not supported in Flow, use[0] https://aphyr.com/posts/342-typing-the-technical-interview
[1] https://www.richard-towers.com/2023/03/11/typescripting-the-...
https://aphyr.com/posts/353-rewriting-the-technical-intervie...
If anyone else is interested in an internship or full-time position in typescript: https://www.uncountable.com/hiring/hn