Data.Singletons.List

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

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 z

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

type family Head a :: a

type family Tail a :: [a]

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

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

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

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

type family Reverse a :: [a]

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