Data.Singletons.TH

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.

Primary Template Haskell generation functions

singletons :: OptionsMonad q => q [Dec] -> q [Dec]

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]

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]

Generate singled definitions for each of the provided type-level declaration Names. 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]

Promote every declaration given to the type level, retaining the originals. See the README for further explanation.

promoteOnly :: OptionsMonad q => q [Dec] -> q [Dec]

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]

Generate defunctionalization symbols for each of the provided type-level declaration Names. See the "Promotion and partial application" section of the singletons README for further explanation.

genPromotions :: OptionsMonad q => [Name] -> q [Dec]

Generate promoted definitions for each of the provided type-level declaration Names. This is generally only useful with classes.

Functions to generate equality instances

promoteEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEq from the given types

promoteEqInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEq from the given type

singEqInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEq for the given types

singEqInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEq for the given type

singDecideInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SDecide, TestEquality, and TestCoercion for each type in the list.

singDecideInstance :: OptionsMonad q => Name -> q [Dec]

Create instances of SDecide, TestEquality, and TestCoercion for the given type.

Functions to generate Ord instances

promoteOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for POrd from the given types

promoteOrdInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for POrd from the given type

singOrdInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SOrd for the given types

singOrdInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SOrd for the given type

Functions to generate Bounded instances

promoteBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PBounded from the given types

promoteBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PBounded from the given type

singBoundedInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SBounded for the given types

singBoundedInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SBounded for the given type

Functions to generate Enum instances

promoteEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PEnum from the given types

promoteEnumInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PEnum from the given type

singEnumInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SEnum for the given types

singEnumInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SEnum for the given type

Functions to generate Show instances

promoteShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Produce instances for PShow from the given types

promoteShowInstance :: OptionsMonad q => Name -> q [Dec]

Produce an instance for PShow from the given type

singShowInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of SShow for the given types

(Not to be confused with showSingInstances.)

singShowInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of SShow for the given type

(Not to be confused with showShowInstance.)

showSingInstances :: OptionsMonad q => [Name] -> q [Dec]

Create instances of Show for the given singleton types

(Not to be confused with singShowInstances.)

showSingInstance :: OptionsMonad q => Name -> q [Dec]

Create instance of Show for the given singleton type

(Not to be confused with singShowInstance.)

Utility functions

singITyConInstances :: DsMonad q => [Int] -> q [Dec]

Create an instance for SingI TyCon{N}, where 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

Create an instance for SingI TyCon{N}, where N is the positive number provided as an argument.

Note that the generated code requires the use of the QuantifiedConstraints language extension.

cases

Arguments

:: DsMonad q

=> Name

The head of the type of the scrutinee. (e.g., ''SBool)

-> q Exp

The scrutinee, in a Template Haskell quote

-> q Exp

The body, in a Template Haskell quote

-> q Exp

sCases

Arguments

:: OptionsMonad q

=> Name

The head of the type the scrutinee's type is based on. (Like ''Maybe or ''Bool.)

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

class SDecide k where

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.

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4

Compute a proof or disproof of equality, given two singletons.

data (a :: k) :~: (b :: k) where

Constructors

Refl :: forall {k} (a :: k). a :~: a

Instances

Category ((:~:) :: k -> k -> Type)

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~: a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c

TestCoercion ((:~:) a :: k -> Type)

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> Type)

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: Type -> Type -> Type)

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

(a ~ b, Data a) => Data (a :~: b)

Defined in Data.Data

Methods

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

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

a ~ b => Read (a :~: b)

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b)

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

Eq (a :~: b)

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b)

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

data Void

Instances

Data Void

Defined in Data.Data

Methods

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

toConstr :: Void -> Constr

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

Defined in GHC.Base

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Generic Void

Defined in GHC.Generics

Associated Types

type Rep Void :: Type -> Type

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Read Void

Defined in GHC.Read

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Defined in GHC.Show

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

NFData Void

Defined in Control.DeepSeq

Methods

rnf :: Void -> ()

Eq Void

Defined in GHC.Base

Methods

(==) :: Void -> Void -> Bool

(/=) :: Void -> Void -> Bool

Ord Void

Defined in GHC.Base

Methods

compare :: Void -> Void -> Ordering

(<) :: Void -> Void -> Bool

(<=) :: Void -> Void -> Bool

(>) :: Void -> Void -> Bool

(>=) :: Void -> Void -> Bool

max :: Void -> Void -> Void

min :: Void -> Void -> Void

Lift Void

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Quote m => Void -> m Exp

liftTyped :: forall (m :: Type -> Type). Quote m => Void -> Code m Void

type Rep Void

Defined in GHC.Generics

type Rep Void = D1 ('MetaData "Void" "GHC.Base" "base" 'False) (V1 :: Type -> Type)

type Refuted a = a -> Void

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists

class SuppressUnusedWarnings (t :: k) where

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.

Methods

suppressUnusedWarnings :: ()