11 ms·

Playing Sudoku in TypeScript while the type checker highlights mistakes

229 points by mjcurl 2y ago

paradite 2y ago
Ok can we reduce sudoku to something Turing complete and hence prove TypeScript is Turing complete?
- itishappy 2y ago
  Issue #14833 - TypeScripts Type System is Turing Complete https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833
  - brap 2y ago
    Does this mean that some types never get resolved? How does the type checker handle that?
    - anamexis 2y ago
      Indeed, the link gives an example of such an infinitely recursive type: type Foo<T extends "true", B> = { "true": Foo<T, Foo<T, B>> }[T]; let f: Foo<"true", {}> = null!; As for how it's handled, it yields the error "Type instantiation is excessively deep and possibly infinite. [2589]" I'm not sure what the max stack depth is, though.
- School-Cotton 2y ago
  Checking a sudoku board always terminates, so no.
davidsgk 2y ago
An amazing (if a bit flowery) read that highlights more arcane stuff you can do with the TS type system: https://www.richard-towers.com/2023/03/11/typescripting-the-technical-interview.html https://www.richard-towers.com/2023/03/11/typescripting-the-...
- egKYzyXeIL 2y ago
  That was fantastic! The end got me good.
a_wild_dandan 2y ago
Using TypeScript for the entire stack feels like a superpower. The type system is incredible. V8 is fast. The frameworks are phenomenal (Next.js, Material UI, etc). The ecosystem is enormous, with packages for everything. The unified codebases save gobs of duplicate code (e.g. ferrying data betwixt client/server). I'm not surprised that such an expressive system can play Sudoku!
- sva_ 2y ago
  > with packages for everything Which can quickly turn into a crutch if you're not wise about it
  - brigadier132 2y ago
    One thing I do when I see a dependency I want to use is get its github and paste it in this site: https://codetabs.com/count-loc/count-loc-online.html https://codetabs.com/count-loc/count-loc-online.html Depending on the # of lines of code and how many people use it actively I decide between just * forking it and using the fork as a dependency * copying the parts i need from it * or just using it as a dependency Either way, the dependencies existing is just a boon. Even if you don't want to depend on it directly you can use the existing work as a guide and implement something yourself.
- leononame 2y ago
  For me, it's the opposite. The type system is decent, but it's generics can get extremely out of hand, it's not sound, and I run into weird type errors with libraries more often than not. Having no integer types (ok, this isn't something typescript could just implement) other than BigInt is another big one for me. That you can just do `as unknown as T` is an endless source of pain and sometimes it doesn't help that JS just does whatever it wants with type coercion. I've seen React libraries with number inputs that actually returned string values in their callbacks, but you wouldn't notice this until you tried doing addition and ended up with concatenation. Have fun finding out where your number turned into a string. The number of times I've read `... does not exist on type undefined` reaches trauma-inducing levels. TypeScript is as good as it can get for being a superset of JS. But it's not a language I have fun writing stuff in (and I even fear it on the backend). It has its place, and it's definitely a decent language, but I would choose something else for frontend if I could, and wouldn't use it on the backend at all. I somehow don't trust it. I know people write amazing software with it, but YMMV I guess.
samwillis 2y ago
This is super cool, love these sort of projects. It's crazy what you can achieve with typescript types, what about inferring sql query results types from a raw sql query string: https://github.com/nikeee/sequelts https://github.com/nikeee/sequelts
umvi 2y ago
(completely serious) I think soon TS is going to need a "type debugger" where you can set breakpoints and step through tsc as it propagates your type info through generics and conditionals and such Otherwise it's just nightmarish to try to debug ultra complex types
- sherburt3 2y ago
  Learning the more advanced features of typescript is one of the worst things that's happened to my productivity. I keep wasting hours making a hyper specific type when in reality `{ [K: string]: string }` probably would have worked just fine.
- jmeyer2k 2y ago
  To debug, I just do `type asdf = Whatever<Generics, You, Want>` then mouse over `asdf`.
- bubblyworld 2y ago
  This would be fantastic, I agree - specifically the interaction between generic constraints and conditionals has bitten me so many times.
beckford 2y ago
> The goal is that we can play Sudoku in TypeScript while the type checker complains about mistakes. This is not about implementing a Sudoku solver. That goal could be extended to implement a Sudoku solver in the type system. One such solver was described at https://ocamlpro.com/blog/2017_04_01_ezsudoku/ https://ocamlpro.com/blog/2017_04_01_ezsudoku/ for OCaml. TLDR: Your compiler can report the solution as an error message if your language supports refutation and has enough type machinery to accurately model Sudoku. Having said that, I don’t think a Sudoku solver implementation embedded in a type system is practical (maybe fun for educational purposes though!)
prologist11 2y ago
Any sufficiently advanced type system is indistinguishable from Prolog.
peeters 2y ago
> This is not about implementing a Sudoku solver If you can capture validity of the game state in the type system, a sufficiently advanced IDE with autocomplete/intellisense could actually already be a naive solver, since they will tend to treat contextual autocomplete as a form of constraint satisfiability problem, which is a sufficient approach to solve easy Sudokus. In other words, throw this into Webstorm, put your cursor in an empty cell that currently has only one possible answer, and hit ctrl-space, and I would expect it to automatically fill in the answer for you.
rafram 2y ago
This is a good illustration of one of the perils of TypeScript, in a funny way. It’s easy to get lost writing a complex verifier for your model using the fantastic type system… and then wake up the next morning and remember that at some point you’ll need to actually implement the logic. And you’ll probably give up and end it with `return result as unknown as ComplexVerifierType<A, B, C>` anyway.

