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

Singletons

data family Sing a

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

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

sing :: Sing a

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

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

Eq (Shape k xs)

Ord (Shape k xs)

Show (Shape k xs)

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

The shape of a type-level list.

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

The length of a type-level list.