singletons-2.5.1: A framework for generating singleton types

Copyright | (C) 2013 Richard Eisenberg
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.CustomStar

Description

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!

Synopsis

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

# Documentation

singletonStar Source #

Arguments

:: DsMonad q |
=> [Name] | A list of Template Haskell `Name`s for types
-> q [Dec] |

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, Ord, Read, Show)

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 :: 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

module Data.Singletons.TH