Data.Singletons.Prelude

Mimics the Haskell Prelude, but with singleton types. Includes the basic singleton definitions. Note: This is currently very incomplete!

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Basic singleton definitions

module Data.Singletons

data family Sing a

The singleton kind-indexed data family.

Though Haddock doesn't show it, the Sing instance above includes the following instances

 data instance Sing (a :: Bool) where
   SFalse :: Sing False
   STrue  :: Sing True

 data instance Sing (a :: [k]) where
   SNil  :: Sing '[]
   SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)

 data instance Sing (a :: Maybe k) where
   SNothing :: Sing Nothing
   SJust    :: Sing (a :: k) -> Sing (Just a)

 data instance Sing (a :: Either x y) where
   SLeft  :: Sing (a :: x) -> Sing (Left a)
   SRight :: Sing (b :: y) -> Sing (Right b)

 data instance Sing (a :: Ordering) where
   SLT :: Sing LT
   SEQ :: Sing EQ
   SGT :: Sing GT

 data instance Sing (a :: ()) where
   STuple0 :: Sing '()

 data instance Sing (z :: (a, b)) where
   STuple2 :: Sing a -> Sing b -> Sing '(a, b)

 data instance Sing (z :: (a, b, c)) where
   STuple3 :: Sing a -> Sing b -> Sing c -> Sing '(a, b, c)

 data instance Sing (z :: (a, b, c, d)) where
   STuple4 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing '(a, b, c, d)

 data instance Sing (z :: (a, b, c, d, e)) where
   STuple5 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing '(a, b, c, d, e)

 data instance Sing (z :: (a, b, c, d, e, f)) where
   STuple6 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing f
           -> Sing '(a, b, c, d, e, f)

 data instance Sing (z :: (a, b, c, d, e, f, g)) where
   STuple7 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing f
           -> Sing g -> Sing '(a, b, c, d, e, f, g)

Singleton type synonyms

These synonyms are all kind-restricted synonyms of Sing. For example SBool requires an argument of kind Bool.

type SBool z = Sing z

type SList z = Sing z

type SMaybe z = Sing z

type SEither z = Sing z

type STuple0 z = Sing z

type STuple2 z = Sing z

type STuple3 z = Sing z

type STuple4 z = Sing z

type STuple5 z = Sing z

type STuple6 z = Sing z

type STuple7 z = Sing z

Functions working with Bool

type family If cond tru fls :: k

Type-level If. If True a b ==> a; If False a b ==> b

sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)

Conditional over singletons

type family Not a :: Bool

Type-level not

sNot :: SBool a -> SBool (Not a)

type :&& a b = a && b

type :|| a b = a || b

(%:&&) :: SBool a -> SBool b -> SBool (a :&& b)

(%:||) :: SBool a -> SBool b -> SBool (a :|| b)

Functions working with lists

type family Head a :: a

type family Tail a :: [a]

type family a :++ a :: [a]

(%:++) :: forall t t. Sing t -> Sing t -> Sing (:++ t t)

Singleton equality

module Data.Singletons.Eq

Other datatypes

type family Maybe_ a a a :: b

sMaybe_ :: forall t t t. Sing t -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Maybe_ t t t)

type family Either_ a a a :: c

sEither_ :: forall t t t. (forall t. Sing t -> Sing (t t)) -> (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing (Either_ t t t)

type family Fst a :: a

sFst :: forall t. Sing t -> Sing (Fst t)

type family Snd a :: b

sSnd :: forall t. Sing t -> Sing (Snd t)

type family Curry a a a :: c

sCurry :: forall t t t. (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing t -> Sing (Curry t t t)

type family Uncurry a a :: c

sUncurry :: forall t t. (forall t. Sing t -> forall t. Sing t -> Sing (t t t)) -> Sing t -> Sing (Uncurry t t)