Safe Haskell	Safe-Inferred
Language	Haskell2010

Generics.SOP.Sing

Contents

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

Singletons

data family Sing a Source

Explicit singleton.

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

The family Sing should have at most one instance per kind, and there should be a matching instance for SingI.

Instances

Eq (Sing [k] xs)
Eq (Sing * x)
Ord (Sing [k] xs)
Ord (Sing * x)
Show (Sing [k] xs)
Show (Sing * x)
data Sing * = SStar	Singleton for types of kind ``. For types of kind ``, we explicitly don't want to reveal more type analysis. Even functions that have a `Sing` constraint should still be parametric in everything that is of kind `*`.
data Sing [k] where SNil :: Sing [k] ([] k) SCons :: (SingI k x, SingI [k] xs) => Sing [k] ((:) k x xs)	Singleton for type-level lists.

class SingI a where Source

Implicit singleton.

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

The class SingI should have instances that match the family instances for Sing.

Methods

Get hold of the explicit singleton (that one can then pattern match on).

Instances

SingI * x
SingI [k] ([] k)
(SingI k x, SingI [k] xs) => SingI [k] ((:) k x xs)

Shape of type-level lists

data Shape :: [k] -> * where Source

Occassionally 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 :: (SingI x, SingI xs) => Shape xs -> Shape (x : xs)

Instances

shape :: forall xs. SingI xs => Shape xs Source

The shape of a type-level list.

lengthSing :: forall xs. SingI xs => Proxy xs -> Int Source

The length of a type-level list.