229 points by mjcurl 2y ago

paradite 2y ago

Ok can we reduce sudoku to something Turing complete and hence prove TypeScript is Turing complete?

itishappy 2y ago
Issue #14833 - TypeScripts Type System is Turing Complete https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833
- brap 2y ago
  Does this mean that some types never get resolved? How does the type checker handle that?
  - anamexis 2y ago
    Indeed, the link gives an example of such an infinitely recursive type: type Foo<T extends "true", B> = { "true": Foo<T, Foo<T, B>> }[T]; let f: Foo<"true", {}> = null!; As for how it's handled, it yields the error "Type instantiation is excessively deep and possibly infinite. [2589]" I'm not sure what the max stack depth is, though.
School-Cotton 2y ago
Checking a sudoku board always terminates, so no.

davidsgk 2y ago

An amazing (if a bit flowery) read that highlights more arcane stuff you can do with the TS type system: https://www.richard-towers.com/2023/03/11/typescripting-the-technical-interview.html https://www.richard-towers.com/2023/03/11/typescripting-the-...

egKYzyXeIL 2y ago
That was fantastic! The end got me good.

a_wild_dandan 2y ago

Using TypeScript for the entire stack feels like a superpower. The type system is incredible. V8 is fast. The frameworks are phenomenal (Next.js, Material UI, etc). The ecosystem is enormous, with packages for everything. The unified codebases save gobs of duplicate code (e.g. ferrying data betwixt client/server). I'm not surprised that such an expressive system can play Sudoku!

sva_ 2y ago
> with packages for everything Which can quickly turn into a crutch if you're not wise about it
- brigadier132 2y ago
  One thing I do when I see a dependency I want to use is get its github and paste it in this site: https://codetabs.com/count-loc/count-loc-online.html https://codetabs.com/count-loc/count-loc-online.html Depending on the # of lines of code and how many people use it actively I decide between just * forking it and using the fork as a dependency * copying the parts i need from it * or just using it as a dependency Either way, the dependencies existing is just a boon. Even if you don't want to depend on it directly you can use the existing work as a guide and implement something yourself.
leononame 2y ago
For me, it's the opposite. The type system is decent, but it's generics can get extremely out of hand, it's not sound, and I run into weird type errors with libraries more often than not. Having no integer types (ok, this isn't something typescript could just implement) other than BigInt is another big one for me. That you can just do `as unknown as T` is an endless source of pain and sometimes it doesn't help that JS just does whatever it wants with type coercion. I've seen React libraries with number inputs that actually returned string values in their callbacks, but you wouldn't notice this until you tried doing addition and ended up with concatenation. Have fun finding out where your number turned into a string. The number of times I've read `... does not exist on type undefined` reaches trauma-inducing levels. TypeScript is as good as it can get for being a superset of JS. But it's not a language I have fun writing stuff in (and I even fear it on the backend). It has its place, and it's definitely a decent language, but I would choose something else for frontend if I could, and wouldn't use it on the backend at all. I somehow don't trust it. I know people write amazing software with it, but YMMV I guess.

samwillis 2y ago

This is super cool, love these sort of projects. It's crazy what you can achieve with typescript types, what about inferring sql query results types from a raw sql query string: https://github.com/nikeee/sequelts https://github.com/nikeee/sequelts

umvi 2y ago

(completely serious) I think soon TS is going to need a "type debugger" where you can set breakpoints and step through tsc as it propagates your type info through generics and conditionals and such Otherwise it's just nightmarish to try to debug ultra complex types

sherburt3 2y ago
Learning the more advanced features of typescript is one of the worst things that's happened to my productivity. I keep wasting hours making a hyper specific type when in reality `{ [K: string]: string }` probably would have worked just fine.
jmeyer2k 2y ago
To debug, I just do `type asdf = Whatever<Generics, You, Want>` then mouse over `asdf`.
bubblyworld 2y ago
This would be fantastic, I agree - specifically the interaction between generic constraints and conditionals has bitten me so many times.

beckford 2y ago

> The goal is that we can play Sudoku in TypeScript while the type checker complains about mistakes. This is not about implementing a Sudoku solver. That goal could be extended to implement a Sudoku solver in the type system. One such solver was described at https://ocamlpro.com/blog/2017_04_01_ezsudoku/ https://ocamlpro.com/blog/2017_04_01_ezsudoku/ for OCaml. TLDR: Your compiler can report the solution as an error message if your language supports refutation and has enough type machinery to accurately model Sudoku. Having said that, I don’t think a Sudoku solver implementation embedded in a type system is practical (maybe fun for educational purposes though!)

prologist11 2y ago

Any sufficiently advanced type system is indistinguishable from Prolog.

peeters 2y ago

> This is not about implementing a Sudoku solver If you can capture validity of the game state in the type system, a sufficiently advanced IDE with autocomplete/intellisense could actually already be a naive solver, since they will tend to treat contextual autocomplete as a form of constraint satisfiability problem, which is a sufficient approach to solve easy Sudokus. In other words, throw this into Webstorm, put your cursor in an empty cell that currently has only one possible answer, and hit ctrl-space, and I would expect it to automatically fill in the answer for you.

rafram 2y ago

This is a good illustration of one of the perils of TypeScript, in a funny way. It’s easy to get lost writing a complex verifier for your model using the fantastic type system… and then wake up the next morning and remember that at some point you’ll need to actually implement the logic. And you’ll probably give up and end it with `return result as unknown as ComplexVerifierType<A, B, C>` anyway.