EzSudoku

---

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.

Solving it

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.

Comments

Louis Gesbert (28 April 2017 at 8 h 11 min):

Brilliant!

---

About OCamlPro:

OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from experts with a state-of-the-art knowledge of programming languages theory and practice.

• We provide audit, support, custom developer tools and training for both the most modern languages, such as Rust, Wasm and OCaml, and for legacy languages, such as COBOL or even home-made domain-specific languages;
• We design, create and implement software with great added-value for our clients. High complexity is not a problem for our PhD-level experts. For example, we helped the French Income Tax Administration re-adapt and improve their internally kept M language, we designed a DSL to model and express revenue streams in the Cinema Industry, codename Niagara, and we also developed the prototype of the Tezos proof-of-stake blockchain from 2014 to 2018.
• We have a long history of creating open-source projects, such as the Opam package manager, the LearnOCaml web platform, and contributing to other ones, such as the Flambda optimizing compiler, or the GnuCOBOL compiler.
• We are also experts of Formal Methods, developing tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users' Club) and using them to prove safety or security properties of programs.

Please reach out, we'll be delighted to discuss your challenges: contact@ocamlpro.com or book a quick discussion.