typelevel sort

tsort.hs

type Sort a = SortI a '[]

type family SortI a b where
  SortI '[]            b = b
  SortI (a:?n ': as)  '[] = SortI as '[ a :? n]
  SortI (a:?n ': as)  bs = SortI as (Insert (a:?n) bs)

type family Insert a b where
  Insert (a :? n) '[] = '[ a :? n ]
  Insert (a :? n) ( b :? m ': bs) = UnOrdering (CmpSymbol n m)
                                               ((a :? n) ': (b :? m) ': bs)
                                               ((a :? n) ': (b :? m) ': bs)
                                               ((b :? m) ': Insert (a :? n) bs)

type family UnOrdering x a b c where
  UnOrdering 'LT a b c = a
  UnOrdering 'EQ a b c = b
  UnOrdering 'GT a b c = c