Module documentation for 1.0
This is the README file for the singletons library. This file contains all the documentation for the definitions and functions in the library.
The singletons library was written by Richard Eisenberg, firstname.lastname@example.org, and with significant contributions by Jan Stolarek, email@example.com. There are two papers that describe the library. Original one, Dependently typed programming with singletons, is available here and will be referenced in this documentation as the “singletons paper”. A follow-up paper, Promoting Functions to Type Families in Haskell, will be available online Real Soon Now and will be referenced in this documentation as the “promotion paper”.
Purpose of the singletons library
The library contains a definition of singleton types, which allow programmers to use dependently typed techniques to enforce rich constraints among the types in their programs. See the singletons paper for a more thorough introduction.
The package also allows promotion of term-level functions to type-level
equivalents. Accordingly, it exports a Prelude of promoted and singletonized
functions, mirroring functions and datatypes found in Prelude,
Data.List. See the promotion
paper for a more thorough introduction.
The singletons library requires GHC 7.8.2 or greater. We plan to restore GHC 7.6.3 support, but no promises as to when will this happen. Any code that uses the singleton generation primitives needs to enable a long list of GHC extensions. This list includes, but is not necessarily limited to, the following:
Modules for singleton types
Data.Singletons exports all the basic singletons definitions. Import this
module if you are not using Template Haskell and wish only to define your
Data.Singletons.TH exports all the definitions needed to use the Template
Haskell code to generate new singletons.
Data.Singletons along with singleton
definitions for various Prelude types. This module provides a singletonized
equivalent of the real
Prelude. Note that not all functions from original
Prelude could be turned into singletons.
Data.Singletons.Prelude.* modules provide singletonized equivalents of
definitions found in the following
base library modules:
GHC.Base. We also
Data.Singletons.Decide exports type classes for propositional equality.
Data.Singletons.TypeLits exports definitions for working with
In GHC 7.6.3,
Data.Singletons.TypeLits defines and exports
KnownSymbol, which are part of
GHC.TypeLits in GHC 7.8. This makes
cross-version support a little easier.
Data.Singletons.Void exports a
Void type, shamelessly copied from
void package, but without the great many package dependencies
Data.Singletons.Types exports a few type-level definitions that are in
base for GHC 7.8, but not in GHC 7.6.3. By importing this package, users
of both GHC versions can access these definitions.
Modules for function promotion
Data.Promotion namespace provide functionality required for
function promotion. They mostly re-export a subset of definitions from
Data.Promotion.TH exports all the definitions needed to use the Template
Haskell code to generate promoted definitions.
Data.Promotion.Prelude.* modules re-export all
promoted definitions from respective
Data.Promotion.Prelude.List adds a significant amount of functions
that couldn’t be singletonized but can be promoted. Some functions still don’t
promote - these are documented in the source code of the module. There is also
Data.Promotion.Prelude.Bounded module that provides promoted
Functions to generate singletons
The top-level functions used to generate singletons are documented in the
Data.Singletons.TH module. The most common case is just calling
which I’ll describe here:
singletons :: Q [Dec] -> Q [Dec]
Generates singletons from the definitions given. Because singleton generation requires promotion, this also promotes all of the definitions given to the type level.
$(singletons [d| data Nat = Zero | Succ Nat pred :: Nat -> Nat pred Zero = Zero pred (Succ n) = n |])
Definitions used to support singletons
Please refer to the singletons paper for a more in-depth explanation of these definitions. Many of the definitions were developed in tandem with Iavor Diatchki.
data family Sing (a :: k)
The data family of singleton types. A new instance of this data family is generated for every new singleton type.
class SingI (a :: k) where sing :: Sing a
A class used to pass singleton values implicitly. The
sing method produces
an explicit singleton value.
data SomeSing (kproxy :: KProxy k) where SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)
SomeSing type wraps up an existentially-quantified singleton. Note that
the type parameter
a does not appear in the
SomeSing type. Thus, this type
can be used when you have a singleton, but you don’t know at compile time what
it will be.
SomeSing ('KProxy :: KProxy Thing) is isomorphic to
class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where type DemoteRep kparam :: * fromSing :: Sing (a :: k) -> DemoteRep kparam toSing :: DemoteRep kparam -> SomeSing kparam
This class is used to convert a singleton value back to a value in the
original, unrefined ADT. The
fromSing method converts, say, a
Nat back to an ordinary
toSing method produces
an existentially-quantified singleton, wrapped up in a
kind-indexed type family maps a proxy of the kind
back to the type
data SingInstance (a :: k) where SingInstance :: SingI a => SingInstance a singInstance :: Sing a -> SingInstance a
Sometimes you have an explicit singleton (a
Sing) where you need an implicit
one (a dictionary for
SingInstance type simply wraps a
dictionary, and the
singInstance function produces this dictionary from an
explicit singleton. The
singInstance function runs in constant time, using
a little magic.
There are two different notions of equality applicable to singletons: Boolean equality and propositional equality.
Boolean equality is implemented in the type family
(:==)(which is actually a synonym for the type family
Data.Type.Equality) and the class
SEq. See the
Data.Singletons.Prelude.Eqmodule for more information.
Propositional equality is implemented through the constraint
(~), the type
(:~:), and the class
SDecide. See modules
Data.Singletons.Decidefor more information.
Which one do you need? That depends on your application. Boolean equality has the advantage that your program can take action when two types do not equal, while propositional equality has the advantage that GHC can use the equality of types during type inference.
Instances of both
SDecide are generated when
singletons is called
on a datatype that has
deriving Eq. You can also generate these instances
directly through functions exported from
The singletons library defines a number of singleton types and functions by default:
- tuples up to length 7
These are all available through
Data.Singletons.Prelude. Functions that
operate on these singletons are available from modules such as
Function promotion allows to generate type-level equivalents of term-level definitions. Almost all Haskell source constructs are supported – see last section of this README for a full list.
Promoted definitions are usually generated by calling
$(promote [d| data Nat = Zero | Succ Nat pred :: Nat -> Nat pred Zero = Zero pred (Succ n) = n |])
Every promoted function and data constructor definition comes with a set of
so-called “symbols”. These are required to represent partial application at the
type level. Each function gets N+1 symbols, where N is the arity. Symbols
represent application of between 0 to N arguments. When calling any of the
promoted definitions it is important refer to it using their symbol
name. Moreover, there is new function application at the type level represented
Apply type family. Symbol representing arity X can have X arguments passed
in using normal function application. All other parameters must be passed by
Users also have access to
Data.Promotion.Prelude and its submodules (
Tuple). These provide promoted versions
of function found in GHC’s base library.
Refer to the promotion paper for more details on function promotion.
The singletons library has to produce new names for the new constructs it generates. Here are some examples showing how this is done:
SNat(which is really a synonym for
'Succ(you can use
There are some special cases:
All tuples (including the 0-tuple, unit) are treated similarly.
Supported Haskell constructs
The following constructs are fully supported:
- if statements
- infix expressions
- aliased patterns
- deriving Eq
- class constraints (though these sometimes fail with
- literals (for
- unboxed tuples (which are treated as normal tuples)
- pattern guards
- lambda expressions
The following constructs are supported for promotion but not singleton generation:
~patterns (silently but successfully ignored during promotion)
- class and instance declarations
- deriving of promoted
- scoped type variables
- overlapping patterns (GHC 7.8.2+ only). Note that overlapping patterns are
sometime not obvious. For example
filterfunction does not singletonize due to overlapping patterns:
filter :: (a -> Bool) -> [a] -> [a] filter _pred  =  filter pred (x:xs) | pred x = x : filter pred xs | otherwise = filter pred xs
Overlap is caused by
otherwise catch-all guard, that is always true and this
pred x guard.
The following constructs are not supported:
- list comprehensions
- arithmetic sequences
- datatypes that store arrows
Why are these out of reach? First two depend on monads, which mention a
higher-kinded type variable. GHC does not support higher-sorted kind variables,
which would be necessary to promote/singletonize monads. There are other tricks
possible, too, but none are likely to work. See the bug report
here for more info.
Arithmetic sequences are defined using
Enum typeclass, which uses infinite
As described in the promotion paper, promotion of datatypes that store arrows is currently impossible. So if you have a declaration such as
data Foo = Bar (Bool -> Maybe Bool)
you will quickly run into errors.
Literals are problematic because we rely on GHC’s built-in support, which
currently is limited. Functions that operate on strings will not work because
type level strings are no longer considered lists of characters. Function
working on integer literals can be promoted by rewriting them to use
Nat does not exist at the term level it will only be possible to
use the promoted definition, but not the original, term-level one.
The built-in Haskell promotion mechanism does not yet have a full story around
* (the kind of types that have values). Ideally, promoting some form
TypeRep would yield
*, but the implementation of TypeRep would have to be
updated for this to really work out. In the meantime, users who wish to
experiment with this feature have two options:
Data.Singletons.TypeRepStarhas all the definitions possible for making
*the promoted version of
TypeRepis currently implemented. The singleton associated with
TypeRephas one constructor:
data instance Sing (a :: *) where STypeRep :: Typeable a => Sing a
Thus, an implicit
TypeRep is stored in the singleton constructor. However,
any datatypes that store
TypeReps will not generally work as expected; the
built-in promotion mechanism will not promote
- The module
Data.Singletons.CustomStarallows the programmer to define a subset of types with which to work. See the Haddock documentation for the function
singletonStarfor more info.
- Due to GHC bug #9081 deriving of hand-written instances of
Boundedis not supported. Your only option here is to have these instances derived automatically.
- Fixity declarations don’t promote due to GHC bug #9066.
- Instances with overlapping patterns don’t promote. This will be fixed Real Soon Now.
- Top-level eta-reduced patterns don’t singletonize
- Record updates don’t singletonize
Changes from earlier versions
singletons 1.0 provides promotion mechanism that supports case expressions, let statements, anonymous functions, higher order functions and many other features. This version of the library was published together with the promotion paper.
singletons 0.9 contains a bit of an API change from previous versions. Here is a summary:
There are no more “smart” constructors. Those were necessary because each singleton used to carry both explicit and implicit versions of any children nodes. However, this leads to exponential overhead! Now, the magic (i.e., a use of
singInstancegets rid of the need for storing implicit singletons. The smart constructors did some of the work of managing the stored implicits, so they are no longer needed.
SingRepare gone. If you need to carry an implicit singleton, use
SingI. Otherwise, you probably want
The Template Haskell functions are now exported from
The Prelude singletons are now exported from
Changelog for singletons project
Template Haskell names are now more hygienic. In other words,
won’t try to gobble up something happened to be named
Sing in your project.
(Note that the Template Haskell names are not completely hygienic; names
generated during singleton generation can still cause conflicts.)
If a function to be promoted or singletonized is missing a type signature, that is now an error, not a warning.
Added a new external module Data.Singletons.TypeLits, which contain the singletons for GHC.TypeLits. Some convenience functions are also provided.
EmptyCase is no longer needed. This caused pain when trying
to support both GHC 7.6.3 and 7.8.
Fix export list of Data.Singletons.TH, again again.
SEq instances for
Fix export list of Data.Singletons.TH, again.
Fix export list of Data.Singletons.TH.
Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.
Change module structure significantly. If you want to derive your own
singletons, you should import
Data.Singletons.TH. The module
Data.Singletons now exports functions only for the use of singletons.
are just like their equivalents from
Data., except for
List, which is
quite lacking in features.
For singleton equality, use
For propositional singleton equality, use
Data.Singletons.Prelude is meant to mirror the Haskell Prelude,
but with singleton definitions.
Streamline representation of singletons, resulting in exponential speedup at execution. (This has not been rigorously measured, but the data structures are now exponentially smaller.)
Add internal support for TypeLits, because the TypeLits module no longer exports singleton definitions.
Add support for existential singletons, through the
toSing method of
SingE class, bundling its functionality into
SingRep synonym has also been removed.
Add support for singletonizing calls to
Add support for singletonizing empty data definitions.
Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.
Bug fix to make singletons compatible with GHC 7.6.1.
Added git info to cabal file.
Update to work with latest version of GHC (7.7.20130114).
Now use branched type family instances to allow for promotion of functions with overlapping patterns.
Permit promotion of functions with constraints by omitting constraints.
Update to work with latest version of GHC (7.7.20121031).
Removed use of Any to simulate kind classes; now using KindOf and OfKind from GHC.TypeLits.
Made compatible with GHC.TypeLits.
Added this changelog
Update to work with latest version of GHC (7.6.1). (There was a change to Template Haskell).
Moved library into Data.Singletons.
Update to work with latest version of GHC. (There was a change to Template Haskell).
Updated dependencies in cabal to include the newer version of TH.
Initial public release