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