generics-sop-0.1.1.1: Generic Programming using True Sums of Products

Safe HaskellSafe-Inferred
LanguageHaskell2010

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

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

sing :: Sing a Source

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

Eq (Shape k xs) 
Ord (Shape k xs) 
Show (Shape k xs) 

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.