Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

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

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`

.

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 |

data Sing [k] where | Singleton for type-level lists. |

## 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)

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

The length of a type-level list.