Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
- Instant Insanity using Closed Type Families.
- See:
{-# OPTIONS_GHC -ftype-function-depth=400 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Prelude hiding (all, flip, map, filter )
data Proxy a = Proxy
main = print (Proxy :: Proxy (Solutions Cubes))
data R -- Red
data G -- Green
data B -- Blue
data W -- White
data Cube u f r b l d
data True
data False
type family And b1 b2 :: * where
And True True = True
And b1 b2 = False
type family NE x y :: * where
NE x x = False
NE x y = True
type family EQ x y :: * where
EQ a a = True
EQ a b = False
data Nil = Nil
data Cons x xs = Cons x xs
type family All l :: * where
All Nil = True
All (Cons False xs) = False
All (Cons True xs) = All xs
type family ListConcat xs ys :: * where
ListConcat Nil ys = ys
ListConcat (Cons x xs) ys = Cons x (ListConcat xs ys)
type family AppendIf b a as :: * where
AppendIf False a as = as
AppendIf True a as = Cons a as
data Rotate
data Twist
data Flip
type family Apply f a :: * where
Apply Rotate (Cube u f r b l d) = (Cube u r b l f d)
Apply Twist (Cube u f r b l d) = (Cube f r u l d b)
Apply Flip (Cube u f r b l d) = (Cube d l b r f u)
type family Map f as :: * where
Map f Nil = Nil
Map f (Cons a as) = Cons (Apply f a) (Map f as)
type family MapAppend f as :: * where
MapAppend f xs = ListConcat xs (Map f xs)
type family MapAppend2 f as :: * where
MapAppend2 f xs = ListConcat xs (MapAppend f (Map f xs))
type family MapAppend3 f as :: * where
MapAppend3 f xs = ListConcat xs (MapAppend2 f (Map f xs))
type family Iterate2 f as :: * where
Iterate2 f Nil = Nil
Iterate2 f (Cons a as) = ListConcat (Cons (Apply f a) (Cons a Nil)) (Iterate2 f as)
type family Iterate3 f as :: * where
Iterate3 f (Cons a as) =
ListConcat (Cons a
(Cons (Apply f a)
(Cons (Apply f (Apply f a))
(Iterate3 f as)
type family Iterate4 f as :: * where
Iterate4 f Nil = Nil
Iterate4 f (Cons a as) =
ListConcat (Cons a
(Cons (Apply f a)
(Cons (Apply f (Apply f a))
(Cons (Apply f (Apply f (Apply f a)))
(Iterate4 f as)
type family Orientations c :: * where
Orientations c = MapAppend3 Rotate (MapAppend2 Twist (MapAppend Flip (Cons c Nil)))
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
type Cubes = Cons Cube1 (Cons Cube2 (Cons Cube3 (Cons Cube4 Nil)))
type family Compatible c d :: * where
Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) =
All (Cons (NE f1 f2) (Cons (NE r1 r2) (Cons (NE b1 b2) (Cons (NE l1 l2) Nil))))
type family Allowed c cs :: * where
Allowed c Nil = True
Allowed c (Cons s ss) = And (Compatible c s) (Allowed c ss)
type family MatchingOrientations as sol :: * where
MatchingOrientations Nil sol = Nil
MatchingOrientations (Cons o os) sol =
AppendIf (Allowed o sol) (Cons o sol) (MatchingOrientations os sol)
type family AllowedCombinations os sols :: * where
AllowedCombinations os Nil = Nil
AllowedCombinations os (Cons sol sols) =
ListConcat (MatchingOrientations os sol) (AllowedCombinations os sols)
type family Solutions c :: * where
Solutions Nil = Cons Nil Nil
Solutions (Cons c cs) = AllowedCombinations (Orientations c) (Solutions cs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.