Data.Singletons.Prelude

Contents

• Basic singleton definitions
• Singleton type synonyms
• Functions working with Bool
• Error reporting
• Singleton equality
• Singleton comparisons
  • Miscellaneous functions
• List operations
  • Reducing lists (folds)
    • Special folds
    • Scans
  • Searching lists
  • Zipping and unzipping lists
• Other datatypes
• Other functions
• Defunctionalization symbols

Description

Synopsis

• module Data.Singletons
• data family Sing a
• type SBool z = Sing z
• type SList z = Sing z
• type SMaybe z = Sing z
• type SEither z = Sing z
• type SOrdering 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
• type family If cond tru fls :: k
• sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
• type family Not a :: Bool
• sNot :: forall t. Sing t -> Sing (Apply NotSym0 t)
• type family a :&& a :: Bool
• type family a :|| a :: Bool
• (%:&&) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:&&$) t) t)
• (%:||) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:||$) t) t)
• type Otherwise = (TrueSym0 :: Bool)
• sOtherwise :: Sing OtherwiseSym0
• type family Error str :: k
• data ErrorSym0 t1
• sError :: Sing (str :: Symbol) -> a
• module Data.Singletons.Prelude.Eq
• module Data.Singletons.Prelude.Ord
• type family Id a :: a
• sId :: forall t. Sing t -> Sing (Apply IdSym0 t)
• type family Const a a :: a
• sConst :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ConstSym0 t) t)
• type family (a :. a) a :: c
• (%:.) :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (:.$) t) t) t)
• type family f $ x :: b
• (%$) :: forall f x. Sing f -> Sing x -> Sing ((($$) @@ f) @@ x)
• type family f $! x :: b
• (%$!) :: forall f x. Sing f -> Sing x -> Sing ((($!$) @@ f) @@ x)
• type family Flip a a a :: c
• sFlip :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FlipSym0 t) t) t)
• type family AsTypeOf a a :: a
• sAsTypeOf :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AsTypeOfSym0 t) t)
• type family Seq a a :: b
• sSeq :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply SeqSym0 t) t)
• type family Map a a :: [] b
• sMap :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t)
• type family a :++ a :: [] a
• (%:++) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:++$) t) t)
• type family Head a :: a
• sHead :: forall t. Sing t -> Sing (Apply HeadSym0 t)
• type family Last a :: a
• sLast :: forall t. Sing t -> Sing (Apply LastSym0 t)
• type family Tail a :: [] a
• sTail :: forall t. Sing t -> Sing (Apply TailSym0 t)
• type family Init a :: [] a
• sInit :: forall t. Sing t -> Sing (Apply InitSym0 t)
• type family Null a :: Bool
• sNull :: forall t. Sing t -> Sing (Apply NullSym0 t)
• type family Reverse a :: [] a
• sReverse :: forall t. Sing t -> Sing (Apply ReverseSym0 t)
• type family Foldl a a a :: b
• sFoldl :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t)
• type family Foldl1 a a :: a
• sFoldl1 :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t)
• type family Foldr a a a :: b
• sFoldr :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t)
• type family Foldr1 a a :: a
• sFoldr1 :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t)
• type family And a :: Bool
• sAnd :: forall t. Sing t -> Sing (Apply AndSym0 t)
• type family Or a :: Bool
• sOr :: forall t. Sing t -> Sing (Apply OrSym0 t)
• type family Any_ a a :: Bool
• sAny_ :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply Any_Sym0 t) t)
• type family All a a :: Bool
• sAll :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply AllSym0 t) t)
• type family Concat a :: [] a
• sConcat :: forall t. Sing t -> Sing (Apply ConcatSym0 t)
• type family ConcatMap a a :: [] b
• sConcatMap :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ConcatMapSym0 t) t)
• type family Scanl a a a :: [] b
• sScanl :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanlSym0 t) t) t)
• type family Scanl1 a a :: [] a
• sScanl1 :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply Scanl1Sym0 t) t)
• type family Scanr a a a :: [] b
• sScanr :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ScanrSym0 t) t) t)
• type family Scanr1 a a :: [] a
• sScanr1 :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply Scanr1Sym0 t) t)
• type family Elem a a :: Bool
• sElem :: forall t t. SEq (KProxy :: KProxy a) => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t)
• type family NotElem a a :: Bool
• sNotElem :: forall t t. SEq (KProxy :: KProxy a) => Sing t -> Sing t -> Sing (Apply (Apply NotElemSym0 t) t)
• type family Zip a a :: [] ((,) a b)
• sZip :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply ZipSym0 t) t)
• type family Zip3 a a a :: [] ((,,) a b c)
• sZip3 :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Zip3Sym0 t) t) t)
• type family ZipWith a a a :: [] c
• sZipWith :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ZipWithSym0 t) t) t)
• type family ZipWith3 a a a a :: [] d
• sZipWith3 :: forall t t t t. Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply ZipWith3Sym0 t) t) t) t)
• type family Unzip a :: (,) ([] a) ([] b)
• sUnzip :: forall t. Sing t -> Sing (Apply UnzipSym0 t)
• type family Unzip3 a :: (,,) ([] a) ([] b) ([] c)
• sUnzip3 :: forall t. Sing t -> Sing (Apply Unzip3Sym0 t)
• type family Maybe_ a a a :: b
• sMaybe_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Maybe_Sym0 t) t) t)
• type family Either_ a a a :: c
• sEither_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Either_Sym0 t) t) t)
• type family Fst a :: a
• sFst :: forall t. Sing t -> Sing (Apply FstSym0 t)
• type family Snd a :: b
• sSnd :: forall t. Sing t -> Sing (Apply SndSym0 t)
• type family Curry a a a :: c
• sCurry :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t)
• type family Uncurry a a :: c
• sUncurry :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t)
• data Symbol :: *
• either_ :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
• maybe_ :: forall b a. b -> (a -> b) -> Maybe a -> b
• bool_ :: forall a. a -> a -> Bool -> a
• any_ :: forall a. (a -> Bool) -> [a] -> Bool
• type FalseSym0 = False
• type TrueSym0 = True
• data NotSym0 l
• type NotSym1 t = Not t
• data (:&&$) l
• data l :&&$$ l
• type (:&&$$$) t t = (:&&) t t
• data (:||$) l
• data l :||$$ l
• type (:||$$$) t t = (:||) t t
• type OtherwiseSym0 = Otherwise
• type NothingSym0 = Nothing
• data JustSym0 l
• type JustSym1 t = Just t
• data Maybe_Sym0 l
• data Maybe_Sym1 l l
• data Maybe_Sym2 l l l
• type Maybe_Sym3 t t t = Maybe_ t t t
• data LeftSym0 l
• type LeftSym1 t = Left t
• data RightSym0 l
• type RightSym1 t = Right t
• data Either_Sym0 l
• data Either_Sym1 l l
• data Either_Sym2 l l l
• type Either_Sym3 t t t = Either_ t t t
• type Tuple0Sym0 = ()
• data Tuple2Sym0 l
• data Tuple2Sym1 l l
• type Tuple2Sym2 t t = (,) t t
• data Tuple3Sym0 l
• data Tuple3Sym1 l l
• data Tuple3Sym2 l l l
• type Tuple3Sym3 t t t = (,,) t t t
• data Tuple4Sym0 l
• data Tuple4Sym1 l l
• data Tuple4Sym2 l l l
• data Tuple4Sym3 l l l l
• type Tuple4Sym4 t t t t = (,,,) t t t t
• data Tuple5Sym0 l
• data Tuple5Sym1 l l
• data Tuple5Sym2 l l l
• data Tuple5Sym3 l l l l
• data Tuple5Sym4 l l l l l
• type Tuple5Sym5 t t t t t = (,,,,) t t t t t
• data Tuple6Sym0 l
• data Tuple6Sym1 l l
• data Tuple6Sym2 l l l
• data Tuple6Sym3 l l l l
• data Tuple6Sym4 l l l l l
• data Tuple6Sym5 l l l l l l
• type Tuple6Sym6 t t t t t t = (,,,,,) t t t t t t
• data Tuple7Sym0 l
• data Tuple7Sym1 l l
• data Tuple7Sym2 l l l
• data Tuple7Sym3 l l l l
• data Tuple7Sym4 l l l l l
• data Tuple7Sym5 l l l l l l
• data Tuple7Sym6 l l l l l l l
• type Tuple7Sym7 t t t t t t t = (,,,,,,) t t t t t t t
• data FstSym0 l
• type FstSym1 t = Fst t
• data SndSym0 l
• type SndSym1 t = Snd t
• data CurrySym0 l
• data CurrySym1 l l
• data CurrySym2 l l l
• type CurrySym3 t t t = Curry t t t
• data UncurrySym0 l
• data UncurrySym1 l l
• type UncurrySym2 t t = Uncurry t t
• data IdSym0 l
• type IdSym1 t = Id t
• data ConstSym0 l
• data ConstSym1 l l
• type ConstSym2 t t = Const t t
• data (:.$) l
• data l :.$$ l
• data (l :.$$$ l) l
• data ($$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *
• data ($$$) :: (TyFun a b -> *) -> TyFun a b -> *
• type ($$$$) a b = ($) a b
• data ($!$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> *
• data ($!$$) :: (TyFun a b -> *) -> TyFun a b -> *
• type ($!$$$) a b = ($!) a b
• data FlipSym0 l
• data FlipSym1 l l
• data FlipSym2 l l l
• data AsTypeOfSym0 l
• data AsTypeOfSym1 l l
• type AsTypeOfSym2 t t = AsTypeOf t t
• data SeqSym0 l
• data SeqSym1 l l
• type SeqSym2 t t = Seq t t
• data (:$) l
• data l :$$ l
• type (:$$$) t t = (:) t t
• type NilSym0 = []
• type ConsSym0 = (:$)
• type ConsSym1 = (:$$)
• type ConsSym2 a b = (:$$$) a b
• data MapSym0 l
• data MapSym1 l l
• type MapSym2 t t = Map t t
• data ReverseSym0 l
• type ReverseSym1 t = Reverse t
• data l :++$$ l
• data (:++$) l
• data HeadSym0 l
• type HeadSym1 t = Head t
• data LastSym0 l
• type LastSym1 t = Last t
• data TailSym0 l
• type TailSym1 t = Tail t
• data InitSym0 l
• type InitSym1 t = Init t
• data NullSym0 l
• type NullSym1 t = Null t
• data FoldlSym0 l
• data FoldlSym1 l l
• data FoldlSym2 l l l
• type FoldlSym3 t t t = Foldl t t t
• data Foldl1Sym0 l
• data Foldl1Sym1 l l
• type Foldl1Sym2 t t = Foldl1 t t
• data FoldrSym0 l
• data FoldrSym1 l l
• data FoldrSym2 l l l
• type FoldrSym3 t t t = Foldr t t t
• data Foldr1Sym0 l
• data Foldr1Sym1 l l
• type Foldr1Sym2 t t = Foldr1 t t
• data ConcatSym0 l
• type ConcatSym1 t = Concat t
• data ConcatMapSym0 l
• data ConcatMapSym1 l l
• type ConcatMapSym2 t t = ConcatMap t t
• data AndSym0 l
• type AndSym1 t = And t
• data OrSym0 l
• type OrSym1 t = Or t
• data Any_Sym0 l
• data Any_Sym1 l l
• type Any_Sym2 t t = Any_ t t
• data AllSym0 l
• data AllSym1 l l
• type AllSym2 t t = All t t
• data ScanlSym0 l
• data ScanlSym1 l l
• data ScanlSym2 l l l
• type ScanlSym3 t t t = Scanl t t t
• data Scanl1Sym0 l
• data Scanl1Sym1 l l
• type Scanl1Sym2 t t = Scanl1 t t
• data ScanrSym0 l
• data ScanrSym1 l l
• data ScanrSym2 l l l
• type ScanrSym3 t t t = Scanr t t t
• data Scanr1Sym0 l
• data Scanr1Sym1 l l
• type Scanr1Sym2 t t = Scanr1 t t
• data ElemSym0 l
• data ElemSym1 l l
• type ElemSym2 t t = Elem t t
• data NotElemSym0 l
• data NotElemSym1 l l
• type NotElemSym2 t t = NotElem t t
• data ZipSym0 l
• data ZipSym1 l l
• type ZipSym2 t t = Zip t t
• data Zip3Sym0 l
• data Zip3Sym1 l l
• data Zip3Sym2 l l l
• type Zip3Sym3 t t t = Zip3 t t t
• data ZipWithSym0 l
• data ZipWithSym1 l l
• data ZipWithSym2 l l l
• type ZipWithSym3 t t t = ZipWith t t t
• data ZipWith3Sym0 l
• data ZipWith3Sym1 l l
• data ZipWith3Sym2 l l l
• data ZipWith3Sym3 l l l l
• data UnzipSym0 l
• type UnzipSym1 t = Unzip t

Basic singleton definitions

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

Functions working with Bool

Error reporting

Singleton equality

Singleton comparisons

Miscellaneous functions

List operations

Reducing lists (folds)

Special folds

Scans

Searching lists

Zipping and unzipping lists

Other datatypes

Other functions

Defunctionalization symbols