はじめに

「PureScriptにはこんなに表現力の高い型システムがあるんだ！」というような気持ちで読んでもらえれば丁度いいと思います。

この方法を使うと「渡された値は整数か？」と同じ要領で「渡されたルービックキューブは不正ではないか？解くことが可能か？」といった検査がコンパイル時にできてしまいます！

※本記事で扱うルービックキューブは2x2x2のものです。

未公開のままだった記事を成仏させるために公開したので、PureScriptのバージョンが結構古めです（v0.13.5くらい）。

注意点

型レベル計算を多用するため、IDEがめちゃくちゃ頑張ることになります。エディタを開いているだけでCPUやメモリの使用率がとても上がる点にご注意ください（IDEを切っていれば平気）。

解く手順

今回の手順は以下の通りです。

完成しているかどうか確認する。
1. で解けていたら、「直前に回した回転記号リスト」を返して終了。
1. で解けていなかったら、以下に続く。
各回転記号を「直前に回した回転記号リスト」の後ろに結合したものを全てキューに入れる。
キューの先頭を取り出す。
1. で取り出した回転記号リストに従ってキューブを回す。
1. に戻る。

幅優先探索を用いています。

回転記号

ルービックキューブの回転を表すために、以下のような回転記号が用いられます。

回転記号	意味
f	前面を時計回りに回す
b	後面を時計回りに回す
r	右面を時計回りに回す
l	左面を時計回りに回す
u	上面を時計回りに回す
d	下面を時計回りに回す
x	下面が正面になるように持ち替え
y	右面が正面になるように持ち替え
z	左面が上面になるように持ち替え
○'	○の逆

実際に書いていく

さっそくルービックキューブを解く準備をしていきます。

キューブをSymbolで表現する

こんなふうに展開した形式のキューブを用意したいです。

  RR
  RR
WWBBYYGG
WWBBYYGG
  OO
  OO

これは、このように表すことにします。

"RRRRWWBBYYGGWWBBYYGGOOOO"

SProxyに渡して幽霊型の値を作ることができます。

SProxy :: SProxy "RRRRWWBBYYGGWWBBYYGGOOOO"

キューブを分解・合成する

class ConsCube
  (mode :: Symbol)
  (c1  :: Symbol) (c2  :: Symbol) (c3  :: Symbol) (c4  :: Symbol)
  (c5  :: Symbol) (c6  :: Symbol) (c7  :: Symbol) (c8  :: Symbol)
  (c9  :: Symbol) (c10 :: Symbol) (c11 :: Symbol) (c12 :: Symbol)
  (c13 :: Symbol) (c14 :: Symbol) (c15 :: Symbol) (c16 :: Symbol)
  (c17 :: Symbol) (c18 :: Symbol) (c19 :: Symbol) (c20 :: Symbol)
  (c21 :: Symbol) (c22 :: Symbol) (c23 :: Symbol) (c24 :: Symbol) (cube :: Symbol)
  | mode
    c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
    c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
    -> cube
  , mode
    cube ->
    c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
    c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24

instance deConsCube ::
  ( Cons c1  t1  cube, Cons c2  t2  t1 , Cons c3  t3  t2 , Cons c4  t4  t3
  , Cons c5  t5  t4  , Cons c6  t6  t5 , Cons c7  t7  t6 , Cons c8  t8  t7
  , Cons c9  t9  t8  , Cons c10 t10 t9 , Cons c11 t11 t10, Cons c12 t12 t11
  , Cons c13 t13 t12 , Cons c14 t14 t13, Cons c15 t15 t14, Cons c16 t16 t15
  , Cons c17 t17 t16 , Cons c18 t18 t17, Cons c19 t19 t18, Cons c20 t20 t19
  , Cons c21 t21 t20 , Cons c22 t22 t21, Cons c23 t23 t22, Cons c24 ""  t23
  ) => ConsCube "DeCon"
         c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
         c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube

else instance consCube ::
  ( Cons   c1  ""  t1 , Cons   t1  c2  t2 , Append t2  c3  t3 , Append t3  c4  t4
  , Append t4  c5  t5 , Append t5  c6  t6 , Append t6  c7  t7 , Append t7  c8  t8
  , Append t8  c9  t9 , Append t9  c10 t10, Append t10 c11 t11, Append t11 c12 t12
  , Append t12 c13 t13, Append t13 c14 t14, Append t14 c15 t15, Append t15 c16 t16
  , Append t16 c17 t17, Append t17 c18 t18, Append t18 c19 t19, Append t19 c20 t20
  , Append t20 c21 t21, Append t21 c22 t22, Append t22 c23 t23, Append t23 c24 cube
  ) => ConsCube "Con"
         c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
         c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube

このクラスを以下のように呼び出すと分解や合成が可能です。

