summaryrefslogtreecommitdiff
path: root/src/Propellor/Types/Singletons.hs
diff options
context:
space:
mode:
authorJoey Hess2016-03-27 18:32:01 -0400
committerJoey Hess2016-03-27 18:32:01 -0400
commit500635568514bc106597a857c60d268dcf668037 (patch)
tree8c8b036b6526e83f88a0b83944e30c128ccad8e1 /src/Propellor/Types/Singletons.hs
parent7e76731a0098a6cd47979c86c8a484cc47e0b0d7 (diff)
split out singletons lib
Diffstat (limited to 'src/Propellor/Types/Singletons.hs')
-rw-r--r--src/Propellor/Types/Singletons.hs17
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Propellor/Types/Singletons.hs b/src/Propellor/Types/Singletons.hs
new file mode 100644
index 00000000..be777ecb
--- /dev/null
+++ b/src/Propellor/Types/Singletons.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs #-}
+
+module Propellor.Types.Singletons where
+
+-- | The data family of singleton types.
+data family Sing (x :: k)
+
+-- | A class used to pass singleton values implicitly.
+class SingI t where
+ sing :: Sing t
+
+-- Lists of singletons
+data instance Sing (x :: [k]) where
+ Nil :: Sing '[]
+ Cons :: Sing x -> Sing xs -> Sing (x ': xs)
+instance (SingI x, SingI xs) => SingI (x ': xs) where sing = Cons sing sing
+instance SingI '[] where sing = Nil