summaryrefslogtreecommitdiff
path: root/src/Propellor/Types/Singletons.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Propellor/Types/Singletons.hs')
-rw-r--r--src/Propellor/Types/Singletons.hs49
1 files changed, 49 insertions, 0 deletions
diff --git a/src/Propellor/Types/Singletons.hs b/src/Propellor/Types/Singletons.hs
new file mode 100644
index 00000000..f2089ee8
--- /dev/null
+++ b/src/Propellor/Types/Singletons.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE CPP, DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, UndecidableInstances #-}
+
+-- | Simple implementation of singletons, portable back to ghc 7.6.3
+
+module Propellor.Types.Singletons (
+ module Propellor.Types.Singletons,
+ KProxy(..)
+) where
+
+#if __GLASGOW_HASKELL__ > 707
+import Data.Proxy (KProxy(..))
+#else
+data KProxy (a :: *) = KProxy
+#endif
+
+-- | 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
+
+data instance Sing (x :: Bool) where
+ TrueS :: Sing 'True
+ FalseS :: Sing 'False
+instance SingI 'True where sing = TrueS
+instance SingI 'False where sing = FalseS
+
+class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where
+ type DemoteRep kparam :: *
+ -- | From singleton to value.
+ fromSing :: Sing (a :: k) -> DemoteRep kparam
+
+instance SingKind ('KProxy :: KProxy a) => SingKind ('KProxy :: KProxy [a]) where
+ type DemoteRep ('KProxy :: KProxy [a]) = [DemoteRep ('KProxy :: KProxy a)]
+ fromSing Nil = []
+ fromSing (Cons x xs) = fromSing x : fromSing xs
+
+instance SingKind ('KProxy :: KProxy Bool) where
+ type DemoteRep ('KProxy :: KProxy Bool) = Bool
+ fromSing FalseS = False
+ fromSing TrueS = True