Modulesop-core-0.5.0.2Haskell2010

Data.SOP.Sing

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.

Contents

Singletons
Shape of type-level lists

Synopsis

data SList
type SListI
value sList
value para_SList
value case_SList
data Shape
value shape
value lengthSList

Packagesop-core-0.5.0.2
Exports8
LanguageHaskell2010
LicenceBSD-3-Clause
SourceSing.hs

Singletons

datadata SList (a :: [k]) 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.

Constructors

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

Instances3Eq, Ord, Show

Eq (SList xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing
Ord (SList xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing
Show (SList xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing

typetype 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.

valuesList :: SListI xs => SList xs

Source#

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

valuepara_SList

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

Source#

Paramorphism for a type-level list.

valuecase_SList

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

Source#

Case distinction on a type-level list.

Shape of type-level lists

datadata Shape (a :: [k]) 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)

Instances3Eq, Ord, Show

Eq (Shape xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing
Ord (Shape xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing
Show (Shape xs)Defined in sop-core-0.5.0.2 · Data.SOP.Sing

valueshape :: SListI xs => Shape xs

Source#

The shape of a type-level list.

valuelengthSList :: SListI xs => proxy xs -> Int

Source#

The length of a type-level list.