Safe Haskell	None
Language	Haskell2010

Data.SOP.Sing

Contents

Singletons
- Shape of type-level lists

Description

Singleton types corresponding to type-level data structures.

The implementation is similar, but subtly different to that of the singletons package. See the "True Sums of Products" paper for details.

Synopsis

data SList :: [k] -> Type where
- SNil :: SList '[]
- SCons :: SListI xs => SList (x ': xs)
type SListI = All Top
sList :: SListI xs => SList xs
para_SList :: SListI xs => r '[] -> ( forall y ys. SListI ys => r ys -> r (y ': ys)) -> r xs
case_SList :: SListI xs => r '[] -> ( forall y ys. SListI ys => r (y ': ys)) -> r xs
data Shape :: [k] -> Type where
- ShapeNil :: Shape '[]
- ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)
shape :: forall k (xs :: [k]). SListI xs => Shape xs
lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int

Singletons

data SList :: [k] -> Type where Source #

Explicit singleton list.

A singleton list can be used to reveal the structure of a type-level list argument that the function is quantified over. For every type-level list xs , there is one non-bottom value of type SList xs .

Note that these singleton lists are polymorphic in the list elements; we do not require a singleton representation for them.

Since: 0.2

Constructors

SNil :: SList '[]
SCons :: SListI xs => SList (x ': xs)

Instances

Instances details

Eq ( SList xs) Source #
Instance details Defined in Data.SOP.Sing Methods (==) :: SList xs -> SList xs -> Bool Source # (/=) :: SList xs -> SList xs -> Bool Source #
Ord ( SList xs) Source #
Instance details Defined in Data.SOP.Sing Methods compare :: SList xs -> SList xs -> Ordering Source # (<) :: SList xs -> SList xs -> Bool Source # (<=) :: SList xs -> SList xs -> Bool Source # (>) :: SList xs -> SList xs -> Bool Source # (>=) :: SList xs -> SList xs -> Bool Source # max :: SList xs -> SList xs -> SList xs Source # min :: SList xs -> SList xs -> SList xs Source #
Show ( SList xs) Source #
Instance details Defined in Data.SOP.Sing Methods showsPrec :: Int -> SList xs -> ShowS Source # show :: SList xs -> String Source # showList :: [ SList xs] -> ShowS Source #

type SListI = All Top Source #

Implicit singleton list.

A singleton list can be used to reveal the structure of a type-level list argument that the function is quantified over.

Since 0.4.0.0, this is now defined in terms of All . A singleton list provides a witness for a type-level list where the elements need not satisfy any additional constraints.

Since: 0.4.0.0

sList :: SListI xs => SList xs Source #

Get hold of an explicit singleton (that one can then pattern match on) for a type-level list

para_SList :: SListI xs => r '[] -> ( forall y ys. SListI ys => r ys -> r (y ': ys)) -> r xs Source #

Paramorphism for a type-level list.

Since: 0.4.0.0

case_SList :: SListI xs => r '[] -> ( forall y ys. SListI ys => r (y ': ys)) -> r xs Source #

Case distinction on a type-level list.

Since: 0.4.0.0

Shape of type-level lists

data Shape :: [k] -> Type where Source #

Occasionally it is useful to have an explicit, term-level, representation of type-level lists (esp because of https://ghc.haskell.org/trac/ghc/ticket/9108 )

Constructors

ShapeNil :: Shape '[]
ShapeCons :: SListI xs => Shape xs -> Shape (x ': xs)

Instances

Instances details

Eq ( Shape xs) Source #
Instance details Defined in Data.SOP.Sing Methods (==) :: Shape xs -> Shape xs -> Bool Source # (/=) :: Shape xs -> Shape xs -> Bool Source #
Ord ( Shape xs) Source #
Instance details Defined in Data.SOP.Sing Methods compare :: Shape xs -> Shape xs -> Ordering Source # (<) :: Shape xs -> Shape xs -> Bool Source # (<=) :: Shape xs -> Shape xs -> Bool Source # (>) :: Shape xs -> Shape xs -> Bool Source # (>=) :: Shape xs -> Shape xs -> Bool Source # max :: Shape xs -> Shape xs -> Shape xs Source # min :: Shape xs -> Shape xs -> Shape xs Source #
Show ( Shape xs) Source #
Instance details Defined in Data.SOP.Sing Methods showsPrec :: Int -> Shape xs -> ShowS Source # show :: Shape xs -> String Source # showList :: [ Shape xs] -> ShowS Source #

shape :: forall k (xs :: [k]). SListI xs => Shape xs Source #

The shape of a type-level list.

lengthSList :: forall k (xs :: [k]) proxy. SListI xs => proxy xs -> Int Source #

The length of a type-level list.

Since: 0.2