Copyright | (C) 2013 Richard Eisenberg |
---|---|

License | BSD-style (see LICENSE) |

Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

This file implements `singletonStar`

, which generates a datatype `Rep`

and associated
singleton from a list of types. The promoted version of `Rep`

is kind `*`

and the
Haskell types themselves. This is still very experimental, so expect unusual
results!

- singletonStar :: DsMonad q => [Name] -> q [Dec]
- module Data.Singletons.Prelude.Eq
- module Data.Singletons.Prelude.Bool

# Documentation

Produce a representation and singleton for the collection of types given.

A datatype `Rep`

is created, with one constructor per type in the declared
universe. When this type is promoted by the singletons library, the
constructors become full types in `*`

, not just promoted data constructors.

For example,

$(singletonStar [''Nat, ''Bool, ''Maybe])

generates the following:

data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)

and its singleton. However, because `Rep`

is promoted to `*`

, the singleton
is perhaps slightly unexpected:

data instance Sing (a :: *) where SNat :: Sing Nat SBool :: Sing Bool SMaybe :: SingRep a => Sing a -> Sing (Maybe a)

The unexpected part is that `Nat`

, `Bool`

, and `Maybe`

above are the real `Nat`

,
`Bool`

, and `Maybe`

, not just promoted data constructors.

Please note that this function is *very* experimental. Use at your own risk.

module Data.Singletons.Prelude.Eq

module Data.Singletons.Prelude.Bool