singletons-0.10.0: 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

Contents

Description

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.

Synopsis

Main singleton definitions

data family Sing a Source

The singleton kind-indexed data family.

Instances

TestCoercion * (Sing *) 
SDecide k (KProxy k) => TestEquality k (Sing k) 
data Sing Bool where 
data Sing Ordering where 
data Sing * where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

See also Sing for exported constructors

class SingI a where Source

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI.

Methods

sing :: Sing a Source

Produce the singleton explicitly. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Instances

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

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.

Associated Types

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.

Methods

fromSing :: Sing (a :: k) -> DemoteRep kparam Source

Convert a singleton to its unrefined version.

toSing :: DemoteRep kparam -> SomeSing kparam Source

Convert an unrefined type to an existentially-quantified singleton type.

Instances

SingKind Bool (KProxy Bool) 
SingKind Ordering (KProxy Ordering) 
SingKind * (KProxy *) 
SingKind Nat (KProxy Nat) 
SingKind Symbol (KProxy Symbol) 
SingKind () (KProxy ()) 
SingKind a0 (KProxy a0) => SingKind [a] (KProxy [a]) 
SingKind a0 (KProxy a0) => SingKind (Maybe a) (KProxy (Maybe a)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0)) => SingKind (Either a b) (KProxy (Either a b)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0)) => SingKind ((,) a b) (KProxy ((,) a b)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0)) => SingKind ((,,) a b c) (KProxy ((,,) a b c)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0)) => SingKind ((,,,) a b c d) (KProxy ((,,,) a b c d)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0)) => SingKind ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0), SingKind f0 (KProxy f0)) => SingKind ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) 
(SingKind a0 (KProxy a0), SingKind b0 (KProxy b0), SingKind c0 (KProxy c0), SingKind d0 (KProxy d0), SingKind e0 (KProxy e0), SingKind f0 (KProxy f0), SingKind g0 (KProxy g0)) => SingKind ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) 

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

A SingInstance wraps up a SingI instance for explicit handling.

Constructors

SingInstance :: SingI a => SingInstance a 

data SomeSing kproxy where Source

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.

Constructors

SomeSing :: Sing (a :: k) -> SomeSing (KProxy :: KProxy k) 

singInstance :: forall a. Sing a -> SingInstance a Source

Get an implicit singleton (a SingI instance) from an explicit one.

withSingI :: Sing n -> (SingI n => r) -> r Source

Convenience function for creating a context with an implicit singleton available.

withSomeSing Source

Arguments

:: 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 a Source

Allows creation of a singleton when a proxy is at hand.

singByProxy# :: SingI a => Proxy# a -> Sing a Source

Allows creation of a singleton when a proxy# is at hand.

withSing :: SingI a => (Sing a -> b) -> b Source

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

bugInGHC :: forall a. a Source

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

Constructors

KProxy 

data Proxy t

A concrete, poly-kinded proxy type

Constructors

Proxy 

Instances

Monad (Proxy *) 
Functor (Proxy *) 
Applicative (Proxy *) 
Bounded (Proxy k s) 
Enum (Proxy k s) 
Eq (Proxy k s) 
Data t => Data (Proxy * t) 
Ord (Proxy k s) 
Read (Proxy k s) 
Show (Proxy k s) 
Ix (Proxy k s) 
Generic (Proxy * t) 
Monoid (Proxy * s) 
Typeable (k -> *) (Proxy k) 
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1)