-- 分解
ConsCube "DeCon"
         c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
         c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
         "RRRRWWBBYYGGWWBBYYGGOOOO"

-- 合成
ConsCube "Con"
         "R" "R" "R" "R" "W" "W" "B" "B" "Y" "Y" "G" "G"
         "W" "W" "B" "B" "Y" "Y" "G" "G" "O" "O" "O" "O" cube

キューブを表示する

ConsCube型クラスを使って分解し、展開図の形になるように文字列として連結していきます。reflectSymbol関数はSymbolをStringに変換する関数で、これを使うためにはIsSymbol型クラス制約が必要になります。

showCube
  :: forall   c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
              c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
   . ConsCube "DeCon"
              c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
              c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  => IsSymbol c1  => IsSymbol c2  => IsSymbol c3  => IsSymbol c4  => IsSymbol c5  => IsSymbol c6
  => IsSymbol c7  => IsSymbol c8  => IsSymbol c9  => IsSymbol c10 => IsSymbol c11 => IsSymbol c12
  => IsSymbol c13 => IsSymbol c14 => IsSymbol c15 => IsSymbol c16 => IsSymbol c17 => IsSymbol c18
  => IsSymbol c19 => IsSymbol c20 => IsSymbol c21 => IsSymbol c22 => IsSymbol c23 => IsSymbol c24
  => SProxy cube -> String
showCube _ =
           " " <> " " <> c1  <> c2
  <> nl <> " " <> " " <> c3  <> c4
  <> nl <> c5  <> c6  <> c7  <> c8  <> c9  <> c10 <> c11 <> c12
  <> nl <> c13 <> c14 <> c15 <> c16 <> c17 <> c18 <> c19 <> c20
  <> nl <> " " <> " " <> c21 <> c22
  <> nl <> " " <> " " <> c23 <> c24

  where
    nl  = "\n"
    c1  = reflectSymbol (SProxy :: SProxy c1 )
    c2  = reflectSymbol (SProxy :: SProxy c2 )
    c3  = reflectSymbol (SProxy :: SProxy c3 )
    c4  = reflectSymbol (SProxy :: SProxy c4 )
    c5  = reflectSymbol (SProxy :: SProxy c5 )
    c6  = reflectSymbol (SProxy :: SProxy c6 )
    c7  = reflectSymbol (SProxy :: SProxy c7 )
    c8  = reflectSymbol (SProxy :: SProxy c8 )
    c9  = reflectSymbol (SProxy :: SProxy c9 )
    c10 = reflectSymbol (SProxy :: SProxy c10)
    c11 = reflectSymbol (SProxy :: SProxy c11)
    c12 = reflectSymbol (SProxy :: SProxy c12)
    c13 = reflectSymbol (SProxy :: SProxy c13)
    c14 = reflectSymbol (SProxy :: SProxy c14)
    c15 = reflectSymbol (SProxy :: SProxy c15)
    c16 = reflectSymbol (SProxy :: SProxy c16)
    c17 = reflectSymbol (SProxy :: SProxy c17)
    c18 = reflectSymbol (SProxy :: SProxy c18)
    c19 = reflectSymbol (SProxy :: SProxy c19)
    c20 = reflectSymbol (SProxy :: SProxy c20)
    c21 = reflectSymbol (SProxy :: SProxy c21)
    c22 = reflectSymbol (SProxy :: SProxy c22)
    c23 = reflectSymbol (SProxy :: SProxy c23)
    c24 = reflectSymbol (SProxy :: SProxy c24)

次のように呼び出せます。

main :: Effect Unit
main = log $ showCube (SProxy :: SProxy "RRRRWWBBYYGGWWBBYYGGOOOO")

実行結果

  RR
  RR
WWBBYYGG
WWBBYYGG
  OO
  OO

キューブを回転させる

まずは前面の回転だけを考えることにします。

回転記号のためのカインドと型を作る

foreign import kind Notation

foreign import data F  :: Notation
foreign import data F' :: Notation

前面の回転記号であるfとその反対のf'のために型を作り、Notationというカインドにしました。

キューブを回転させる型クラスを作る

class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated

instance rotateF ::
  ( ConsCube "DeCon" c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
                     c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  , ConsCube "Con"   c7  c2  c15 c4  c6  c14 c21 c8  c9  c10 c11 c3
                     c5 c13  c23 c16 c17 c18 c19 c1  c20 c22 c12 c24 rotated
  ) => Rotate F  cube rotated

instance rotateF' ::
  ( Rotate F cube r'
  , Rotate F r'   r''
  , Rotate F r''  rotate
  ) => Rotate F' cube rotated

rotateFではキューブを分解し、f回転後の状態に並べ替えて結合し直します。その反対のrotateF'ではrotateFを呼び出した結果を再びrotateFに渡すことを3回繰り返します（ルービックキューブは4回回すと元に戻るので、ある方向への3回転とその反対方向への1回転は同じ結果になります）。

