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

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

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