Fast set union w/ type-level lists

Main.hs

{-# LANGUAGE TypeFamilies
           , DataKinds
           , PolyKinds
           , UndecidableInstances
           , DeriveGeneric
           , TypeOperators #-}
module Main where

import           GHC.Generics
import           GHC.TypeLits
import           Prelude

newtype X0  = X0  Int deriving (Generic, Show)
newtype X1  = X1  Int deriving (Generic, Show)
newtype X2  = X2  Int deriving (Generic, Show)
newtype X3  = X3  Int deriving (Generic, Show)
newtype X4  = X4  Int deriving (Generic, Show)
newtype X5  = X5  Int deriving (Generic, Show)
newtype X6  = X6  Int deriving (Generic, Show)
newtype X7  = X7  Int deriving (Generic, Show)
newtype X8  = X8  Int deriving (Generic, Show)
newtype X9  = X9  Int deriving (Generic, Show)
newtype X10 = X10 Int deriving (Generic, Show)
newtype X11 = X11 Int deriving (Generic, Show)
newtype X12 = X12 Int deriving (Generic, Show)
newtype X13 = X13 Int deriving (Generic, Show)
newtype X14 = X14 Int deriving (Generic, Show)
newtype X15 = X15 Int deriving (Generic, Show)
newtype X16 = X16 Int deriving (Generic, Show)
newtype X17 = X17 Int deriving (Generic, Show)
newtype X18 = X18 Int deriving (Generic, Show)
newtype X19 = X19 Int deriving (Generic, Show)

type R0_to_9 = '[
    X0
  , X1
  , X2
  , X3
  , X4
  , X5
  , X6
  , X7
  , X8
  , X9
  ]

type R10_to_19 = '[
    X10
  , X11
  , X12
  , X13
  , X14
  , X15
  , X16
  , X17
  , X18
  , X19
  ]

type R0_to_19 = '[
    X0
  , X1
  , X2
  , X3
  , X4
  , X5
  , X6
  , X7
  , X8
  , X9
  , X10
  , X11
  , X12
  , X13
  , X14
  , X15
  , X16
  , X17
  , X18
  , X19
  ]

verify :: (R0_to_19 :<>: R10_to_19 ~ R0_to_19) => ()
verify = ()

