hpaste

recent | annotate | new

  import Prelude hiding (all, flip, map, filter)
  u = undefined

  data R  -- Red
  data G  -- Green
  data B  -- Blue
  data W  -- White

  data Cube u f r b l d

  type CubeRed = Cube R R R R R R
  type CubeBlue = Cube B B B B B B
  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

  data True
  data False

  type family And b1 b2
  and :: b1 -> b2 -> And b1 b2
  and = u

  type instance And True  True = True
  type instance And True  False= False
  type instance And False True = False
  type instance And False False= False

  data Nil
  data Cons x xs
  data x ::: xs
  infixr 5 :::

  type family ListConcat l1 l2
  listConcat :: l1 -> l2 -> ListConcat l1 l2
  listConcat = u
  type instance ListConcat Nil l = l
  type instance ListConcat (x:::xs) ys = x:::(ListConcat xs ys)

  type family Apply f a 
  apply :: f -> a -> Apply f a
  apply = u

  data Rotation
  data Twist
  data Flip
  type instance Apply Rotation (Cube u f r b l d) = Cube u r b l f d
  type instance Apply Twist    (Cube u f r b l d) = Cube f r u l d b
  type instance Apply Flip     (Cube u f r b l d) = Cube d l b r f u

  type family Map f xs
  map :: f -> xs -> Map f xs
  map = u
  type instance Map f Nil = Nil
  type instance Map f (x:::xs) = Apply f x ::: Map f xs

  type family Filter f xs
  filter :: f -> xs -> Filter f xs
  filter = u
  type instance Filter f Nil = Nil
  type instance Filter f (x:::xs) = AppendIf (Apply f x) x (Filter f xs)

  type family AppendIf b x ys 
  type instance AppendIf True x ys  = x ::: ys
  type instance AppendIf False x ys = ys

  type family MapAppend f xs
  mapAppend :: f -> xs -> MapAppend f xs
  mapAppend = u
  type instance MapAppend f Nil = Nil
  type instance MapAppend f (x:::xs) = ListConcat (x:::xs) (Map f (x:::xs)) 

  type family MapAppend2 f xs 
  mapAppend2 :: f -> xs -> MapAppend2 f xs
  mapAppend2 = u
  type instance MapAppend2 f Nil = Nil
  type instance MapAppend2 f (x:::xs)  = ListConcat (x:::xs) (MapAppend f (Map f (x:::xs)))

  type family MapAppend3 f xs
  mapAppend3 :: f -> xs -> MapAppend3 f xs
  mapAppend3 = u
  type instance MapAppend3 f Nil = Nil
  type instance MapAppend3 f (x:::xs) = ListConcat xs (MapAppend2 f (Map f (x:::xs)))


  data Orientations
  type instance Apply Orientations c = MapAppend3 Rotation (
                                       MapAppend2 Twist (
                                       MapAppend Flip (c:::Nil)))
  type family NE x y
  ne :: x -> y -> NE x y
  ne = u
  type instance NE R R = False
  type instance NE R G = True 
  type instance NE R B = True 
  type instance NE R W = True 
  type instance NE G R = True 
  type instance NE G G = False
  type instance NE G B = True 
  type instance NE G W = True 
  type instance NE B R = True 
  type instance NE B G = True 
  type instance NE B B = False
  type instance NE B W = True 
  type instance NE W R = True 
  type instance NE W G = True 
  type instance NE W B = True 
  type instance NE W W = False

  type family All l 
  all :: l -> All l
  all = u
 
  type instance All Nil = True
  type instance All (False ::: xs) = False
  type instance All (True ::: xs)  = All xs

  type family Compatible c1 c2
  compatible :: c1 -> c2 -> Compatible c1 c2
  compatible = u
  type instance Compatible (Cube u1 f1 r1 b1 l1 d1) (Cube u2 f2 r2 b2 l2 d2) =
      All (NE f1 f2 ::: NE r1 r2 ::: NE b1 b2 ::: NE l1 l2)

  type family Allowed c cs
  allowed :: c -> cs -> Allowed c cs
  allowed = u
  type instance Allowed c Nil = True
  type instance Allowed c (y ::: ys) = And (Compatible c y) (Allowed c ys)

  type family Solutions cs
  solutions :: cs -> Solutions cs
  solutions = u
  type instance Solutions Nil = (Nil ::: Nil)
  type instance Solutions (c ::: cs) = AllowedCombinations (Apply Orientations c) (Solutions cs)

  type family AllowedCombinations os sols
  type instance AllowedCombinations os Nil = Nil
  type instance AllowedCombinations os (s ::: sols) =
      ListConcat (AllowedCombinations os sols) (MatchingOrientations os s)

  type family MatchingOrientations os sol
  type instance MatchingOrientations Nil sol = Nil
  type instance MatchingOrientations (o ::: os) sol =
      AppendIf (Allowed o sol) (o:::sol) (MatchingOrientations os sol)

  type Cubes = (Cube1 ::: Cube2 ::: Cube3 ::: Cube4 ::: Nil)

  solution = solutions (u::Cubes)

  -- Did all this and now I don't know how to reduce the type of solution in order to display it

-- There is unfortunately, no simple way to print the normalised type.  
-- In fact, GHC goes to great length to show types with as little 
-- normalisation as possible to users.  (Especially for error messages, 
-- that usually makes them much easier to understand.)  However, with 
-- type families, I think we really ought to have a ghci command to
-- specifically request a normalised type.  I'll put that on my
-- TODO list!

-- For the moment, you can of course try forcing normalisation by
-- triggering type errors; eg
-- > :t solution :: Int

-- There is unfortunately, no simple way to print the normalised type.  
-- In fact, GHC goes to great length to show types with as little 
-- normalisation as possible to users.  (Especially for error messages, 
-- that usually makes them much easier to understand.)  However, with 
-- type families, I think we really ought to have a ghci command to
-- specifically request a normalised type.  I'll put that on my
-- TODO list!

-- For the moment, you can of course try forcing normalisation by
-- triggering type errors; eg
-- > :t solution :: Int

-- What about a flag, e.g. -fshow-normalized-types ?