As you may have noticed, on the begining of April I have some urge to write something technical about some deeply specific point of OCaml. This time I'd like to tackle that through sudoku.
It appeard that Sudoku is of great importance considering the number of posts explaining how to write a solver. Following that trend I will explain how to write one in OCaml. But with a twist.
We will try to optimize it. I won't show you anything as obvious as how to micro-optimize your code or some smart heuristc. No we are not aiming for being merely algorithmically good. We will try to make something serious, we are want it to be solved even before the program starts.
Yes really. Before. And I will show you how to use a feature of OCaml 4.03 that is sadly not well known.
First of all, as we do like type and safe programs, we will define what a well formed sudoku solution looks like. And by defining of course I mean declaring some GADTs with enough constraints to ensure that only well correct solutions are valid.
I assume tha you know the rules of Sudoku and will refrain from infuriating you by explaining it. But we will still need some vocabulary.
So the aim of sudoku is to fill a 'grid' with 'symbols' satisfying some 'row' 'column' and 'square' constraints.
To make the code examples readable we will stick to
4*4 sudokus. It's the smallest size that behaves the same way as
9*9 ones (I considered going for
1*1 ones, but the article ended up being a bit short). Of course everything would still apply to any
n^2*n^2 sized one.
So let's start digging in some types. As we will refine them along the way, I will leave some parts to be filled later. This is represented by '...' .
First there are symbols, just 4 of them befause we reduced the size. Nothing special about that right now.
type ... symbol = | A : ... | B : ... | C : ... | D : ...
And a grid is 16 symbols. To avoid too much visual clutter in the type I just put them linearly. The comment show how it is supposed to be seen in the 2d representation of the grid:
(* a b c d e f g h i j k l m n o p *) type grid = Grid : ... symbol * (* a *) ... symbol * (* b *) ... symbol * (* c *) ... symbol * (* d *) ... symbol * (* e *) ... symbol * (* f *) ... symbol * (* g *) ... symbol * (* h *) ... symbol * (* i *) ... symbol * (* j *) ... symbol * (* k *) ... symbol * (* l *) ... symbol * (* m *) ... symbol * (* n *) ... symbol * (* o *) ... symbol (* p *) -> solution
Right now grid is a simple 16-uple of symbols, but we will soon start filling those '...' to forbid any set of symbols that is not a valid solution.
Each constraint looks like, 'among those 4 positions neither 2 symbols are the same'. To express that (in fact something equivalent but a bit simpler to state with our types), we will need to name positions. So let's introduce some names:
type r1 (* the first position among a row constraint *) type r2 (* the second position among a row constraint *) type r3 type r4 type c1 (* the first position among a column constraint *) type c2 type c3 type c4 type s1 type s2 type s3 type s4 type ('row, 'column, 'square) position
On the 2d grid this is how the various positions will be mapped.
r1 r2 r3 r4 r1 r2 r3 r4 r1 r2 r3 r4 r1 r2 r3 r4 c1 c1 c1 c1 c2 c2 c2 c2 c3 c3 c3 c3 c4 c4 c4 c4 s1 s2 s1 s2 s3 s4 s3 s4 s1 s2 s1 s2 s3 s4 s4 s4
For instance, the position g, in the 2nd row, 3rd column, will at the 3rd position in its row constraint, 2nd in its column constraint, and 3rd in its square constraint:
type g = (r3, c2, s3) position
We could have declare a single constraint position type, but this is slightly more readable. than:
type g = (p3, p2, p3) position
The position type is phantom, we could have provided a representation, but since no value of this type will ever be created, it's less confusing to state it that way.
type a = (r1, c1, s1) position type b = (r2, c1, s2) position type c = (r3, c1, s1) position type d = (r4, c1, s2) position type e = (r1, c2, s3) position type f = (r2, c2, s4) position type g = (r3, c2, s3) position type h = (r4, c2, s4) position type i = (r1, c3, s1) position type j = (r2, c3, s2) position type k = (r3, c3, s1) position type r = (r4, c3, s2) position type m = (r1, c4, s3) position type n = (r2, c4, s4) position type o = (r3, c4, s3) position type p = (r4, c4, s4) position
It is now possible to state for each symbol in which position it is, so we will start filling a bit those types.
type ('position, ...) symbol = | A : (('r, 'c, 's) position, ...) symbol | B : (('r, 'c, 's) position, ...) symbol | C : (('r, 'c, 's) position, ...) symbol | D : (('r, 'c, 's) position, ...) symbol
This means that a symbol value is then associated to a single position in each constraint. We will need to state that in the grid type too:
type grid = Grid : (a, ...) symbol * (* a *) (b, ...) symbol * (* b *) (c, ...) symbol * (* c *) (d, ...) symbol * (* d *) (e, ...) symbol * (* e *) (f, ...) symbol * (* f *) (g, ...) symbol * (* g *) (h, ...) symbol * (* h *) (i, ...) symbol * (* i *) (j, ...) symbol * (* j *) (k, ...) symbol * (* k *) (l, ...) symbol * (* l *) (m, ...) symbol * (* m *) (n, ...) symbol * (* n *) (o, ...) symbol * (* o *) (p, ...) symbol (* p *) -> solution
We just need to forbid a symbol to appear in two different positions of a given row/column/square to prevent invalid solutions.
type 'fields row constraint 'fields = < a : 'a; b : 'b; c : 'c; d : 'd > type 'fields column constraint 'fields = < a : 'a; b : 'b; c : 'c; d : 'd > type 'fields square constraint 'fields = < a : 'a; b : 'b; c : 'c; d : 'd >
Those types represent the statement 'in this line/column/square, the symbol a is at the position 'a, the symbol b is at the position 'b, ...'
For instance, the row 'A D B C' will be represented by
< a : l1; b : l3; c : l4; d : l2 > row
Which reads: 'The symbol A is in first position, B in third position, C in fourth, and D in second'
The object type is used to make things a bit lighter later and allow to state names.
Now the symbols can be a bit more annotated:
type ('position, 'row, 'column, 'square) symbol = | A : (('r, 'c, 's) position, < a : 'r; .. > row, < a : 'c; .. > column, < a : 's; .. > square) symbol | B : (('r, 'c, 's) position, < b : 'r; .. > row, < b : 'c; .. > column, < b : 's; .. > square) symbol | C : (('r, 'c, 's) position, < c : 'r; .. > row, < c : 'c; .. > column, < c : 's; .. > square) symbol | D : (('r, 'c, 's) position, < d : 'r; .. > row, < d : 'c; .. > column, < d : 's; .. > square) symbol
Notice that '..' is not '...'. Those dots are really part of the OCaml syntax: it means 'put whatever you want here, I don't care'. There is nothing more to add to this type.
This type declaration reports the position information. Using the same variable name 'r in the position and in the row constraint parameter for instance means that both fields will have the same type.
For instance, a symbol 'B' in position 'g' would be in the 3rd position of its row, 2nd position of its column , and 3rd position of its square:
let v : (g, _, _, _) symbol = B;; val v : (g, < b : r3 > row, < b : c2 > column, < b : s3 > square) symbol = B
Those types constraints ensure that this is correctly reported.
The real output of the type checker is a bit more verbose, but I remove the irrelevant part:
val v : (g, < a : 'a; b : r3; c : 'b; d : 'c > row, < a : 'd; b : c2; c : 'e; d : 'f > column, < a : 'g; b : s3; c : 'h; d : 'i > square) symbol = B
We are now quite close from a completely constrained type. We just need to say that the various symbols from the same row/line/column constraint have the same type:
type grid = Grid : (a, 'row1, 'column1, 'square1) symbol * (b, 'row1, 'column2, 'square1) symbol * (c, 'row1, 'column3, 'square2) symbol * (d, 'row1, 'column4, 'square2) symbol * (e, 'row2, 'column1, 'square1) symbol * (f, 'row2, 'column2, 'square1) symbol * (g, 'row2, 'column3, 'square2) symbol * (h, 'row2, 'column4, 'square2) symbol * (i, 'row3, 'column1, 'square3) symbol * (j, 'row3, 'column2, 'square3) symbol * (k, 'row3, 'column3, 'square4) symbol * (l, 'row3, 'column4, 'square4) symbol * (m, 'row4, 'column1, 'square3) symbol * (n, 'row4, 'column2, 'square3) symbol * (o, 'row4, 'column3, 'square4) symbol * (p, 'row4, 'column4, 'square4) symbol *
That is two symbols in the same row/column/square will share the same 'row/'symbol/'square type. For any couple of symbols in say, a row, they must agree on that type, hence, on the position of every symbol.
Let's look at the 'A' symbol for the 'a' and 'c' position for instance. Both share the same 'row1 type variable. There are two cases. Either both are 'A's ore one is not.
- If one symbol is not a 'A', let's say those are 'C' and 'A' symbols. Their row type (pun almost intended) will be respectively
< c : r1; .. >and
< a : r3; .. >. Meaning that 'C' does not care about the position of 'A' and conversly. Those types are compatible. No problem here.
- If both are 'A's then something else happens. Their row types will be
< a : r1; .. >and
< a : r3; .. >which is certainly not compatible since r1 and r3 are not compatible. This will be rejected. Now we have a grid type that checks the sudoku constraints !
Let's try it.
let ok = Grid (A, B, C, D, C, D, A, B, D, A, B, C, B, C, D, A) val ok : grid = Grid (A, B, C, D, C, D, A, B, D, A, B, C, B, C, D, A) let not_ok = Grid (A, B, C, D, C, D, A, B, D, A, B, C, B, C, A, D) B, C, A, D);; ^ Error: This expression has type (o, < a : r3; b : r1; c : r2; d : 'a > row, < a : c4; b : 'b; c : 'c; d : 'd > column, < a : s3; b : 'e; c : 'f; d : 'g > square) symbol but an expression was expected of type (o, < a : r3; b : r1; c : r2; d : 'a > row, < a : c2; b : c3; c : c1; d : 'h > column, < a : 'i; b : s1; c : s2; d : 'j > square) symbol Types for method a are incompatible
What it is trying to say is that 'A' is both at position '2' and '4' of its column. Well it seems to work.
But we are not only interested in checking that a solution is correct, we want to find them !
But with 'one weird trick' we will magically transform it into a solver, namely the
-> . syntax. It was introduced in OCaml 4.03 for some other purpose. But we will now use its hidden power !
This is the right hand side of a pattern. It explicitely states that a pattern is unreachable. For instance
type _ t = | Int : int -> int t | Float : float -> float t let add (type v) (a : v t) (b : v t) : v t = match a, b with | Int a, Int b -> Int (a + b) | Float a, Float b -> Float (a +. b) | _ -> .
By writing it here you state that you don't expect any other pattern to verify the type constraints. This is effectively the case here. In general you won't need this as the exhaustivity checker will see it. But in some intricate situations it will need some hints to work a bit more. For more information see Jacques Garrigue / Le Normand article
This may be a bit obscure, but this is what we now need. Indeed, we can ask the exhaustivity checker if there exist a value verifying the pattern and the type constraints. For instance to solve a problem, we ask the compiler to check if there is any value verifying a partial solution encoded as a pattern.
A _ C _ _ D _ B _ A D _ D _ B _
let test x = match x with | Grid (A, _, C, _, _, D, _, B, _, A, D, _, D, _, B, _) -> . | _ -> () Error: This match case could not be refuted. Here is an example of a value that would reach it: Grid (A, B, C, D, C, D, A, B, B, A, D, C, D, C, B, A)
The checker tells us that there is a solution verifying those constraints, and provides it.
If there were no solution, there would have been no error.
let test x = match x with | Grid (A, B, C, _, _, _, _, D, _, _, _, _, _, _, _, _) -> . | _ -> () val test : grid -> unit =
And that's it !
Wrapping it up
Of course that's a bit cheating since the program is not executable, but who cares really ? If you want to use it, I made a small (ugly) script generating those types. You can try it on bigger problems, but in fact it is a bit exponential. So you shouldn't really expect an answer too soon.
Louis Gesbert (28 April 2017 at 8 h 11 min):
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust.
We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch.
Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users'). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Please reach out, we'll be delighted to discuss your challenges: email@example.com or book a quick discussion.