Show HN: Conway's Game of Life in TypeScript's type system | Hacker News Reader

Show HN: Conway's Game of Life in TypeScript's type system

github.com

186 pointscandleknight45 comments

TypeScript playground: https://www.typescriptlang.org/play?#code/KYDwDg9gTgLgBDAnmY...

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:

    const boardstr: PGun10 = `............................................
    ........................xx..................
    ........................x..x................
    ..........x.x...............x......xx.......
    ........x...x..xxx..........x......xx.......
    .xx.....x...................x...............
    .xx....x....x.......xx..x..x................
    ........x.......x.x..x..xx..................
    ........x...x.....xxx.......................
    ..........x.x...............................
    ............................................`;

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:

  declare const boardstr: PGun10
  //            ^?

1: https://www.npmjs.com/package/@typescript/twoslash

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.

[0] https://aphyr.com/posts/342-typing-the-technical-interview

[1] https://www.richard-towers.com/2023/03/11/typescripting-the-...

I think you have an off-by-one error there!

Just a ui bug, the presentation layer doesn’t match the data layer

Don't forget "Rewriting the technical interview":

https://aphyr.com/posts/353-rewriting-the-technical-intervie...

Sometimes I think I don't understand TypeScript's type system and then I see something like this and I realize I know even less than I thought

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.

[0] https://www.typescriptlang.org/docs/handbook/2/template-lite...

Any sufficiently advanced type system is indistinguishable from Prolog.

Note to readers: if the author’s username doesn’t make it obvious, it’s funny because is true.

If feeling adventurous, read e.g. https://lpn.swi-prolog.org/lpnpage.php?pagetype=html&pageid=...

commenting for future reference.

that's a great quote.

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]

1: https://shenlanguage.org/OSM/Recursive.html

Yes! I have played with Shen before.

IIRC the type checker is literally a Prolog.

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.

We’re using conditional types for type inference in garph (https://garph.dev)

It is year 2035. TypeScript type system gained conscious.

Considering that in 2035 all software runs on top of JavaScript [1], I'm not surprised.

[1] https://www.destroyallsoftware.com/talks/the-birth-and-death...

Nice work, Ruyi! You've definitely taken typescript mastery to a new level. It was great to have you intern with us.

If anyone else is interested in an internship or full-time position in typescript: https://www.uncountable.com/hiring/hn

Stop overcalculating a mess out of junk, learn Rust and see what a Typesystem should and shouldn't have to do.

Cute :)

Any sufficiently advanced type system is indistinguishable from an interpreter!

=> turing completeness

You can also easily implement meta-languages. Eg. lambda calculus: https://github.com/desi-ivanov/ts-lambda-calc

How do I run this/see the results? I'm a little lost.

Same here. I hit "run" but get an error

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.

At this point, TypeScript should just let us define types using plain imperative TS code that will execute during static analysis. Might as well.

type MyType<T> = someFunc(T)

Of course these functions might be typed too…

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.

[0] https://tc39.es/proposal-type-annotations

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.

I mean this seems like a nice proposal, but I guess I’m missing something, how does it relate to my comment?

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

    type UserProperties = keyOf(typeOf(User));

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.

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).

the power of tail call optimization :)

SO many ways.

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 :)

It can do a Y Combinator with types can't it?

Yes: https://gist.github.com/forivall/a80d382b8c399044eb7d45d9124...

Playground: https://www.typescriptlang.org/play?#code/PTAEHkCUEkHFoHIEEA...

I'm happy to see people learning the Curry–Howard isomorphism the fun way.

I though I knew TypeScript pretty well, but I can barely read that.

I'm really confused, is it what TS is supposed to looks like?

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.

TypeScripts Type System is Turing Complete #14833

https://github.com/microsoft/TypeScript/issues/14833

This is probably the slowest Game of Life ever.

I like having type hints, I really do- but I've definitely been on projects where TS began to feel a lot like a nerd snipe https://xkcd.com/356/

Reply on news.ycombinator.com