singletons-0.9.3: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
License(C) 2013 Richard Eisenberg
MaintainerRichard Eisenberg (
Safe HaskellNone




Defines functions and datatypes relating to the singleton for '[]', including a singletons version of a few of the definitions in Data.List.

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


The singleton for lists

data family Sing a Source

The singleton kind-indexed data family.

Though Haddock doesn't show it, the Sing instance above declares constructors

 SNil  :: Sing '[]
 SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)

type SList z = Sing zSource

SList is a kind-restricted synonym for Sing: type SList (a :: [k]) = Sing a

type family Head a :: aSource

type family Tail a :: [a]Source

sHead :: forall t. Sing t -> Sing (Head t)Source

sTail :: forall t. Sing t -> Sing (Tail t)Source

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

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

type family Reverse a :: [a]Source

sReverse :: forall t. Sing t -> Sing (Reverse t)Source