type family TypeName a :: Symbol where
  TypeName Double = "Double"
  TypeName Int = "Int"
  TypeName String = "String"
  TypeName (M1 D ('MetaData name _ _ _) f ()) = name
  TypeName a = TypeName (Rep a ())

type family Cmp (a :: k) (b :: k) :: Ordering where
  Cmp a b = CmpSymbol (TypeName a) (TypeName b)

type family Sort (xs :: [k]) :: [k]  where
  Sort xs = SortHelper xs '[]

type family SortHelper (xs :: [k]) (ys :: [k]) :: [k]  where
  SortHelper '[] ys = ys
  SortHelper (x ': xs) '[] = SortHelper xs '[x]
  SortHelper (x ': xs) (y ': ys) = SortHelper2 (NotEqual (Cmp x y) GT) x xs y ys

type family NotEqual (a :: k) (b :: k) :: Bool where
  NotEqual a a = True
  NotEqual a b = False

type family SortHelper2 (b :: Bool) (x :: k) (xs :: [k]) (y :: k) (ys :: [k]) :: [k]  where
  SortHelper2 False  x xs y ys = SortHelper xs (x ': y ': ys)
  SortHelper2 True x xs y ys = SortHelper xs (y ': InsertSorted x ys)

type family InsertSorted (x :: k) (ys :: [k]) :: [k]  where
  InsertSorted x '[] = '[x]
  InsertSorted x (y ': ys) = InsertSortedHelper (NotEqual (Cmp x y) GT) x y ys

type family InsertSortedHelper (b :: Bool) (x :: k) (y :: k) (ys :: [k]) :: [k]  where
  InsertSortedHelper False  x y ys = x ': y ': ys
  InsertSortedHelper True x y ys = y ': InsertSorted x ys

type family Nub (xs :: [k]) :: [k] where
  Nub '[] = '[]
  Nub (a ': a ': as) = Nub (a ': as)
  Nub (a ': as) = a ': Nub as

type family (:<>:) (xs :: [k]) (ys :: [k]) :: [k] where
  xs :<>: ys = Nub (Sort (xs :++: ys))

type family (:++:) (xs :: [k]) (ys :: [k]) :: [k] where
  xs :++: '[] =  '[]
  (x ': xs) :++: ys = x ': (xs :++: ys)

main :: IO ()
main = print "Hello"

Main2.hs

module Main where

import           GHC.Generics
import           GHC.TypeLits
import           Prelude

newtype X0  = X0  Int deriving (Generic, Show)
newtype X1  = X1  Int deriving (Generic, Show)
newtype X2  = X2  Int deriving (Generic, Show)
newtype X3  = X3  Int deriving (Generic, Show)
newtype X4  = X4  Int deriving (Generic, Show)
newtype X5  = X5  Int deriving (Generic, Show)
newtype X6  = X6  Int deriving (Generic, Show)
newtype X7  = X7  Int deriving (Generic, Show)
newtype X8  = X8  Int deriving (Generic, Show)
newtype X9  = X9  Int deriving (Generic, Show)
newtype X10 = X10 Int deriving (Generic, Show)
newtype X11 = X11 Int deriving (Generic, Show)
newtype X12 = X12 Int deriving (Generic, Show)
newtype X13 = X13 Int deriving (Generic, Show)
newtype X14 = X14 Int deriving (Generic, Show)
newtype X15 = X15 Int deriving (Generic, Show)
newtype X16 = X16 Int deriving (Generic, Show)
newtype X17 = X17 Int deriving (Generic, Show)
newtype X18 = X18 Int deriving (Generic, Show)
newtype X19 = X19 Int deriving (Generic, Show)

type R0_to_9 = '[
    X0
  , X1
  , X2
  , X3
  , X4
  , X5
  , X6
  , X7
  , X8
  , X9
  ]

type R10_to_19 = '[
    X10
  , X11
  , X12
  , X13
  , X14
  , X15
  , X16
  , X17
  , X18
  , X19
  ]

type R0_to_19 = '[
    X0
  , X1
  , X2
  , X3
  , X4
  , X5
  , X6
  , X7
  , X8
  , X9
  , X10
  , X11
  , X12
  , X13
  , X14
  , X15
  , X16
  , X17
  , X18
  , X19
  ]

verify :: ( SetEquals (Union R0_to_19  R10_to_19) R0_to_19 ~ True
          , SetEquals (Union R10_to_19 R0_to_19)  R0_to_19 ~ True
          , SetEquals (Union R0_to_9   R10_to_19) R0_to_19 ~ True
          , SetEquals (Union R10_to_19 R0_to_9)   R0_to_19 ~ True )
          => ()
verify = ()

type family SetEquals (xs :: [k]) (ys :: [k]) :: Bool where
  SetEquals '[] '[]      = True
  SetEquals '[]  ys      = False
  SetEquals (x ': xs) ys = SetEquals xs (Delete x ys '[])

type family Delete (x :: k) (ys :: [k]) (zs :: [k]) :: [k] where
  Delete x '[]       zs = zs
  Delete x (x ': ys) zs = Delete x ys zs
  Delete x (y ': ys) zs = Delete x ys (y ': zs)

type family Union (xs :: [k]) (ys :: [k]) :: [k] where
  Union '[] ys = ys
  Union xs '[] = xs
  Union xs  ys = UnionHelper xs ys '[]

type family UnionHelper (xs :: [k]) (ys :: [k]) (zs :: [k]) :: [k] where
  UnionHelper xs '[] zs = zs :++: xs
  UnionHelper '[] ys zs = zs :++: ys
  UnionHelper (x ': xs) ys zs = UnionHelper xs (Delete x ys '[]) (x ': zs)

type family (:++:) (xs :: [k]) (ys :: [k]) :: [k] where
  '[] :++: ys = ys
  (x ': xs) :++: ys = x ': (xs :++: ys)

main :: IO ()
main = print "Hello"