module Data.HSet
( HSet(..)
, HGet(..)
) where
data Nat = Z | S Nat
type family Elem (typ :: *) (typs :: [*]) :: Bool where
Elem typ '[] = 'False
Elem typ (typ ': typs) = 'True
Elem typ1 (typ2 ': typs) = Elem typ1 typs
type family Index (typ :: *) (typs :: [*]) :: Nat where
Index t (t ': ts) = 'Z
Index t (tt ': ts) = 'S (Index t ts)
data HSet (elems :: [*]) where
HSNil :: HSet '[]
HSCons :: ('False ~ (Elem elem elems)) => elem -> HSet elems -> HSet (elem ': elems)
class (i ~ (Index e els)) => HGet els e i where
hget :: HSet els -> e
instance HGet (e ': els) e 'Z where
hget (HSCons e _) = e
instance (i ~ (Index e els), ('S i) ~ (Index e (e1 ': els)), HGet els e i) => HGet (e1 ': els) e ('S i) where
hget (HSCons _ els) = hget els
fun :: HSet '[Int, Double, Integer, Float]
fun = HSCons 1
$ HSCons 2
$ HSCons 3
$ HSCons 4
$ HSNil
funInt :: Int
funInt = hget fun
funDoube :: Double
funDoube = hget fun
funInteger :: Integer
funInteger = hget fun
funFloat :: Float
funFloat = hget fun