Data.Singletons.CustomStar

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!

Documentation

singletonStar

Arguments

:: DsMonad q

=> [Name]

A list of Template Haskell Names 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