Last active
December 26, 2018 00:46
-
-
Save danidiaz/9007ba96650d69b727079c252b758f4d to your computer and use it in GitHub Desktop.
A type-level symbol set.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment