deal.hs

{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators, UndecidableInstances #-}

data Z
data S n
data Nil
data x :<: xs
infixr 5 :<:
data Yes
data No

type family Pred n
type instance Pred (S n) = n

type family Null xs
type instance Null Nil = Yes
type instance Null (x :<: xs) = No

type family Take n xs
type instance Take Z xs = Nil
type instance Take n Nil = Nil
type instance Take (S n) (x :<: xs) = x :<: Take n xs

type family Drop n xs
type instance Drop Z xs = xs
type instance Drop n Nil = Nil
type instance Drop (S n) (x :<: xs) = Drop n xs

type Divide n xs = DivideBool (Null (Drop (Pred n) xs)) n xs
type family DivideBool b n xs
type instance DivideBool Yes n xs = Nil
type instance DivideBool No n xs = Take n xs :<: Divide n (Drop n xs)

type family Transpose xss
type instance Transpose Nil = Nil
type instance Transpose (Nil :<: xss) = Transpose xss
type instance Transpose ((x :<: xs) :<: xss) = (x :<: Heads xss) :<: Transpose (xs :<: Tails xss)

type family Heads xss
type instance Heads Nil = Nil
type instance Heads ((x :<: xs) :<: xss) = x :<: Heads xss

type family Tails xss
type instance Tails Nil = Nil
type instance Tails ((x :<: xs) :<: xss) = xs :<: Tails xss

type Deal n xs = Transpose (Divide n xs)

-- test
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three
data A
data B
data C

type Ls = A :<: B :<: C :<: A :<: B :<: C :<: A :<: B :<: C :<: Nil

type Test1 = Deal Three Ls
type Expected1 = (A :<: A :<: A :<: Nil) :<: (B :<: B :<: B :<: Nil) :<: (C :<: C :<: C :<: Nil) :<: Nil
test1 :: Test1
test1 = undefined
expected1 :: Expected1
expected1 = test1

type Test2 = Deal Four Ls
type Expected2 = (A :<: B :<: Nil) :<: (B :<: C :<: Nil) :<: (C :<: A :<: Nil) :<: (A :<: B :<: Nil) :<: Nil
test2 :: Test2
test2 = undefined
expected2 :: Expected2
expected2 = test2