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.

Instances

TestCoercion * (Sing *)

SDecide k (KProxy k) => TestEquality k (Sing k)

data Sing Bool where

• SFalse :: (~) Bool z False => Sing Bool z
• STrue :: (~) Bool z True => Sing Bool z

data Sing Ordering where

• SLT :: (~) Ordering z LT => Sing Ordering z
• SEQ :: (~) Ordering z EQ => Sing Ordering z
• SGT :: (~) Ordering z GT => Sing Ordering z

data Sing * where

• STypeRep :: Typeable * a => Sing * a

data Sing Nat = SNat Integer

data Sing Symbol = SSym String

data Sing () where

• STuple0 :: (~) () z () => Sing () z

data Sing [a0] where

• SNil :: (~) [a] z ([] a) => Sing [a] z
• SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z

data Sing (Maybe a0) where

• SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z
• SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z

data Sing (Either a0 b0) where

• SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z
• SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z

data Sing ((,,) a0 b0 c0) where

• STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z

data Sing ((,,,) a0 b0 c0 d0) where

• STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z

data Sing ((,,,,) a0 b0 c0 d0 e0) where

• STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z

data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where

• STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z

data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where

• STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z

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

Equations

If k True tru fls = tru

If k False tru fls = fls

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

Conditional over singletons

type family Not a :: Bool

Type-level "not"

Equations

Not False = True

Not True = False

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

Equations

Head ((:) a z) = a

Head [] = Error "Data.Singletons.List.head: empty list"

type family Tail a :: [a]

Equations

Tail ((:) z t) = t

Tail [] = Error "Data.Singletons.List.tail: empty list"

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

Equations

[] :++ a = a

((:) h t) :++ a = (:) h ((:++) t 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

Equations

Maybe_ n z Nothing = n

Maybe_ z f (Just x) = f x

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

Equations

Either_ f z (Left x) = f x

Either_ z g (Right y) = g y

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

Equations

Fst `(x, z)` = x

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

type family Snd a :: b

Equations

Snd `(z, y)` = y

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

type family Curry a a a :: c

Equations

Curry f x y = f `(x, y)`

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

Equations

Uncurry f p = f (Fst p) (Snd p)

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