This post is a Scala version of Haskell Type-Level Instant Insanity by Conrad Parker
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.
Textbook Implementation
Instant Insanity puzzle formulated as:
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.
1 2 |
|
1 2 3 4 5 |
|
Simple Types
There are four possible colors. Rather then encoding them as values
of type Char
, I’m introducing new types.
1 2 3 4 |
|
1 2 |
|
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
|
|
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.
1 2 3 4 5 6 |
|
Type Aliases
Now I can define the actual cubes in our puzzle as results of applying Cube
function to concrete types.
1 2 3 4 5 6 7 |
|
Transformation Functions
Now I need to encode following three functions from textbook solution at a type-level.
1 2 3 4 5 6 7 8 9 |
|
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.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
|
1 2 3 4 5 |
|
Type-Level Boolean Algebra
So far we’ve seen how to construct simple types, and perform type transformations of one parametrized type into a differently parametrized type.
For solving a puzzle I’ll need some rudimentary boolean algebra at a type-level:
- encode true/false in types
- provide boolean
and
operator
1 2 3 4 5 6 7 8 9 10 11 |
|
1 2 3 4 5 |
|
Type-Level Lists
Lists at a type-level can be defined as following atoms:
1 2 |
|
To make lists useful I’ll need concatenate function, that should be also encoded at a type-level.
1 2 3 4 5 6 7 8 9 10 |
|
1 2 |
|
As you can see now I can concatenate two lists at type-level: [R] concat [G, W] yields [R, G, W].
Applyable Type Functions
For this puzzle I need to be able to do things like flip each of the cubes in a list, which sounds exactly like map at the type level.
First step is abstracting application of a type-level function, so I introduce Apply
and supported operations:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
|
1 2 |
|
Map and Filter
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.
1 2 3 4 5 6 7 8 9 10 11 |
|
1 2 |
|
Filter
function is similar to Map
:
1 2 3 4 5 6 7 8 |
|
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:
1 2 3 4 5 6 7 8 |
|
1 2 3 4 5 |
|
Sequence Comprehensions
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:
1 2 3 4 5 6 |
|
I create MapAppend
class in order to compose Map
and ListConcat
:
1 2 3 4 5 6 7 |
|
Further, I’ll need to be able to do the same twice for twist and three times for rot:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 |
|
Orientation
The full sequence comprehension for generating all possible orientations of a cube build upon all combinations of rot, twist and flip:
1 2 3 4 5 6 7 |
|
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:
1 2 3 4 5 6 7 |
|
For any Cube
this function generates the 24 possible orientations:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
|
Stacking Cubes
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.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 |
|
All
Now, I define a function all to check if all elements of a list are True.
1 2 3 4 5 6 7 |
|
1 2 3 4 5 6 7 8 9 10 11 |
|
Compatible
Now I can write the compatibility check in the Scala Type System, that corresponds original compatible funcation:
1 2 3 4 5 6 7 8 |
|
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.
1 2 3 4 5 6 7 8 9 10 11 12 13 |
|
1 2 3 4 5 |
|
Allowed
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.
1 2 3 4 5 |
|
Allowed
class generalize Compatible
over list.
1 2 3 4 5 6 7 8 9 10 |
|
1 2 |
|
Solution
Now I’m ready to implement solutions:
1 2 3 4 5 6 7 8 9 10 |
|
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.
1 2 3 4 5 6 7 8 |
|
The AllowedCombinations
class recurses across the solutions so far, checking each against the given orientation.
1 2 3 4 5 6 7 |
|
Finally MatchingOrientations
class recurses across the orientations of the new cube, checking each against a particular solution sol.
1 2 3 4 5 6 7 |
|
If orientation is allowed, then the combination o is added to the existing solution sol, by forming the type o ::: sol.
Finally I can solve the puzzle for given cubes:
1 2 3 |
|
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.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 |
|
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