singletons-2.1: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

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