Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
This module contains basic functionality for deriving your own singletons
via Template Haskell. Note that this module does not define any singled
definitions on its own. For a version of this module that comes pre-equipped
with several singled definitions based on the Prelude, see
Data.Singletons.Base.TH
from the singletons-base
library.
Synopsis
- singletons :: OptionsMonad q => q [Dec] -> q [Dec]
- singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec]
- genSingletons :: OptionsMonad q => [Name] -> q [Dec]
- promote :: OptionsMonad q => q [Dec] -> q [Dec]
- promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]
- genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec]
- genPromotions :: OptionsMonad q => [Name] -> q [Dec]
- promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteEqInstance :: OptionsMonad q => Name -> q [Dec]
- singEqInstances :: OptionsMonad q => [Name] -> q [Dec]
- singEqInstance :: OptionsMonad q => Name -> q [Dec]
- singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]
- singDecideInstance :: OptionsMonad q => Name -> q [Dec]
- promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]
- singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]
- singOrdInstance :: OptionsMonad q => Name -> q [Dec]
- promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]
- singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]
- singBoundedInstance :: OptionsMonad q => Name -> q [Dec]
- promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]
- singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]
- singEnumInstance :: OptionsMonad q => Name -> q [Dec]
- promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]
- promoteShowInstance :: OptionsMonad q => Name -> q [Dec]
- singShowInstances :: OptionsMonad q => [Name] -> q [Dec]
- singShowInstance :: OptionsMonad q => Name -> q [Dec]
- showSingInstances :: OptionsMonad q => [Name] -> q [Dec]
- showSingInstance :: OptionsMonad q => Name -> q [Dec]
- singITyConInstances :: DsMonad q => [Int] -> q [Dec]
- singITyConInstance :: DsMonad q => Int -> q Dec
- cases :: DsMonad q => Name -> q Exp -> q Exp -> q Exp
- sCases :: OptionsMonad q => Name -> q Exp -> q Exp -> q Exp
- module Data.Singletons
- class SDecide k where
- data (a :: k) :~: (b :: k) where
- data Void
- type Refuted a = a -> Void
- data Decision a
- class SuppressUnusedWarnings (t :: k) where
- suppressUnusedWarnings :: ()
Primary Template Haskell generation functions
singletons :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Make promoted and singled versions of all declarations given, retaining
the original declarations. See the
README
for further explanation.
singletonsOnly :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Make promoted and singled versions of all declarations given, discarding the original declarations. Note that a singleton based on a datatype needs the original datatype, so this will fail if it sees any datatype declarations. Classes, instances, and functions are all fine.
genSingletons :: OptionsMonad q => [Name] -> q [Dec] Source #
Generate singled definitions for each of the provided type-level
declaration Name
s. For example, the singletons-th package itself uses
$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
to generate singletons for Prelude types.
promote :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Promote every declaration given to the type level, retaining the originals.
See the
README
for further explanation.
promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec] Source #
Promote each declaration, discarding the originals. Note that a promoted datatype uses the same definition as an original datatype, so this will not work with datatypes. Classes, instances, and functions are all fine.
genDefunSymbols :: OptionsMonad q => [Name] -> q [Dec] Source #
Generate defunctionalization symbols for each of the provided type-level
declaration Name
s. See the "Promotion and partial application" section of
the singletons
README
for further explanation.
genPromotions :: OptionsMonad q => [Name] -> q [Dec] Source #
Generate promoted definitions for each of the provided type-level
declaration Name
s. This is generally only useful with classes.
Functions to generate equality instances
promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PEq
from the given types
promoteEqInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PEq
from the given type
singEqInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SEq
for the given types
singEqInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SEq
for the given type
singDecideInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SDecide
, TestEquality
, and TestCoercion
for each
type in the list.
singDecideInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instances of SDecide
, TestEquality
, and TestCoercion
for the
given type.
Functions to generate Ord
instances
promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for POrd
from the given types
promoteOrdInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for POrd
from the given type
singOrdInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SOrd
for the given types
singOrdInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SOrd
for the given type
Functions to generate Bounded
instances
promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PBounded
from the given types
promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PBounded
from the given type
singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SBounded
for the given types
singBoundedInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SBounded
for the given type
Functions to generate Enum
instances
promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PEnum
from the given types
promoteEnumInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PEnum
from the given type
singEnumInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SEnum
for the given types
singEnumInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SEnum
for the given type
Functions to generate Show
instances
promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Produce instances for PShow
from the given types
promoteShowInstance :: OptionsMonad q => Name -> q [Dec] Source #
Produce an instance for PShow
from the given type
singShowInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of SShow
for the given types
(Not to be confused with showSingInstances
.)
singShowInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of SShow
for the given type
(Not to be confused with showShowInstance
.)
showSingInstances :: OptionsMonad q => [Name] -> q [Dec] Source #
Create instances of Show
for the given singleton types
(Not to be confused with singShowInstances
.)
showSingInstance :: OptionsMonad q => Name -> q [Dec] Source #
Create instance of Show
for the given singleton type
(Not to be confused with singShowInstance
.)
Utility functions
singITyConInstances :: DsMonad q => [Int] -> q [Dec] Source #
Create an instance for
, where SingI
TyCon{N}N
is the positive
number provided as an argument.
Note that the generated code requires the use of the QuantifiedConstraints
language extension.
singITyConInstance :: DsMonad q => Int -> q Dec Source #
Create an instance for
, where SingI
TyCon{N}N
is the positive
number provided as an argument.
Note that the generated code requires the use of the QuantifiedConstraints
language extension.
:: DsMonad q | |
=> Name | The head of the type of the scrutinee. (e.g., |
-> q Exp | The scrutinee, in a Template Haskell quote |
-> q Exp | The body, in a Template Haskell quote |
-> q Exp |
:: OptionsMonad q | |
=> Name | The head of the type the scrutinee's type is based on.
(Like |
-> q Exp | The scrutinee, in a Template Haskell quote |
-> q Exp | The body, in a Template Haskell quote |
-> q Exp |
The function sCases
generates a case expression where each right-hand side
is identical. This may be useful if the type-checker requires knowledge of which
constructor is used to satisfy equality or type-class constraints, but where
each constructor is treated the same.
For sCases
, unlike cases
, the scrutinee is a singleton. But make sure to
pass in the name of the original datatype, preferring ''Maybe
over
''SMaybe
. In other words, sCases ''Maybe
is equivalent to
.cases
''SMaybe
Basic singleton definitions
module Data.Singletons
Auxiliary definitions
Members of the SDecide
"kind" class support decidable equality. Instances
of this class are generated alongside singleton definitions for datatypes that
derive an Eq
instance.
data (a :: k) :~: (b :: k) where #
Instances
Category ((:~:) :: k -> k -> Type) | |
TestCoercion ((:~:) a :: k -> Type) | |
Defined in Data.Type.Coercion testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) | |
NFData2 ((:~:) :: Type -> Type -> Type) | |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | |
Defined in Control.DeepSeq | |
(a ~ b, Data a) => Data (a :~: b) | |
Defined in Data.Data gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) toConstr :: (a :~: b) -> Constr dataTypeOf :: (a :~: b) -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) | |
a ~ b => Bounded (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (a :~: b) | |
NFData (a :~: b) | |
Defined in Control.DeepSeq | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality |
Instances
Data Void | |
Defined in Data.Data gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void dataTypeOf :: Void -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void) gmapT :: (forall b. Data b => b -> b) -> Void -> Void gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r gmapQ :: (forall d. Data d => d -> u) -> Void -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void | |
Semigroup Void | |
Generic Void | |
Read Void | |
Show Void | |
NFData Void | |
Defined in Control.DeepSeq | |
Eq Void | |
Ord Void | |
Lift Void | |
type Rep Void | |
Defined in GHC.Generics type Rep Void = D1 ('MetaData "Void" "GHC.Base" "base" 'False) (V1 :: Type -> Type) |
A Decision
about a type a
is either a proof of existence or a proof that a
cannot exist.
class SuppressUnusedWarnings (t :: k) where Source #
This class (which users should never see) is to be instantiated in order to use an otherwise-unused data constructor, such as the "kind-inference" data constructor for defunctionalization symbols.
suppressUnusedWarnings :: () Source #