# Type-Level Instant Insanity in Scala

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.

## Simple Types

There are four possible colors. Rather then encoding them as `values` of type `Char`, I’m introducing new types.

## 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:

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.

## Type Aliases

Now I can define the actual cubes in our puzzle as results of applying `Cube` function to concrete types.

## Transformation Functions

Now I need to encode following three functions from textbook solution at a type-level.

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.

## 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

## Type-Level Lists

Lists at a type-level can be defined as following atoms:

To make lists useful I’ll need concatenate function, that should be also encoded at a type-level.

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:

## 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.

`Filter` function is similar to `Map`:

`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:

## 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:

I create `MapAppend` class in order to compose `Map` and `ListConcat`:

Further, I’ll need to be able to do the same twice for twist and three times for rot:

## Orientation

The full sequence comprehension for generating all possible orientations of a cube build upon all combinations of rot, twist and flip:

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:

For any `Cube` this function generates the 24 possible orientations:

## 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.

## All

Now, I define a function all to check if all elements of a list are True.

## Compatible

Now I can write the compatibility check in the Scala Type System, that corresponds original compatible funcation:

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.

## 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.

`Allowed` class generalize `Compatible` over list.

## Solution

Now I’m ready to implement solutions:

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.

The `AllowedCombinations` class recurses across the solutions so far, checking each against the given orientation.

Finally `MatchingOrientations` class recurses across the orientations of the new cube, checking each against a particular solution sol.

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:

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.

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