A type-level symbol set.

TypeLevelSymbolSet.hs

{-# LANGUAGE DataKinds, 
             PolyKinds,
             TypeFamilies, 
             UndecidableInstances, 
             FlexibleContexts,
             ScopedTypeVariables, 
             TypeApplications, 
             TypeOperators, 
             ExistentialQuantification,
             DeriveFunctor,
             FlexibleInstances
             #-}
module Main where

import           GHC.TypeLits

data Set a = Nope
           | Node (Set a) a (Set a)

type family Insert (m :: Set Symbol) (v :: Symbol) :: Set Symbol where
    Insert Nope v = Node Nope v Nope
    Insert (Node left val right) v = InsertAux (CmpSymbol val v) left val right v

type family InsertAux (o :: Ordering) (left :: Set Symbol) (val :: Symbol) (right :: Set Symbol) (v :: Symbol) :: Set Symbol where
    InsertAux EQ left val right _ = Node left val right
    InsertAux LT left val right v = Node left val (Insert right v)
    InsertAux GT left val right v = Node (Insert left v) val right

type family MkSymbolSetAux (ns :: [Symbol]) (m :: Set Symbol) :: Set Symbol where
    MkSymbolSetAux '[]       acc = acc
    MkSymbolSetAux (x ': xs) acc = Insert (MkSymbolSetAux xs acc) x

type family MkSymbolSet (ns :: [Symbol]) :: Set Symbol where
    MkSymbolSet ns = MkSymbolSetAux ns Nope

type family Present (m :: Set Symbol) (v :: Symbol) :: Bool where
    Present Nope                  _ = False
    Present (Node left val right) v = PresentAux (CmpSymbol val v) left right v
    
type family PresentAux (o :: Ordering) (left :: Set Symbol) (right :: Set Symbol) (v :: Symbol) :: Bool where
    PresentAux EQ _    _     _ = True
    PresentAux LT _    right v = Present right v
    PresentAux GT left _     v = Present left  v

-- *Main> type Setty = MkSymbolSet ["foo","bar","baz"]
-- *Main> :kind! Setty
-- *Main> :kind! Present Setty "whoopey"
-- Present Setty "whoopey" :: Bool
-- = 'False
-- *Main> :kind! Present Setty "foo"
-- Present Setty "foo" :: Bool
-- = 'True

main :: IO ()
main = do
    return ()