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

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.

## Synopsis

- data SList :: [k] -> * where
- class SListI (xs :: [k]) where
- type Sing = SList
- class SListI xs => SingI (xs :: [k]) where
- data Shape :: [k] -> * where
- shape :: forall (xs :: [k]). SListI xs => Shape xs
- lengthSList :: forall (xs :: [k]) proxy. SListI xs => proxy xs -> Int
- lengthSing :: SListI xs => proxy xs -> Int

# Singletons

data SList :: [k] -> * where Source #

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*

Deprecated: Use `SList`

instead.

Explicit singleton type.

Just provided for limited backward compatibility.

class SListI xs => SingI (xs :: [k]) where Source #

Deprecated: Use `SListI`

instead.

General class for implicit singletons.

Just provided for limited backward compatibility.

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

lengthSList :: forall (xs :: [k]) proxy. SListI xs => proxy xs -> Int Source #

The length of a type-level list.

*Since: 0.2*

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

Deprecated: Use `lengthSList`

instead.

Old name for `lengthSList`

.