This post shows an implementation of Instant Insanity puzzle game at compile time, using powerful Scala type system. This post is
based on amazing article by Conrad Parker in the Monad Reader Issue 8.
Original article is around 20 pages long, this post is much more concise version of it. Original article is very well written and easy to
understand, this post should help with jumping from Scala to Haskell code for people who are not familiar with Haskell language.
It consists of four cubes, with faces coloured blue, green, red or white.
The problem is to arrange the cubes in a vertical pile such that each
visible column of faces contains four distinct colours.
“Classic” solution in scala can be found here, this solution
stacks the cubes one at a time, trying each possible orientation of each cube.
I’m going to show how to translate this solution into Scala Type System.
Type-Level Implementation
When I say “Type-Level Implementation”, I mean that I’m going to find a solution to the problem without creating any “values”,
just operating with types, and I’ll do it using Scala compiler only, without running any code.
⊥ (Bottom)
I’m working in the type system, so I don’t need any value for any of the variables, just the type. In scala there is one
special type, that is subtype of every other type - Nothing. There exist no instances of this type, but that’s ok because I don’t need one.
I’m introducing two functions that will make code look closer to Haskell version, and will save me some typing.
There are four possible colors. Rather then encoding them as values of type Char, I’m introducing new types.
1234
traitR// RedtraitG// GreentraitB// BluetraitW// White
12
scala>:type⊥[R]R
Parametrized Types
A cube is a thing that can have six faces. In Scala Type System, I use the keyword trait to introduce such a thing:
1
traitCube[u, f, r, b, l, d]
I can’t get a type of a Cube because there is not such thing, Cube exist only when it’s applied to type parameters,
namely u, f, r, b, l, d. Applying concrete types to Cube will create concrete result type.
One way to think about Cube is that it’s like a function, but at the type level.
123456
scala>:type⊥[Cube]<console>:17:error:traitCubetakestypeparameters⊥[Cube]scala>:type⊥[Cube[R, R, R, R, R, R]]// a red cubeCube[R,R,R,R,R,R]
Type Aliases
Now I can define the actual cubes in our puzzle as results of applying Cube function to concrete types.
Now I need to encode following three functions from textbook solution at a type-level.
123456789
// Rotate a cube 90 degrees over its Z-axis, leaving up and down in place.defrot:Cube=>Cube={caseSeq(u,f,r,b,l,d)=>Seq(u,r,b,l,f,d)}// Twist a cube around the axis running from the upper-front-right// corner to the back-left-down corner.deftwist:Cube=>Cube={caseSeq(u,f,r,b,l,d)=>Seq(f,r,u,l,d,b)}// Exchange up and down, front and left, back and right.defflip:Cube=>Cube={caseSeq(u,f,r,b,l,d)=>Seq(d,l,b,r,f,u)}
I’m going to group all of them into single Transform trait. Implicit transform function can generate an
instance of Transform for any type u, f, r, b, l, d. I’m not providing any implementation for any of them,
because I never going to call them.
Now I can create a function that recurses over a list and Applys another function f to each element. This is type-level
equivalent of the map function.
Filter introduced new constraint, AppendIf, which takes a boolean values b, a value x and a list ys.
The given values x is appended to ys only if b is True, otherwise ys is returned unaltered:
Unfortunately sequence comprehensions can’t be directly mimiced in Scala Type System, but we can translate the meaning of a given
sequence comprehension using the type-level list functions.
For example, building a list of the possible orientations of a cube involves appending a list of possible
applications of flip, so we will need to be able to map over a list and append the original list. Original sequence comprehension was:
I will implement Orientation as an Applyable type function. It’s defined in terms of applications of
Rotation, Twist and Flip, invoked via various MapAppend functions:
Given two cubes Cube[u1, f1, r1, b1, l1, d1] and Cube[u2, f2, r2, b2, l2, d2], I want to check that none of
the corresponding visible faces are the same color: the front sides f1 and f2 are not equal, and the right
sides r1 and r2 are not equal, and so on.
In order to do this, it’s required to define not equal relation for all four colors. Given two cubes I can apply
this relations to each pair of visible faces to get four boolean values. To check that all of these are True, I will
construct a list of those values and then write generic list function to check if all elements of a list are True.
Not Equal
I’m instantiating NE instance for all color combinations.
Now I can write the compatibility check in the Scala Type System, that corresponds original compatible funcation:
12345678
// Compute which faces of a cube are visible when placed in a pile.defvisible:Cube=>Seq[Char]={caseSeq(u,f,r,b,l,d)=>Seq(f,r,b,l)}// Two cubes are compatible if they have different colours on every// visible face.defcompatible:(Cube,Cube)=>Boolean={case(c1,c2)=>visible(c1).zip(visible(c2)).forall{case(v1,v2)=>v1!=v2}}
I introduce a new Compatible class, it should check that no corresponding visible faces are the same color. It does
validation by evaluating NE relationship for each pair of corresponding visible faces.
The above Compatible class checks a cube for compatibility with another single cube. In the puzzle,
a cube needs to be compatible with all the other cubes in the pile.
12345
// Determine whether a cube can be added to pile of cubes, without// invalidating the solution.defallowed:(Cube,Seq[Cube])=>Boolean={case(c,cs)=>cs.forall(compatible(_,c))}
// Return a list of all ways of orienting each cube such that no side of// the pile has two faces the same.defsolutions:Seq[Cube]=>Seq[Seq[Cube]]={caseNil=>Seq(Nil)casec::cs=>for{_cs<-solutions(cs)_c<-orientations(c)ifallowed(_c,_cs)}yield_c+:_cs}
I will create a corresponding class Sultions, which takes a list of Cube as input, and returs a list of
possible solutions, where each solution is a list of Cube in allowed orientations.
Unfortunately I still was not able to compute solution for four cubes, it’s still running (almost 24 hours).
I will update this post when it’s done. But without loss of generality I can compute all possible ways to
arrange a list with one single cube.
Computing solution for two cubes takes reasonable 10 minutes, but it generates so many possible arrangements,
and final type name is so long, that it breaks JVM class file size limitation.
scala>:typesolutions(⊥[Cubes])// It's already running for 24 hoursscala>:typesolutions(⊥[Cube1:::Nil])(Cube[B,G,W,G,B,R]:::Nil):::(Cube[R,B,G,W,G,B]:::Nil):::(Cube[G,W,B,B,R,G]:::Nil):::(Cube[B,G,R,G,B,W]:::Nil):::(Cube[W,B,G,R,G,B]:::Nil):::(Cube[G,R,B,B,W,G]:::Nil):::(Cube[B,W,G,B,G,R]:::Nil):::(Cube[R,G,W,G,B,B]:::Nil):::(Cube[G,B,B,R,W,G]:::Nil):::(Cube[B,R,G,B,G,W]:::Nil):::(Cube[W,G,R,G,B,B]:::Nil):::(Cube[G,B,B,W,R,G]:::Nil):::(Cube[B,G,B,G,W,R]:::Nil):::(Cube[R,W,G,B,G,B]:::Nil):::(Cube[G,B,R,W,B,G]:::Nil):::(Cube[B,G,B,G,R,W]:::Nil):::(Cube[W,R,G,B,G,B]:::Nil):::(Cube[G,B,W,R,B,G]:::Nil):::(Cube[B,B,G,W,G,R]:::Nil):::(Cube[R,G,B,G,W,B]:::Nil):::(Cube[G,R,W,B,B,G]:::Nil):::(Cube[B,B,G,R,G,W]:::Nil):::(Cube[W,G,B,G,R,B]:::Nil):::(Cube[G,W,R,B,B,G]:::Nil):::Nil
For comparison, here is the solution generated by the pure Scala version:
Conclusion
We’ve seen how to use Scala Type System as a programming language to solve a given problem, and apparently
it’s as powerful as Haskell Type System.
Solving this kind of puzzles using type system is not very practical, it took me more then 24 hours to get
a solution, but it shows how expressing type system can be.
Full code for Type-Level Instant Insanity is on Github