回転順序を表すカインドPathを作る

foreign import kind Path
foreign import data Path :: Notation -> Path -> Path
foreign import data PNil :: Path

data PProxy (p :: Path) = PProxy

class RotatePath (path :: Path) (cube :: Symbol) (rotated :: Symbol) | cube path -> rotated

instance rotatedPathNil :: RotatePath PNil cube cube

instance rotatedPath ::
  ( Rotate notation cube cube'
  , RotatePath tail cube' cube''
  , TypeEquals (SProxy cube'') (SProxy rotated)
  ) => RotatePath (Path notation tail) cube rotated

class AppendPath (pl :: Path) (pr :: Path) (plr :: Path) | pl pr -> plr

instance appendPathNil :: AppendPath PNil pr pr

instance appendPath ::
  ( AppendPath tail pr plr'
  , TypeEquals (PProxy (Path head plr')) (PProxy plr)
  ) => AppendPath (Path head tail) pr plr

PathとRotatePathを作ることによって、複数回の回転をシンプルに表せるようになります。

-- これが
instance rotateF' ::
  ( Rotate F cube r'
  , Rotate F r'   r''
  , Rotate F r''  rotate
  ) => Rotate F' cube rotated

-- こうなる！
instance rotateF' ::
  ( RotatePath
      (Path F (Path F (Path F PNil)))
      cube rotated
  ) => Rotate F' cube rotated

中間の変数が消えてとても読みやすくなります。

また、AppendPathクラスはPathとPathを連結するための型クラスです。これは後ほど使います。

Pathを保持するキューを作る

foreign import kind Queue
foreign import data Queue :: Path -> Queue -> Queue
foreign import data QNil  :: Queue

data QProxy (q :: Queue) = QProxy

class Enqueue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue path -> queue'

instance enqueueNil :: Enqueue QNil path (Queue path QNil)

instance enqueue ::
  ( Enqueue tail newPath q'
  , TypeEquals (QProxy (Queue path q')) (QProxy queue')
  ) => Enqueue (Queue path tail) newPath queue'

class Dequeue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue -> path queue'

instance dequeueNil :: Dequeue (Queue path tail) path tail
instance dequeue :: Dequeue QNil PNil QNil

型レベルのキューです。Enqueueによってキューの末尾にPathを追加、Dequeueによってキューの先頭からPathを取り出すことができます。キューブの状態を各回転順序ごとに調べていく幅優先探索のために用います。

使用例

test1 :: QProxy (Queue (Path F PNil) QNil)
test1 = QProxy :: (forall q. Enqueue QNil (Path F PNil) q => QProxy q)

test2 :: PProxy (Path F PNil)
test2 = PProxy :: (forall q' q'' p. Enqueue QNil (Path F PNil) q' => Dequeue q' p q'' => PProxy p)

探索候補をキューに入れる

class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'

instance enqueueAllPath ::
  ( TypeEquals (QProxy queue) (QProxy q')

  , AppendPath currPath (Path F  PNil) pF
  , Enqueue q'  pF  qF

  , AppendPath currPath (Path F' PNil) pF'
  , Enqueue qF  pF' qF'

  , TypeEquals (QProxy qF') (QProxy queue')
  ) => EnqueueAllNotation queue currPath queue'

これで現在のPathに対する次の深さの探索候補をすべてキューに追加することができます。

使用例

test1 :: QProxy (Queue (Path F PNil) (Queue (Path F' PNil) QNil))
test1 = QProxy :: forall q. EnqueueAllNotation QNil PNil q => QProxy q

test2 :: QProxy (Queue (Path F (Path F PNil)) (Queue (Path F (Path F' PNil)) QNil))
test2 = QProxy :: forall q. EnqueueAllNotation QNil (Path F PNil) q => QProxy q

上の例では、queueが空（QNil）で現在のpathが空（PNil）のときはqueue'がQueue (Path F PNil) (Queue (Path F' PNil) QNil)になり（test1）、queueが空で現在のpathがPath F PNilのときはqueue'がQueue (Path F' PNil) (Queue (Path F (Path F PNil)) (Queue (Path F (Path F' PNil)) QNil))になる（test2）ことを確かめています。

解く

ここまで積み上げてきたパーツを組み合わせ、実際に解いていきます。

cubeを渡すと完成までの回転順序をpathとして導出してくれる型クラスSolveを作ります。

class Solve (cube :: Symbol) (path :: Path) | cube -> path

instance initSolve ::
  (SolveImpl cube "RRRRWWBBYYGGWWBBYYGGOOOO" prev QNil PNil path) => Solve cube path

class SolveImpl
  (cube :: Symbol)
  (goal :: Symbol)
  (prevCube :: Symbol)
  (queue :: Queue)
  (currPath :: Path)
  (path :: Path)
  | cube goal -> path

instance solved :: SolveImpl goal goal prev queue currPath PNil
else instance solved' :: SolveImpl cube goal goal queue currPath path

else instance solveImpl ::
  ( EnqueueAllNotation queue currPath q
  , Dequeue q pHead qTail
  , RotatePath pHead cube rotated
  , Equals rotated goal isEq
  , If isEq (PProxy pHead) (PProxy path) (PProxy path)
  , SolveImpl cube goal rotated qTail pHead path
  ) => SolveImpl cube goal prev queue currPath path

このように作りました。

SolveImplで行っているのは何の工夫もないただの幅優先探索で、ゴールはSolveのインスタンスinitSolveから渡された完成状態のキューブです。cubeとgoalが一致したところのcurrPath（直前に回した回転記号リスト）を返して終了します。

型クラスSolveの使い方

まだ前面のfとf'しか考えていないため、前面だけをシャッフルして解かせてみます。

まずは前面を時計回りに1回だけ回した結果のキューブを見ます。

-- f方向に回す
shuffle :: SProxy "BRBRWWOBYYGRWWOBYYGRGOGO"
shuffle = SProxy
  :: forall shuffled
   . RotatePath (Path F PNil) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => SProxy shuffled

1回だけですがシャッフルされました。これはfの方向に1度回しため、解き方としてはPath F' PNilが正しいです。結果を見てみましょう。

solve :: PProxy (Path F' PNil)
solve = PProxy
  :: forall shuffled path
   . RotatePath (Path F PNil) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => Solve shuffled path
  => PProxy path

正しく解き方を導出できています！

次はf方向に3回回した場合の解き方を導出させてみます。

solve :: PProxy (Path F PNil)
solve = PProxy
  :: forall shuffled path
   . RotatePath (Path F (Path F (Path F PNil))) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => Solve shuffled path
  => PProxy path

答えはPath F PNilとなりました。キューブは4回回すと元に戻ってくるので、同じ方向に3回回した場合はもう一度回せば戻ってきます。正しいです。

solve :: PProxy (Path F (Path F PNil))
solve = PProxy
  :: forall shuffled path
   . RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => Solve shuffled path
  => PProxy path

次に、この方法の問題点が1つ発覚します。

-- 正しい
solve1 :: PProxy (Path F (Path F PNil))
solve1 = PProxy
  :: forall shuffled path
   . RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => Solve shuffled path
  => PProxy path

-- 正しくない(エラー)
solve2 :: PProxy (Path F' (Path F' PNil))
solve2 = PProxy
  :: forall shuffled path
   . RotatePath (Path F (Path F PNil)) "RRRRWWBBYYGGWWBBYYGGOOOO" shuffled
  => Solve shuffled path
  => PProxy path

この例では、f方向に2回、つまり前面を180度回転させたキューブを解かせています。fとf'のどちらに2回回しても解けるはずですが、関数の型定義にf'方向に2回回すPathを書いたsolve2ではエラーになってしまっています。

これは、型クラスEnqueueAllNotationでキューに入れる探索候補の順番と幅優先探索の方法によって起きてしまった問題です。候補が見つかり次第終了するこの方法では、それより後に見つかる別解を導出できません。

他の回転方法も追加する

ここまでは前面（fとf'）だけを考えてきましたが、他の回転も追加します。

まず、回転の型を追加します。

foreign import kind Notation

foreign import data F  :: Notation
foreign import data F' :: Notation
foreign import data R  :: Notation
foreign import data R' :: Notation
foreign import data B  :: Notation
foreign import data B' :: Notation
foreign import data U  :: Notation
foreign import data U' :: Notation
foreign import data L  :: Notation
foreign import data L' :: Notation
foreign import data D  :: Notation
foreign import data D' :: Notation
foreign import data X  :: Notation
foreign import data X' :: Notation
foreign import data Y  :: Notation
foreign import data Y' :: Notation
foreign import data Z  :: Notation
foreign import data Z' :: Notation

次に、型クラスRotateのインスタンスを追加します。

class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated

instance rotateF ::
  ( ConsCube "DeCon" c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
                     c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  , ConsCube "Con"   c7  c2  c15 c4  c6  c14 c21 c8  c9  c10 c11 c3
                     c5 c13  c23 c16 c17 c18 c19 c1  c20 c22 c12 c24 rotated
  ) => Rotate F  cube rotated

instance rotateF' ::
  ( RotatePath
      (Path F (Path F (Path F PNil)))
      cube rotated
  ) => Rotate F' cube rotated

instance rotateR  ::
  ( RotatePath
      (Path Y (Path F (Path Y' PNil)))
      cube rotated
  ) => Rotate R  cube rotated

instance rotateR' ::
  ( RotatePath
      (Path R (Path R (Path R PNil)))
      cube rotated
  ) => Rotate R' cube rotated

instance rotateB  ::
  ( RotatePath
      (Path Y (Path Y (Path F (Path Y (Path Y PNil)))))
      cube rotated
  ) => Rotate B  cube rotated

instance rotateB' ::
  ( RotatePath
      (Path B (Path B (Path B PNil)))
      cube rotated
  ) => Rotate B' cube rotated

instance rotateU  ::
  ( RotatePath
      (Path X' (Path F (Path X PNil)))
      cube rotated
  ) => Rotate U  cube rotated

instance rotateU' ::
  ( RotatePath
      (Path U (Path U (Path U PNil)))
      cube rotated
  ) => Rotate U' cube rotated

instance rotateL  ::
  ( RotatePath
      (Path Y' (Path F (Path Y PNil)))
      cube rotated
  ) => Rotate L  cube rotated

instance rotateL' ::
  ( RotatePath
      (Path L (Path L (Path L PNil)))
      cube rotated
  ) => Rotate L' cube rotated

instance rotateD  ::
  ( RotatePath
      (Path X (Path F (Path X' PNil)))
      cube rotated
  ) => Rotate D  cube rotated

instance rotateD' ::
  ( RotatePath
      (Path D (Path D (Path D PNil)))
      cube rotated
  ) => Rotate D' cube rotated

instance rotateX ::
  ( ConsCube "DeCon" c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
                     c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  , ConsCube "Con"   c3  c1  c4  c2  c7  c8  c9  c10 c11 c12 c5  c6
                     c15 c16 c17 c18 c19 c20 c13 c14 c22 c24 c21 c23 rotated
  ) => Rotate X  cube rotated

instance rotateX' ::
  ( RotatePath
      (Path X (Path X (Path X PNil)))
      cube rotated
  ) => Rotate X' cube rotated

instance rotateY  ::
  ( RotatePath
      (Path U (Path D' PNil))
      cube rotated
  ) => Rotate Y  cube rotated

instance rotateY' ::
  ( RotatePath
      (Path Y (Path Y (Path Y PNil)))
      cube rotated
  ) => Rotate Y' cube rotated

instance rotateZ  ::
  ( RotatePath
      (Path F (Path B' PNil))
      cube rotated
  ) => Rotate Z  cube rotated

instance rotateZ' ::
  ( RotatePath
      (Path Z (Path Z (Path Z PNil)))
      cube rotated
  ) => Rotate Z' cube rotated

次に、全探索候補を追加する型クラスEnqueueAllNotationにも回転方法を追加します。

class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'

instance enqueueAllPath ::
  ( TypeEquals (QProxy queue) (QProxy q')

  , AppendPath currPath (Path F  PNil) pF
  , Enqueue q'  pF  qF

  , AppendPath currPath (Path F' PNil) pF'
  , Enqueue qF  pF' qF'

  , AppendPath currPath (Path R  PNil) pR
  , Enqueue qF' pR  qR

  , AppendPath currPath (Path R' PNil) pR'
  , Enqueue qR  pR' qR'

  , AppendPath currPath (Path B  PNil) pB
  , Enqueue qR' pB  qB

  , AppendPath currPath (Path B' PNil) pB'
  , Enqueue qB  pB' qB'

  , AppendPath currPath (Path U  PNil) pU
  , Enqueue qB' pU  qU

  , AppendPath currPath (Path U' PNil) pU'
  , Enqueue qU  pU' qU'

  , AppendPath currPath (Path L  PNil) pL
  , Enqueue qU' pL  qL

  , AppendPath currPath (Path L' PNil) pL'
  , Enqueue qL  pL' qL'

  , AppendPath currPath (Path D  PNil) pD
  , Enqueue qL' pD  qD

  , AppendPath currPath (Path D' PNil) pD'
  , Enqueue qD  pD' qD'

  , AppendPath currPath (Path X  PNil) pX
  , Enqueue qD' pX  qX

  , AppendPath currPath (Path X' PNil) pX'
  , Enqueue qX  pX' qX'

  , AppendPath currPath (Path Y  PNil) pY
  , Enqueue qX' pY  qY

  , AppendPath currPath (Path Y' PNil) pY'
  , Enqueue qY  pY' qY'

  , AppendPath currPath (Path Z  PNil) pZ
  , Enqueue qY' pZ  qZ

  , AppendPath currPath (Path Z' PNil) pZ'
  , Enqueue qZ  pZ' qZ'

  , TypeEquals (QProxy qZ') (QProxy queue')
  ) => EnqueueAllNotation queue currPath queue'

ここまでのまとめ

ここまでのソースコード（クリックで開きます）

module Main where

import Prelude

import Data.Symbol (class IsSymbol, SProxy(..), reflectSymbol)
import Effect.Console (log)
import Prim.Symbol (class Append, class Cons)
import Type.Data.Boolean (class If)
import Type.Data.Symbol (class Equals)
import Type.Equality (class TypeEquals)

showCube
  :: forall   c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
              c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
   . ConsCube "DeCon"
              c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
              c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  => IsSymbol c1  => IsSymbol c2  => IsSymbol c3  => IsSymbol c4  => IsSymbol c5  => IsSymbol c6
  => IsSymbol c7  => IsSymbol c8  => IsSymbol c9  => IsSymbol c10 => IsSymbol c11 => IsSymbol c12
  => IsSymbol c13 => IsSymbol c14 => IsSymbol c15 => IsSymbol c16 => IsSymbol c17 => IsSymbol c18
  => IsSymbol c19 => IsSymbol c20 => IsSymbol c21 => IsSymbol c22 => IsSymbol c23 => IsSymbol c24
  => SProxy cube -> String
showCube _ =
           " " <> " " <> c1  <> c2
  <> nl <> " " <> " " <> c3  <> c4
  <> nl <> c5  <> c6  <> c7  <> c8  <> c9  <> c10 <> c11 <> c12
  <> nl <> c13 <> c14 <> c15 <> c16 <> c17 <> c18 <> c19 <> c20
  <> nl <> " " <> " " <> c21 <> c22
  <> nl <> " " <> " " <> c23 <> c24

  where
    nl  = "\n"
    c1  = reflectSymbol (SProxy :: SProxy c1 )
    c2  = reflectSymbol (SProxy :: SProxy c2 )
    c3  = reflectSymbol (SProxy :: SProxy c3 )
    c4  = reflectSymbol (SProxy :: SProxy c4 )
    c5  = reflectSymbol (SProxy :: SProxy c5 )
    c6  = reflectSymbol (SProxy :: SProxy c6 )
    c7  = reflectSymbol (SProxy :: SProxy c7 )
    c8  = reflectSymbol (SProxy :: SProxy c8 )
    c9  = reflectSymbol (SProxy :: SProxy c9 )
    c10 = reflectSymbol (SProxy :: SProxy c10)
    c11 = reflectSymbol (SProxy :: SProxy c11)
    c12 = reflectSymbol (SProxy :: SProxy c12)
    c13 = reflectSymbol (SProxy :: SProxy c13)
    c14 = reflectSymbol (SProxy :: SProxy c14)
    c15 = reflectSymbol (SProxy :: SProxy c15)
    c16 = reflectSymbol (SProxy :: SProxy c16)
    c17 = reflectSymbol (SProxy :: SProxy c17)
    c18 = reflectSymbol (SProxy :: SProxy c18)
    c19 = reflectSymbol (SProxy :: SProxy c19)
    c20 = reflectSymbol (SProxy :: SProxy c20)
    c21 = reflectSymbol (SProxy :: SProxy c21)
    c22 = reflectSymbol (SProxy :: SProxy c22)
    c23 = reflectSymbol (SProxy :: SProxy c23)
    c24 = reflectSymbol (SProxy :: SProxy c24)

foreign import kind Notation

foreign import data F  :: Notation
foreign import data F' :: Notation
foreign import data R  :: Notation
foreign import data R' :: Notation
foreign import data B  :: Notation
foreign import data B' :: Notation
foreign import data U  :: Notation
foreign import data U' :: Notation
foreign import data L  :: Notation
foreign import data L' :: Notation
foreign import data D  :: Notation
foreign import data D' :: Notation
foreign import data X  :: Notation
foreign import data X' :: Notation
foreign import data Y  :: Notation
foreign import data Y' :: Notation
foreign import data Z  :: Notation
foreign import data Z' :: Notation

foreign import kind Path
foreign import data Path :: Notation -> Path -> Path
foreign import data PNil :: Path

data PProxy (p :: Path) = PProxy

class AppendPath (pl :: Path) (pr :: Path) (plr :: Path) | pl pr -> plr

instance appendPathNil :: AppendPath PNil pr pr

instance appendPath ::
  ( AppendPath tail pr plr'
  , TypeEquals (PProxy (Path head plr')) (PProxy plr)
  ) => AppendPath (Path head tail) pr plr

class HeadPath (p :: Path) (head :: Notation) (tail :: Path) | p -> head tail

instance headPath :: HeadPath (Path head tail) head tail

foreign import kind Queue
foreign import data Queue :: Path -> Queue -> Queue
foreign import data QNil  :: Queue

data QProxy (q :: Queue) = QProxy

class Enqueue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue path -> queue'

instance enqueueNil :: Enqueue QNil path (Queue path QNil)

instance enqueue ::
  ( Enqueue tail newPath q'
  , TypeEquals (QProxy (Queue path q')) (QProxy queue')
  ) => Enqueue (Queue path tail) newPath queue'

class Dequeue (queue :: Queue) (path :: Path) (queue' :: Queue) | queue -> path queue'

instance dequeueNil :: Dequeue (Queue path tail) path tail
instance dequeue :: Dequeue QNil PNil QNil

class EnqueueAllNotation (queue :: Queue) (currPath :: Path) (queue' :: Queue) | queue -> queue'

instance enqueueAllPath ::
  ( TypeEquals (QProxy queue) (QProxy q')

  , AppendPath currPath (Path F  PNil) pF
  , Enqueue q'  pF  qF

  , AppendPath currPath (Path F' PNil) pF'
  , Enqueue qF  pF' qF'

  , AppendPath currPath (Path R  PNil) pR
  , Enqueue qF' pR  qR

  , AppendPath currPath (Path R' PNil) pR'
  , Enqueue qR  pR' qR'

  , AppendPath currPath (Path B  PNil) pB
  , Enqueue qR' pB  qB

  , AppendPath currPath (Path B' PNil) pB'
  , Enqueue qB  pB' qB'

  , AppendPath currPath (Path U  PNil) pU
  , Enqueue qB' pU  qU

  , AppendPath currPath (Path U' PNil) pU'
  , Enqueue qU  pU' qU'

  , AppendPath currPath (Path L  PNil) pL
  , Enqueue qU' pL  qL

  , AppendPath currPath (Path L' PNil) pL'
  , Enqueue qL  pL' qL'

  , AppendPath currPath (Path D  PNil) pD
  , Enqueue qL' pD  qD

  , AppendPath currPath (Path D' PNil) pD'
  , Enqueue qD  pD' qD'

  , AppendPath currPath (Path X  PNil) pX
  , Enqueue qD' pX  qX

  , AppendPath currPath (Path X' PNil) pX'
  , Enqueue qX  pX' qX'

  , AppendPath currPath (Path Y  PNil) pY
  , Enqueue qX' pY  qY

  , AppendPath currPath (Path Y' PNil) pY'
  , Enqueue qY  pY' qY'

  , AppendPath currPath (Path Z  PNil) pZ
  , Enqueue qY' pZ  qZ

  , AppendPath currPath (Path Z' PNil) pZ'
  , Enqueue qZ  pZ' qZ'

  , TypeEquals (QProxy qZ') (QProxy queue')
  ) => EnqueueAllNotation queue currPath queue'

class Solve (cube :: Symbol) (path :: Path) | cube -> path

instance initSolve ::
  (SolveImpl cube "RRRRWWBBYYGGWWBBYYGGOOOO" prev QNil PNil path) => Solve cube path

class SolveImpl
  (cube :: Symbol)
  (goal :: Symbol)
  (prevCube :: Symbol)
  (queue :: Queue)
  (currPath :: Path)
  (path :: Path)
  | cube goal -> path

instance solved :: SolveImpl goal goal prev queue currPath PNil
else instance solved' :: SolveImpl cube goal goal queue currPath path

else instance solveImpl ::
  ( EnqueueAllNotation queue currPath q
  , Dequeue q pHead qTail
  , RotatePath pHead cube rotated
  , Equals rotated goal isEq
  , If isEq (PProxy pHead) (PProxy path) (PProxy path)
  , SolveImpl cube goal rotated qTail pHead path
  ) => SolveImpl cube goal prev queue currPath path

class RotatePath (path :: Path) (cube :: Symbol) (rotated :: Symbol) | cube path -> rotated

instance rotatedPathNil :: RotatePath PNil cube cube

instance rotatedPath ::
  ( Rotate notation cube cube'
  , RotatePath tail cube' cube''
  , TypeEquals (SProxy cube'') (SProxy rotated)
  ) => RotatePath (Path notation tail) cube rotated

class ConsCube
  (mode :: Symbol)
  (c1  :: Symbol) (c2  :: Symbol) (c3  :: Symbol) (c4  :: Symbol)
  (c5  :: Symbol) (c6  :: Symbol) (c7  :: Symbol) (c8  :: Symbol)
  (c9  :: Symbol) (c10 :: Symbol) (c11 :: Symbol) (c12 :: Symbol)
  (c13 :: Symbol) (c14 :: Symbol) (c15 :: Symbol) (c16 :: Symbol)
  (c17 :: Symbol) (c18 :: Symbol) (c19 :: Symbol) (c20 :: Symbol)
  (c21 :: Symbol) (c22 :: Symbol) (c23 :: Symbol) (c24 :: Symbol) (cube :: Symbol)
  | mode
    c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
    c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24
    -> cube
  , mode
    cube ->
    c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
    c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24

instance deConsCube ::
  ( Cons c1  t1  cube, Cons c2  t2  t1 , Cons c3  t3  t2 , Cons c4  t4  t3
  , Cons c5  t5  t4  , Cons c6  t6  t5 , Cons c7  t7  t6 , Cons c8  t8  t7
  , Cons c9  t9  t8  , Cons c10 t10 t9 , Cons c11 t11 t10, Cons c12 t12 t11
  , Cons c13 t13 t12 , Cons c14 t14 t13, Cons c15 t15 t14, Cons c16 t16 t15
  , Cons c17 t17 t16 , Cons c18 t18 t17, Cons c19 t19 t18, Cons c20 t20 t19
  , Cons c21 t21 t20 , Cons c22 t22 t21, Cons c23 t23 t22, Cons c24 ""  t23
  ) => ConsCube "DeCon"
         c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
         c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube

else instance consCube ::
  ( Cons   c1  ""  t1 , Cons   t1  c2  t2 , Append t2  c3  t3 , Append t3  c4  t4
  , Append t4  c5  t5 , Append t5  c6  t6 , Append t6  c7  t7 , Append t7  c8  t8
  , Append t8  c9  t9 , Append t9  c10 t10, Append t10 c11 t11, Append t11 c12 t12
  , Append t12 c13 t13, Append t13 c14 t14, Append t14 c15 t15, Append t15 c16 t16
  , Append t16 c17 t17, Append t17 c18 t18, Append t18 c19 t19, Append t19 c20 t20
  , Append t20 c21 t21, Append t21 c22 t22, Append t22 c23 t23, Append t23 c24 cube
  ) => ConsCube "Con"
         c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
         c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube

class Rotate (notation :: Notation) (cube :: Symbol) (rotated :: Symbol) | notation cube -> rotated

instance rotateF ::
  ( ConsCube "DeCon" c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
                     c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  , ConsCube "Con"   c7  c2  c15 c4  c6  c14 c21 c8  c9  c10 c11 c3
                     c5 c13  c23 c16 c17 c18 c19 c1  c20 c22 c12 c24 rotated
  ) => Rotate F  cube rotated

instance rotateF' ::
  ( RotatePath
      (Path F (Path F (Path F PNil)))
      cube rotated
  ) => Rotate F' cube rotated

instance rotateR  ::
  ( RotatePath
      (Path Y (Path F (Path Y' PNil)))
      cube rotated
  ) => Rotate R  cube rotated

instance rotateR' ::
  ( RotatePath
      (Path R (Path R (Path R PNil)))
      cube rotated
  ) => Rotate R' cube rotated

instance rotateB  ::
  ( RotatePath
      (Path Y (Path Y (Path F (Path Y (Path Y PNil)))))
      cube rotated
  ) => Rotate B  cube rotated

instance rotateB' ::
  ( RotatePath
      (Path B (Path B (Path B PNil)))
      cube rotated
  ) => Rotate B' cube rotated

instance rotateU  ::
  ( RotatePath
      (Path X' (Path F (Path X PNil)))
      cube rotated
  ) => Rotate U  cube rotated

instance rotateU' ::
  ( RotatePath
      (Path U (Path U (Path U PNil)))
      cube rotated
  ) => Rotate U' cube rotated

instance rotateL  ::
  ( RotatePath
      (Path Y' (Path F (Path Y PNil)))
      cube rotated
  ) => Rotate L  cube rotated

instance rotateL' ::
  ( RotatePath
      (Path L (Path L (Path L PNil)))
      cube rotated
  ) => Rotate L' cube rotated

instance rotateD  ::
  ( RotatePath
      (Path X (Path F (Path X' PNil)))
      cube rotated
  ) => Rotate D  cube rotated

instance rotateD' ::
  ( RotatePath
      (Path D (Path D (Path D PNil)))
      cube rotated
  ) => Rotate D' cube rotated

instance rotateX ::
  ( ConsCube "DeCon" c1  c2  c3  c4  c5  c6  c7  c8  c9  c10 c11 c12
                     c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 cube
  , ConsCube "Con"   c3  c1  c4  c2  c7  c8  c9  c10 c11 c12 c5  c6
                     c15 c16 c17 c18 c19 c20 c13 c14 c22 c24 c21 c23 rotated
  ) => Rotate X  cube rotated

instance rotateX' ::
  ( RotatePath
      (Path X (Path X (Path X PNil)))
      cube rotated
  ) => Rotate X' cube rotated

instance rotateY  ::
  ( RotatePath
      (Path U (Path D' PNil))
      cube rotated
  ) => Rotate Y  cube rotated

instance rotateY' ::
  ( RotatePath
      (Path Y (Path Y (Path Y PNil)))
      cube rotated
  ) => Rotate Y' cube rotated

instance rotateZ  ::
  ( RotatePath
      (Path F (Path B' PNil))
      cube rotated
  ) => Rotate Z  cube rotated

instance rotateZ' ::
  ( RotatePath
      (Path Z (Path Z (Path Z PNil)))
      cube rotated
  ) => Rotate Z' cube rotated

回転方法をすべて定義したので、これでどんなにシャッフルされたキューブが来ても解けるはずです。