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 SList :: [k] -> * where

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

Eq (SList k xs)

Methods

(==) :: SList k xs -> SList k xs -> Bool

(/=) :: SList k xs -> SList k xs -> Bool

Ord (SList k xs)

Methods

compare :: SList k xs -> SList k xs -> Ordering

(<) :: SList k xs -> SList k xs -> Bool

(<=) :: SList k xs -> SList k xs -> Bool

(>) :: SList k xs -> SList k xs -> Bool

(>=) :: SList k xs -> SList k xs -> Bool

max :: SList k xs -> SList k xs -> SList k xs

min :: SList k xs -> SList k xs -> SList k xs

Show (SList k xs)

Methods

showsPrec :: Int -> SList k xs -> ShowS

show :: SList k xs -> String

showList :: [SList k xs] -> ShowS

class SListI xs where

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.

The class SListI should have instances that match the constructors of SList.

Since: 0.2

Minimal complete definition

sList

Methods

sList :: SList xs

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

Instances

SListI k ([] k)

Methods

sList :: SList [k] xs

SListI k xs => SListI k ((:) k x xs)

Methods

sList :: SList ((k ': x) xs) xs

type Sing = SList

Deprecated: Use SList instead.

Explicit singleton type.

Just provided for limited backward compatibility.

class SListI xs => SingI xs where

Deprecated: Use SListI instead.

General class for implicit singletons.

Just provided for limited backward compatibility.

Minimal complete definition

sing

Methods

sing :: Sing xs

Deprecated: Use sList instead.

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 :: SListI xs => Shape xs -> Shape (x ': xs)

Instances

Eq (Shape k xs)

Methods

(==) :: Shape k xs -> Shape k xs -> Bool

(/=) :: Shape k xs -> Shape k xs -> Bool

Ord (Shape k xs)

Methods

compare :: Shape k xs -> Shape k xs -> Ordering

(<) :: Shape k xs -> Shape k xs -> Bool

(<=) :: Shape k xs -> Shape k xs -> Bool

(>) :: Shape k xs -> Shape k xs -> Bool

(>=) :: Shape k xs -> Shape k xs -> Bool

max :: Shape k xs -> Shape k xs -> Shape k xs

min :: Shape k xs -> Shape k xs -> Shape k xs

Show (Shape k xs)

Methods

showsPrec :: Int -> Shape k xs -> ShowS

show :: Shape k xs -> String

showList :: [Shape k xs] -> ShowS

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

The shape of a type-level list.

lengthSList :: forall xs proxy. SListI xs => proxy xs -> Int

The length of a type-level list.

Since: 0.2

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

Deprecated: Use lengthSList instead.

Old name for lengthSList.