Instantly share code, notes, and snippets.

Embed
What would you like to do?
Type-Level Instant Insanity in Scala
object InstantInsanity extends App {
// scalastyle:off
def undefined[T]: T = ???
def ⊥[T]: T = undefined
trait R
trait G
trait B
trait W
trait Cube[u, f, b, r, l, d]
type Cube1 = Cube[B, G, W, G, B, R]
type Cube2 = Cube[W, G, B, W, R, R]
type Cube3 = Cube[G, W, R, B, R, R]
type Cube4 = Cube[B, R, G, G, W, W]
trait Transform[u, f, r, b, l, d] {
def rot: Cube[u, f, r, b, l, d] => Cube[u, r, b, l, f, d]
def twist: Cube[u, f, r, b, l, d] => Cube[f, r, u, l, d, b]
def flip: Cube[u, f, r, b, l, d] => Cube[d, l, b, r, f, u]
}
implicit def transform[u, f, r, b, l, d] = new Transform[u, f, r, b, l, d] {
def rot: (Cube[u, f, r, b, l, d]) => Cube[u, r, b, l, f, d] =
def twist: (Cube[u, f, r, b, l, d]) => Cube[f, r, u, l, d, b] =
def flip: (Cube[u, f, r, b, l, d]) => Cube[d, l, b, r, f, u] =
}
def rot[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.rot(cube)
def twist[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.twist(cube)
def flip[u, f, r, b, l, d](cube: Cube[u, f, r, b, l, d])(implicit t: Transform[u, f, r, b, l, d]) = t.flip(cube)
// :type rot(⊥[Cube1])
// :type twist(flip(rot(⊥[Cube1])))
trait True
trait False
trait And[l, r, o]
implicit object ttt extends And[True, True, True]
implicit object tff extends And[True, False, False]
implicit object ftf extends And[False, True, False]
implicit object fff extends And[False, False, False]
def and[l, r, o](l: l, r: r)(implicit and: And[l, r, o]): o =
// :type and(⊥[True], ⊥[False])
trait Nil
trait :::[x, xs]
trait ListConcat[l1, l2, l]
implicit def nilConcat[l]: ListConcat[Nil, l, l] =
implicit def notNilConcat[x, xs, ys, zs](implicit
lc: ListConcat[xs, ys, zs]
): ListConcat[x ::: xs, ys, x ::: zs] =
def listConcat[xs, ys, zs](l1: xs, l2: ys)(implicit
lc: ListConcat[xs, ys, zs]
): zs =
// :type listConcat(⊥[R ::: Nil], ⊥[G ::: W ::: Nil])
trait Rotation
trait Twist
trait Flip
trait Apply[f, a, b]
implicit def apRotation[u, f, r, b, l, d]: Apply[Rotation, Cube[u, f, r, b, l, d], Cube[u, r, b, l, f, d]] =
implicit def apTwist[u, f, r, b, l, d]: Apply[Twist, Cube[u, f, r, b, l, d], Cube[f, r, u, l, d, b]] =
implicit def apFlip[u, f, r, b, l, d]: Apply[Flip, Cube[u, f, r, b, l, d], Cube[d, l, b, r, f, u]] =
def ap[t, u, f, r, b, l, d, o](r: t, c1: Cube[u, f, r, b, l, d])(implicit
ap: Apply[t, Cube[u, f, r, b, l, d], o]
): o =
// :type ap(⊥[Rotation], ⊥[Cube1])
trait Map[f, xs, zs]
implicit def mapNil[f]: Map[f, Nil, Nil] =
implicit def mapCons[f, x, z, xs, zs](implicit
ap: Apply[f, x, z],
map: Map[f, xs, zs]
): Map[f, x ::: xs, z ::: zs] =
def map[f, xs, zs](f: f, xs: xs)(implicit
map: Map[f, xs, zs]
): zs =
// :type map(⊥[Flip], ⊥[Cube1 ::: Cube2 ::: Nil])
trait AppendIf[b, x, ys, zs]
implicit def appendIfTrue[x, ys]: AppendIf[True, x, ys, x ::: ys] =
implicit def appendIfFalse[x, ys]: AppendIf[False, x, ys, ys] =
def append[b, x, ys, zs](b: b, x: x, ys: ys)(implicit
apn: AppendIf[b, x, ys, zs]
): zs =
// :type append(⊥[True], ⊥[R], ⊥[G ::: W ::: Nil])
// :type append(⊥[False], ⊥[R], ⊥[G ::: W ::: Nil])
trait Filter[f, xs, zs]
implicit def filterNil[f]: Filter[f, Nil, Nil] =
implicit def filterCons[f, x, b, xs, ys, zs](implicit
ap: Apply[f, x, b],
f: Filter[f, xs, ys],
apn: AppendIf[b, x, ys, zs]
): Filter[f, x ::: xs, zs] =
//
trait MapAppend[f, xs, zs]
implicit def mapAppendNil[f]: MapAppend[f, Nil, Nil] =
implicit def mapAppendCons[f, xs, ys, zs](implicit
m: Map[f, xs, ys],
lc: ListConcat[xs, ys, zs]
): MapAppend[f, xs, zs] =
trait MapAppend2[f, xs, zs]
implicit def mapAppend2Nil[f]: MapAppend2[f, Nil, Nil] =
implicit def mapAppend2Cons[f, xs, ys, _ys, zs](implicit
m: Map[f, xs, ys],
ma: MapAppend[f, ys, _ys],
lc: ListConcat[xs, _ys, zs]
): MapAppend2[f, xs, zs] =
trait MapAppend3[f, xs, zs]
implicit def mapAppend3Nil[f]: MapAppend3[f, Nil, Nil] =
implicit def mapAppend3Cons[f, xs, ys, _ys, zs](implicit
m: Map[f, xs, ys],
ma2: MapAppend2[f, ys, _ys],
lc: ListConcat[xs, _ys, zs]
): MapAppend3[f, xs, zs] =
trait Orientations
implicit def orientations[c, fs, ts, zs](implicit
ma: MapAppend[Flip, c ::: Nil, fs],
ma2: MapAppend2[Twist, fs, ts],
ma3: MapAppend3[Rotation, ts, zs]
): Apply[Orientations, c, zs] =
// :type ap(⊥[Orientations], ⊥[Cube1])
trait NE[x, y, b]
implicit object neRR extends NE[R, R, False]
implicit object neRG extends NE[R, G, True]
implicit object neRB extends NE[R, B, True]
implicit object neRW extends NE[R, W, True]
implicit object neGR extends NE[G, R, True]
implicit object neGG extends NE[G, G, False]
implicit object neGB extends NE[G, B, True]
implicit object neGW extends NE[G, W, True]
implicit object neBR extends NE[B, R, True]
implicit object neBG extends NE[B, G, True]
implicit object neBB extends NE[B, B, False]
implicit object neBW extends NE[B, W, True]
implicit object neWR extends NE[W, R, True]
implicit object neWG extends NE[W, G, True]
implicit object neWB extends NE[W, B, True]
implicit object neWW extends NE[W, W, False]
trait All[l, b]
implicit def allNil: All[Nil, True]
=
implicit def allFalse[xs]: All[False ::: xs, False] =
implicit def allTrue[b, xs](implicit all: All[xs, b]): All[True ::: xs, b] =
def all[b, xs](l: xs)(implicit all: All[xs, b]): b =
// :type all(⊥[Nil])
// :type all(⊥[False ::: Nil])
// :type all(⊥[True ::: False ::: Nil])
// :type all(⊥[True ::: True ::: Nil])
trait Compatible[c1, c2, b]
implicit def compatibleInstance[f1, f2, bF, r1, r2, bR, b1, b2, bB, l1, l2, bL, u1, u2, d1, d2, b](implicit
ne1: NE[f1, f2, bF],
ne2: NE[r1, r2, bR],
ne3: NE[b1, b2, bB],
ne4: NE[l1, l2, bL],
all: All[bF ::: bR ::: bB ::: bL ::: Nil, b]
): Compatible[Cube[u1, f1, r1, b1, l1, d1], Cube[u2, f2, r2, b2, l2, d2], b] =
def compatible[c1, c2, b](c1: c1, c2: c2)(implicit
c: Compatible[c1, c2, b]
): b =
// :type compatible(⊥[Cube[R, R, R, R, R, R]], ⊥[Cube[B, B, B, B, B, B]])
// :type compatible(⊥[Cube[R, R, G, R, R, R]], ⊥[Cube[B, B, G, B, B, B]])
trait Allowed[c, cs, b]
implicit def allowedNil[c]: Allowed[c, Nil, True] =
implicit def allowedCons[c, y, b1, ys, b2, b](implicit
c: Compatible[c, y, b1],
allowed: Allowed[c, ys, b2],
and: And[b1, b2, b]
): Allowed[c, y ::: ys, b] =
def allowed[c, cs, b](c: c, cs: cs)(implicit a: Allowed[c, cs, b]): b =
type CubeRed = Cube[R, R, R, R, R, R]
type CubeBlue = Cube[B, B, B, B, B, B]
// :type allowed(⊥[CubeRed], ⊥[CubeBlue ::: CubeRed ::: Nil])
trait MatchingOrientations[os, sols, zs]
implicit def matchingOrientationsNil[sol]: MatchingOrientations[Nil, sol, Nil] =
implicit def matchingOrientationsCons[os, sol, as, o, b, zs](implicit
mo: MatchingOrientations[os, sol, as],
a: Allowed[o, sol, b],
apn: AppendIf[b, o ::: sol, as, zs]
): MatchingOrientations[o ::: os, sol, zs] =
trait AllowedCombinations[os, sols, zs]
implicit def allowedCombinationsNil[os]: AllowedCombinations[os, Nil, Nil] =
implicit def allowedCombinationsCons[os, sols, as, s, bs, zs](implicit
ac: AllowedCombinations[os, sols, as],
mo: MatchingOrientations[os, s, bs],
lc: ListConcat[as, bs, zs]
): AllowedCombinations[os, s ::: sols, zs] =
class Solutions[cs, ss]
implicit def solutionsNil: Solutions[Nil, Nil ::: Nil] =
implicit def solutionsCons[cs, sols, c, os, zs](implicit
s: Solutions[cs, sols],
ap: Apply[Orientations, c, os],
ac: AllowedCombinations[os, sols, zs]
): Solutions[c ::: cs, zs] =
type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil)
def solutions[cs, ss](cs: cs)(implicit sol: Solutions[cs, ss]): ss =
// :type solutions(⊥[Cubes])
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment