singletons-0.10.0: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude

Contents

Description

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.

Synopsis

Basic singleton definitions

module Data.Singletons

data family Sing a Source

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *) 
SDecide k (KProxy k) => TestEquality k (Sing k) 
data Sing Bool where 
data Sing Ordering where 
data Sing * where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

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 Source

type SList z = Sing z Source

type SMaybe z = Sing z Source

type SEither z = Sing z Source

type SOrdering z = Sing z Source

type STuple0 z = Sing z Source

type STuple2 z = Sing z Source

type STuple3 z = Sing z Source

type STuple4 z = Sing z Source

type STuple5 z = Sing z Source

type STuple6 z = Sing z Source

type STuple7 z = Sing z Source

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) Source

Conditional over singletons

type family Not a :: Bool

Type-level "not"

Equations

Not False = True 
Not True = False 

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

type (:&&) a b = a && b Source

type (:||) a b = a || b Source

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

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

Functions working with lists

type family Head a :: a Source

Equations

Head ((:) a z) = a 
Head [] = Error "Data.Singletons.List.head: empty list" 

type family Tail a :: [a] Source

Equations

Tail ((:) z t) = t 
Tail [] = Error "Data.Singletons.List.tail: empty list" 

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

Equations

[] :++ a = a 
((:) h t) :++ a = (:) h ((:++) t a) 

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

Error reporting

type family Error str :: k Source

The promotion of error

sError :: Sing (str :: Symbol) -> a Source

The singleton for error

Singleton equality

module Data.Singletons.Eq

Other datatypes

type family Maybe_ a a a :: b Source

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) Source

type family Either_ a a a :: c Source

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) Source

type family Fst a :: a Source

Equations

Fst `(x, z)` = x 

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

type family Snd a :: b Source

Equations

Snd `(z, y)` = y 

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

type family Curry a a a :: c Source

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) Source

type family Uncurry a a :: c Source

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) Source