type-level insertion and quick sort

gistfile1.hs

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

-- bools
data True
data False

type family Or a b
type instance Or True True   = True
type instance Or True False  = True
type instance Or False True  = True
type instance Or False False = False

type family If c a b
type instance If True a b  = a
type instance If False a b = b

-- nats
data Zero 
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four  = Succ Three

data LT
data EQ
data GT

type family Compare a b
type instance Compare Zero Zero         = EQ
type instance Compare (Succ a) Zero     = GT
type instance Compare Zero (Succ a)     = LT
type instance Compare (Succ a) (Succ b) = Compare a b

type family IsLT a
type instance IsLT LT = True
-- type instance IsLT a = False -- conflicting family instance declaraitons blahblahblah
type instance IsLT GT = False
type instance IsLT EQ = False

type family IsGT a
type instance IsGT GT = True
type instance IsGT LT = False
type instance IsGT EQ = False

type family IsEQ a
type instance IsEQ EQ = True
type instance IsEQ LT = False
type instance IsEQ GT = False

type family Less a b
type instance Less a b = IsLT (Compare a b)

type family More a b
type instance More a b = IsGT (Compare a b)

type family Equals a b
type instance Equals a b = IsEQ (Compare a b)

type family Max a b 
type instance Max a b = If (Less a b) b a

type family Min a b
type instance Min a b = If (Less a b) a b

-- lists
data Nil 
data Cons a b

type family Filter (f :: * -> *) l
type instance Filter f Nil         = Nil
type instance Filter f (Cons x xs) = If (f x) (Cons x (Filter f xs)) (Filter f xs)

type family Foldl (f :: * -> * -> *) a x
type instance Foldl f a Nil         = a
type instance Foldl f a (Cons x xs) = Foldl f (f a x) xs

type family Foldr (f :: * -> * -> *) a x
type instance Foldr f a Nil         = a
type instance Foldr f a (Cons x xs) = f x (Foldr f a xs)

type family Concat p q
type instance Concat p q = Foldr Cons q p

-- insertion sort
type family ISort a 
type instance ISort Nil         = Nil
type instance ISort (Cons x xs) = Insert x (ISort xs)

type family Insert a l
type instance Insert a Nil         = Cons a Nil
type instance Insert a (Cons x xs) = If (Less a x) 
                                        (Cons a (Cons x xs)) 
                                        (Cons x (Insert a xs))

-- quick sort
-- Filter (More a) is seems to be a something disallowed, so type families do not support partial application probably
-- thus we need specialized filter for qsort
type family FilterMoreEq a l
type instance FilterMoreEq a Nil = Nil
type instance FilterMoreEq a (Cons x xs) = If (Or (More x a) (Equals x a)) 
                                              (Cons x (FilterMoreEq a xs)) 
                                              (FilterMoreEq a xs)

type family FilterLess a l
type instance FilterLess a Nil = Nil
type instance FilterLess a (Cons x xs) = If (Less x a) 
                                            (Cons x (FilterLess a xs)) 
                                            (FilterLess a xs)

type family QSort a
type instance QSort Nil = Nil
type instance QSort (Cons a xs) = (Concat 
                                    (QSort (FilterLess a xs)) 
                                    (Cons a 
                                       (QSort (FilterMoreEq a xs))))