https://github.com/gruhn/typescript-sudoku Skip to content Navigation Menu Toggle navigation Sign in * Product + Actions Automate any workflow + Packages Host and manage packages + Security Find and fix vulnerabilities + Codespaces Instant dev environments + GitHub Copilot Write better code with AI + Code review Manage code changes + Issues Plan and track work + Discussions Collaborate outside of code Explore + All features + Documentation + GitHub Skills + Blog * Solutions By size + Enterprise + Teams + Startups By industry + Healthcare + Financial services + Manufacturing By use case + CI/CD & Automation + DevOps + DevSecOps * Resources Topics + AI + DevOps + Security + Software Development + View all Explore + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Enterprise + Enterprise platform AI-powered developer platform Available add-ons + Advanced Security Enterprise-grade security features + GitHub Copilot Enterprise-grade AI features + Premium Support Enterprise-grade 24/7 support * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up Reseting focus You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} gruhn / typescript-sudoku Public * Notifications You must be signed in to change notification settings * Fork 1 * Star 202 Playing Sudoku in TypeScript while the type checker highlights mistakes. 202 stars 1 fork Branches Tags Activity Star Notifications You must be signed in to change notification settings * Code * Issues 0 * Pull requests 0 * Actions * Projects 0 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Actions * Projects * Security * Insights gruhn/typescript-sudoku This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository. master BranchesTags Go to file Code Folders and files Name Name Last commit Last commit message date Latest commit History 31 Commits .editorconfig .editorconfig .envrc .envrc .gitignore .gitignore README.md README.md deno.lock deno.lock flake.lock flake.lock flake.nix flake.nix generate_sudoku_v1.ts generate_sudoku_v1.ts intersect_never.png intersect_never.png intersect_unknown.png intersect_unknown.png package-lock.json package-lock.json package.json package.json sudoku_v1.ts sudoku_v1.ts sudoku_v1_demo.png sudoku_v1_demo.png sudoku_v2.ts sudoku_v2.ts sudoku_v2_demo.gif sudoku_v2_demo.gif type-hierarchie.png type-hierarchie.png View all files Repository files navigation * README TypeScript Sudoku This is an experiment to precisely define a Sudoku type. 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. Just about writing unnecessarily complicated type definitions. For the final result, check out sudoku_v2.ts. demo video: final approach As a first approximation we can define the type as an array of numbers: type Sudoku = number[] This permits all valid Sudokus, but also allows many invalid Sudokus. const invalidSudoku: Sudoku = [ -1, 7.5, 9, 9 ] First, all array elements have to be integers in the range 1 to 9. Second, Sudokus are 9-by-9 grids so we need an array with exactly 81 elements. That's easy enough: type Cell = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 type Sudoku = [ Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, Cell, ] But the interesting part is: how do we enforce the Sudoku rules? Currently, this still type checks: const invalidSudoku: Sudoku = [ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ] We have to make sure that * all rows are duplicate free, * all columns are duplicate free and * each of the 3-by-3 squares is also duplicate free. For simplicity, let's just consider a 3-cell Sudoku for now: type BabySudoku = [ Cell, Cell, Cell ] How can we require that the three cells all have different values? The definition of a cell is dependent on other cells, so we need a way to reference individual cells. By introducing a type parameter for every cell, we can refer to cells by name: type BabySudoku = [ X1, X2, X3 ] Guess how many parameters the full 9-by-9 Sudoku needs. A problem is, we have to instantiate these type parameters when we create BabySudoku values: const s: BabySudoku<1, 2, 3> = [ 1, 2, 3 ] This is redundant. The type parameters should get inferred from the value. Type parameters on functions are automatically inferred: const func = (val: T) => val func("hello") // type parameter can be provided ... func("hello") // ... but not necessary So as a workaround we can define the type in the argument of some dummy function: const babySudoku = ( grid: [ X1, X2, X3 ] ) => grid With that we can construct Sudokus, without instantiating type parameters: const s = babySudoku([1, 2, 3]) The runtime behavior of babySudoku is boring. It just returns it's argument unchanged (aka. the identity function). This is a bit awkward but I haven't found a better way so far. Constraints using Exclude We still need to ensure that all cells are different. One way to do it, is with the built-in utility type Exclude. const babySudoku = < X1 extends Cell, X2 extends Cell, X3 extends Cell >( grid: [ Exclude, Exclude, Exclude, ] ) => grid This works! What's particularly nice about this approach is that the type checker highlights exactly the cells that are in conflict: demo: first approach A downside is that the full type definition is very large. For each cell we have to explicitly list the other cells that are required to be different. Writing that out manually is tedious. I ended up creating a script just to print out the type definition. I came up with another approach that is more complex but also more flexible. Before we can talk about that we need to talk about the types unknown and never. Interlude: unknown and never never is the empty type, making it a subtype of everything. There is no value that has type never. So you always get a type error no matter what you write on the right-hand side of const value: never = ???. That is, unless the assignment is unreachable or you use some malicous type cast like: const value: never = "obviously not never" as never never is useful to strategically provoke a type error. The plan is to formulate the Sudoku type in such a way, that it is equal to never IF constraints are violated. unknown is a supertype of everything, similar to any (What's the difference between unknown and any?). type hierarchie I find it useful to think of unknown and never as type-level analogs of true and false. In combination with unknown and never, union types (A | B) and intersection types (A & B) behave just like boolean OR (a || b) and boolean AND (a && b). Notice the syntactic similarity of these operators. For example, unknown | never is the same as unknown, because building the union of absolutely-everything and absolutely-nothing gives back absolutely-everything. Analogously, true || false is true. Let's define type aliases, to make the relationship more obvious: type True = unknown type False = never With that we have: Term-level Type-level true && true is true True & True is True true && false is false True & False is False true || false is true True | False is True false || false is false False | False is False ... ... Now that we can talk about booleans on the type-level, we can formulate arbitrary boolean constraints inside type definitions. Constraints using Type-Level Predicates The plan is to come up with some type-level boolean expression that describes the Sudoku constraints. Again, let's stick to a 3-cell grid for now, where all cells have to be different. We want a to define a type type CheckSudokuConstraints = ??? // "returns" either `unknown` or `never` At this point we can think of CheckSudokuConstraints as a function that returns true or false (aka. a predicate). An analogous term-level function would look like this: function checkSudokuConstraints(x1: Cell, x2: Cell, x3: Cell): boolean { return ??? } Once we know how to define CheckSudokuConstraints we build the intersection with the actual number grid: [ X1, X2, X3 ] & CheckSudokuConstraints IF some Sudoku constraint is violated, then CheckSudokuConstraints "returns" never and we get: [ X1, X2, X3 ] & never // ==> never The intersection with absolutely-nothing is always absolutely-nothing again, so the whole definition "collapses" down to never. Venn diagram: never intersection IF all Sudoku constraint are satisfied, then CheckSudokuConstraints "returns" unknown and we get: [ X1, X2, X3 ] & unknown // ==> [ X1, X2, X3 ] The intersection with unknown just leaves the left-hand side alone. Venn diagram: unknown intersection Defining CheckSudokuConstraints First we need a type-level predicate to compare two cells. We can use conditional types to check if two types are equal: type Equal = A extends B ? (B extends A ? unknown : never) : never // Equal<3, 3> ==> unknown // Equal<3, 4> ==> never If A is a subtype of B and B is a subtype of A, then A and B must be the same type. Thus, we return true (i.e. unknown). Otherwise, we return false (i.e. never). By negating the logic, we get a type-level predicate that tells us when two cells are different: type Different = A extends B ? (B extends A ? never : unknown) : unknown // Different<3, 3> ==> never // Different<3, 4> ==> unkown To express that a bunch of cells are all different, we can go through all pairs. Again, read the intersection type operator (&) just like boolean AND: Different & Different & Different & Different & Different & Different Actually, Different is symmetric, i.e. Different and Different are the same, so we can skip half the pairs: Different & Different & Different And that's already the definition of CheckSudokuConstraints if we only have three cells: type CheckSudokuConstraints = Different & Different & Different For the full 81-cell Sudoku, the number of cells to compare is getting a bit out of hand. We want to express that the cells in each row, each column and each square are pairwise different. Rows, columns and squares always have exactly 9 cells. So we can define one more utility type that just checks pairwise difference of 9 arbitrary given cells: type AllDifferent = Different & Different & Different & Different & Different & Different & ... Finally, we can define CheckSudokuConstraints for the full Sudoku: type CheckSudokuConstraints< X11, X12, X13, X14, X15, X16, X17, X18, X19, X21, X22, X23, X24, X25, X26, X27, X28, X29, X31, X32, X33, X34, X35, X36, X37, X38, X39, X41, X42, X43, X44, X45, X46, X47, X48, X49, X51, X52, X53, X54, X55, X56, X57, X58, X59, X61, X62, X63, X64, X65, X66, X67, X68, X69, X71, X72, X73, X74, X75, X76, X77, X78, X79, X81, X82, X83, X84, X85, X86, X87, X88, X89, X91, X92, X93, X94, X95, X96, X97, X98, X99, > = // all 9 rows & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent // all 9 columns & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent & AllDifferent // three upper squares & AllDifferent & AllDifferent & AllDifferent // three center squares & AllDifferent & AllDifferent & AllDifferent // three lower squares & AllDifferent & AllDifferent & AllDifferent Incomplete Sudokus Until now we have only described complete Sudokus, where every cell is already filled with an integer. To actually play Sudoku, we need to allow empty cells. For that we pick some dummy value to represent an empty cell. This can be anything, as long as it's not a number from 1 to 9: const _ = "empty cell" type EmptyCell = typeof _ Now we could redefine Cell to include this value: type Cell = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | EmptyCell // won't work But then the constraints also apply to empty cells and the type checker starts complaining about things like two empty cells in the same row. Empty cells should be unconstrained and allowed everywhere. We can do that by explicitly annotating each cell with | EmptyCell: [ X1 | EmptyCell, X2 | EmptyCell, X3 | EmptyCell ] & CheckSudokuConstraints So in each cell we either allow an empty cell or we allow an integer from 1-9 that is additionally constrained. For the full type definition, check out sudoku_v2.ts. Conclusion This is pretty useless. One could try to implement a statically verified Sudoku solver based on these types: function solveSudoku(grid: IncompleteSudoku): CompleteSudoku { /* ... */ } This would give very high confidence in the implementations correctness. However, it's probably hard to convince the type checker that the code really matches the spec. Even then, error messages are not very friendly and, depending on the TypeScript version, it can take multiple seconds to type check the code. Nevertheless, I think it's interesting to see how much expressivity one can squeeze out of the type system. About Playing Sudoku in TypeScript while the type checker highlights mistakes. Topics typescript type-theory sudoku Resources Readme Activity Stars 202 stars Watchers 2 watching Forks 1 fork Report repository Releases No releases published Packages 0 No packages published Languages * TypeScript 97.5% * Nix 2.5% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.