4 ms·
> 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
by 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!)