Copyright | (C) 2013 Richard Eisenberg |
---|---|
License | (C) 2013 Richard Eisenberg |
Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
This module exports the basic definitions to use singletons. For routine
use, consider importing Prelude
, which exports constructors
for singletons based on types in the Prelude
.
You may also want to read http://www.cis.upenn.edu/~eir/packages/singletons/README.html and the original paper presenting this library, available at http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf.
- data family Sing a
- class SingI a where
- class kparam ~ KProxy => SingKind kparam where
- type KindOf a = (KProxy :: KProxy k)
- type Demote a = DemoteRep (KProxy :: KProxy k)
- data SingInstance a where
- SingInstance :: SingI a => SingInstance a
- data SomeSing kproxy where
- singInstance :: forall a. Sing a -> SingInstance a
- withSingI :: Sing n -> (SingI n => r) -> r
- withSomeSing :: SingKind (KProxy :: KProxy k) => DemoteRep (KProxy :: KProxy k) -> (forall a. Sing a -> r) -> r
- singByProxy :: SingI a => proxy a -> Sing a
- singByProxy# :: SingI a => Proxy# a -> Sing a
- withSing :: SingI a => (Sing a -> b) -> b
- singThat :: forall a. (SingKind (KProxy :: KProxy k), SingI a) => (Demote a -> Bool) -> Maybe (Sing a)
- bugInGHC :: forall a. a
- type family Error str :: k
- sError :: Sing (str :: Symbol) -> a
- data KProxy t = KProxy
- data Proxy t = Proxy
Main singleton definitions
See also Sing
for exported constructors
A SingI
constraint is essentially an implicitly-passed singleton.
If you need to satisfy this constraint with an explicit singleton, please
see withSingI
.
Produce the singleton explicitly. You will likely need the ScopedTypeVariables
extension to use this method the way you want.
SingI Bool False | |
SingI Bool True | |
SingI Ordering LT | |
SingI Ordering EQ | |
SingI Ordering GT | |
Typeable * a => SingI * a | |
KnownNat n => SingI Nat n | |
KnownSymbol n => SingI Symbol n | |
SingI () () | |
SingI [k] ([] k) | |
SingI (Maybe k) (Nothing k) | |
SingI a0 n0 => SingI (Maybe a) (Just a n) | |
(SingI a0 n0, SingI [a0] n1) => SingI [a] (: a n n) | |
SingI b0 n0 => SingI (Either k b) (Right k b n) | |
SingI a0 n0 => SingI (Either a k) (Left a k n) | |
(SingI a0 n0, SingI b0 n1) => SingI ((,) a b) ((,) a b n n) | |
(SingI a0 n0, SingI b0 n1, SingI c0 n2) => SingI ((,,) a b c) ((,,) a b c n n n) | |
(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3) => SingI ((,,,) a b c d) ((,,,) a b c d n n n n) | |
(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4) => SingI ((,,,,) a b c d e) ((,,,,) a b c d e n n n n n) | |
(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4, SingI f0 n5) => SingI ((,,,,,) a b c d e f) ((,,,,,) a b c d e f n n n n n n) | |
(SingI a0 n0, SingI b0 n1, SingI c0 n2, SingI d0 n3, SingI e0 n4, SingI f0 n5, SingI g0 n6) => SingI ((,,,,,,) a b c d e f g) ((,,,,,,) a b c d e f g n n n n n n n) |
class kparam ~ KProxy => SingKind kparam whereSource
The SingKind
class is essentially a kind class. It classifies all kinds
for which singletons are defined. The class supports converting between a singleton
type and the base (unrefined) type which it is built from.
type DemoteRep kparam :: *Source
Get a base type from a proxy for the promoted kind. For example,
DemoteRep ('KProxy :: KProxy Bool)
will be the type Bool
.
fromSing :: Sing (a :: k) -> DemoteRep kparamSource
Convert a singleton to its unrefined version.
toSing :: DemoteRep kparam -> SomeSing kparamSource
Convert an unrefined type to an existentially-quantified singleton type.
Working with singletons
type KindOf a = (KProxy :: KProxy k)Source
Convenient synonym to refer to the kind of a type variable:
type KindOf (a :: k) = ('KProxy :: KProxy k)
type Demote a = DemoteRep (KProxy :: KProxy k)Source
Convenient abbreviation for DemoteRep
:
type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)
data SingInstance a whereSource
A SingInstance
wraps up a SingI
instance for explicit handling.
SingInstance :: SingI a => SingInstance a |
data SomeSing kproxy whereSource
An existentially-quantified singleton. This type is useful when you want a singleton type, but there is no way of knowing, at compile-time, what the type index will be. To make use of this type, you will generally have to use a pattern-match:
foo :: Bool -> ... foo b = case toSing b of SomeSing sb -> {- fancy dependently-typed code with sb -}
An example like the one above may be easier to write using withSomeSing
.
singInstance :: forall a. Sing a -> SingInstance aSource
Get an implicit singleton (a SingI
instance) from an explicit one.
withSingI :: Sing n -> (SingI n => r) -> rSource
Convenience function for creating a context with an implicit singleton available.
:: SingKind (KProxy :: KProxy k) | |
=> DemoteRep (KProxy :: KProxy k) | The original datatype |
-> (forall a. Sing a -> r) | Function expecting a singleton |
-> r |
Convert a normal datatype (like Bool
) to a singleton for that datatype,
passing it into a continuation.
singByProxy :: SingI a => proxy a -> Sing aSource
Allows creation of a singleton when a proxy is at hand.
singByProxy# :: SingI a => Proxy# a -> Sing aSource
Allows creation of a singleton when a proxy#
is at hand.
withSing :: SingI a => (Sing a -> b) -> bSource
A convenience function useful when we need to name a singleton value
multiple times. Without this function, each use of sing
could potentially
refer to a different singleton, and one has to use type signatures (often
with ScopedTypeVariables
) to ensure that they are the same.
singThat :: forall a. (SingKind (KProxy :: KProxy k), SingI a) => (Demote a -> Bool) -> Maybe (Sing a)Source
A convenience function that names a singleton satisfying a certain
property. If the singleton does not satisfy the property, then the function
returns Nothing
. The property is expressed in terms of the underlying
representation of the singleton.
Auxiliary functions
GHC 7.8 sometimes warns about incomplete pattern matches when no such
patterns are possible, due to GADT constraints.
See the bug report at https://ghc.haskell.org/trac/ghc/ticket/3927.
In such cases, it's useful to have a catch-all pattern that then has
bugInGHC
as its right-hand side.
data KProxy t
A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only
data Proxy t
A concrete, poly-kinded proxy type