singletons
==========
This is the README file for the singletons library. This file contains all the
documentation for the definitions and functions in the library. As of the time
of this writing (January 16, 2013), haddock has not quite caught up with GHC in
handling kind-polymorphic code, and the HEAD version of haddock cannot process
Template Haskell. Thus, the documentation is in here. In the future, it will
be generated by haddock.
The singletons library was written by Richard Eisenberg, [email protected].
See also /Dependently typed programming with singletons/, available at
<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>
---------------------------------
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 paper cited above for a
more thorough introduction.
-------------
Compatibility
-------------
The singletons library requires GHC version 7.6.1 or greater.
Any code that uses the singleton generation primitives will also need
to enable a long list of GHC extensions. This list includes, but
is not necessarily limited to, the following:
* TemplateHaskell
* TypeFamilies
* GADTs
* KindSignatures
* DataKinds
* PolyKinds
* TypeOperators
* FlexibleContexts
* RankNTypes
* UndecidableInstances
* FlexibleInstances
In addition, @ScopedTypeVariables@ is often very helpful.
--------------------------------
Functions to generate singletons
--------------------------------
There are four top-level functions used to generate the singleton definitions.
These functions should all be used within top-level Template Haskell splices.
See #supported-features# for a list of what Haskell constructs are supported.
These functions are all defined in Data.Singletons.
genPromotion :: [Name] -> Q [Dec]
Takes a list of names of types and promotes them to the kind level. Although
@DataKinds@ does this promotion automaticlly, the manual promotion also
handles generating instances of @:==:@, Boolean equality at the type level,
for type that derive @Eq@.
To use:
> $(genPromotion [''Bool, ''Maybe])
genSingletons :: [Name] -> Q [Dec]
Takes a list of names of types and generates singleton type definitions
for them.
To use:
> $(genSingletons [''Bool, ''Maybe])
promote :: Q [Dec] -> Q [Dec]
Promotes the declarations given.
To use:
> $(promote [d|
> data Nat = Zero | Succ Nat
> pred :: Nat -> Nat
> pred Zero = Zero
> pred (Succ n) = n
> |])
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 use:
> $(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 paper cited above for a more in-depth explanation of these
definitions.
-----
NOTE: The original paper used a trick with the GHC primitive 'Any' to simulate
kind classes and to perform other shenanigans. 'Any' is like undefined at the
type level. GHC has evolved to prevent pattern-matching on 'Any', which is a
Good Thing. This means that some of singletons's uses of 'Any' were invalid.
These were replaced with a kind-level proxy, defined thus:
data OfKind (k :: *) = KindParam
type KindOf (a :: k) = (KindParam :: OfKind k)
The parameter must be explicitly kinded to * to prevent polymorphism, because
only monomorphic types are promoted to kinds. This definition should only be
used at the kind level.
-----
Many of the definitions were developed in tandem with Iavor Diatchki, the
maintainer of type-level literals in GHC. In GHC 7.7 , the singletons library
imports many of these definitions from GHC.TypeLits.
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.
class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where
type DemoteRep kparam :: *
fromSing :: Sing (a :: k) -> DemoteRep 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
singleton @Nat@ back to an ordinary @Nat@. The 'DemoteRep' associated
kind-indexed type family maps a proxy of the kind @Nat@
back to the type @Nat@.
class (SingI a, SingE (KindOf a)) => SingRep (a :: k)
instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)
'SingRep' is a synonym for @('SingI' a, 'SingE' (KindOf a))@.
type family (a :: k) :==: (b :: k) :: Bool
type a :== b = a :==: b
type a :/=: b = Not (a :==: b)
type a :/= b = a :/=: b
These are two equivalent forms of Boolean equality and inequality at the type
level. When promoted a datatype that derives @Eq@, instances of this type
family are generated.
data SingInstance (a :: k) where
SingInstance :: SingRep a => SingInstance a
class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where
singInstance :: forall (a :: k). Sing a -> SingInstance a
The 'SingKind' class allows for easy access to implicit parameters. The
intuition here is that for any kind @k@ with an associated singleton definition,
@SingKind (KindParam :: OfKind k)@ is defined.
class (kparam ~ KindParam) => SEq (kparam :: OfKind k) where
(%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)
(%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)
This is the equivalent of @Eq@ for singletons. It computes singleton Boolean
equality. Alternate spellings of the functions are provided: (%:==) is the
same as (%==%) and (%:/=) is the same as (%/=%). These synonyms are provided
for compatibility with generated code.
type family If (a :: Bool) (b :: k) (c :: k) :: k
This type family is a Boolean conditional at the type level. Note that type-
level computation is *strict* in GHC. Thus, you cannot use If to check a
termination condition in a recursive type family -- the type checker will
loop if you try. Corollary: you cannot use plain old 'if' to check a
termination condition in a term-level function you wish to promote or refine
into a singleton.
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
This function is a conditional for singletons.
type family Head (a :: [k]) :: k
Returns the head of a type-level list. Gets stuck when given @'[]@.
type family Tail (a :: [k]) :: [k]
Returns the tail of a type-level list. Gets stuck when given @'[]@.
-----------------------
Other utility functions
-----------------------
cases :: Name -- the type of the scrutinee
-> Q Exp -- the scrutinee
-> Q Exp -- the body of each branch
-> Q Exp -- the resulting expression
It is sometimes necessary to get GHC to do case analysis on all possible
types for a given type parameter. No matter what the type variable is, though,
the resulting action is the same. This normally takes the form of a case
statement where every branch has the same expression. The 'cases' function
generates such a case statement. For example,
> $(cases ''Bool [| not foo |] [| doSomething foo |])
expands to
> case not foo of
> True -> doSomething foo
> False -> doSomething foo
bugInGHC :: forall a. a
Currently, GHC will issue a warning for an incomplete pattern match, even
when all omitted cases can be statically proven to be impossible. For example:
> safePred :: Sing (Succ n) -> Sing n
> safePred (SSucc n) = n
With @-fwarn-incomplete-patterns@ (which we highly recommend using), GHC
warns that the pattern match is incomplete. The solution? Suppress the warning
with a wildcard pattern, using 'bugInGHC':
> safePred _ = bugInGHC
The 'bugInGHC' function just calls @error@ with an appropriate message.
----------------------
Pre-defined singletons
----------------------
The singletons library defines a number of singleton types and functions
by default:
* @Bool@
* @Maybe@
* @Either@
* @()@
* tuples up to length 7
* @not@, @&&@, @||@
* lists
* @ @
--------
On names
--------
The singletons library has to produce new names for the new constructs it
generates. Here are some examples showing how this is done:
original datatype: Nat
promoted kind: Nat
singleton type: SNat (which is really a synonym for @Sing@)
original datatype: (:/\:)
promoted kind: (:/\:)
singleton type: (:%/\:)
original constructor: Zero
promoted type: 'Zero
singleton constructor: SZero
smart constructor: sZero (see paper cited above for more info)
original constructor: : :
promoted type: ': :
singleton constructor: :% :
smart constructor: %: :
original value: pred
promoted type: Pred
singleton value: sPred
original value:
promoted type: :
singleton value: %:
Special names
-------------
There are some special cases:
original datatype: []
singleton type: SList
original constructor: []
singleton constructor: SNil
smart constructor: sNil
original constructor: :
singleton constructor: SCons
smart constructor: sCons
original datatype: (,)
singleton type: STuple2
original constructor: (,)
singleton constructor: STuple2
smart constructor: sTuple2
All tuples (including the 0-tuple, unit) are treated similarly.
original value: undefined
promoted type: Any
singleton value: undefined
----------------------------
Supported Haskell constructs
----------------------------
#supported-features#
The following constructs are fully supported:
* variables
* tuples
* constructors
* if statements
* infix expressions
* !, ~, and _ patterns
* aliased patterns (except at top-level)
* lists
* ( ) sections
* (x ) sections
* undefined
* deriving Eq
* class constraints
The following constructs will be coming soon:
* unboxed tuples
* records
* scoped type variables
* overlapping patterns
* pattern guards
* ( x) sections
* case
* let
* list comprehensions
The following constructs are problematic and are not planned to be
implemented:
* literals
* lambda expressions
* do
* arithmetic sequences
See the paper cited above for reasons why these are problematic.
As described briefly in the paper, the singletons generation mechanism does not
currently work for higher-order datatypes (though higher-order functions are
just peachy). So, if you have a declaration such as
> data Foo = Bar (Bool -> Maybe Bool)
, its singleton will not work correctly. It turns out that getting this to work
requires fairly thorough changes to the whole singleton generation scheme.
Please shout (to [email protected]) if you have a compelling use case for this
and I can take a look at it. No promises, though.
-------------
Support for *
-------------
The built-in Haskell promotion mechanism does not yet have a full story around
the kind * (the kind of types that have values). Ideally, promoting some form
of 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:
1) The module Data.Singletons.TypeRepStar has all the definitions possible for
making * the promoted version of TypeRep, as TypeRep is currently implemented.
The singleton associated with TypeRep has 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 TypeRep to *.
2) The module Singletons.CustomStar allows the programmer to define a subset
of types with which to work. A datatype @Rep@ is created, with one constructor
per type in the declared universe. When this type is promoted by the singletons
library, the constructors become full types in *, not just promoted data
constructors. The universe is specified with the @singletonStar@ function.
For example,
> $(singletonStar [''Nat, ''Bool, ''Maybe])
generates the following:
> data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)
and its singleton. However, because @Rep@ is promoted to @*@, the singleton
is perhaps slightly unexpected:
> data instance Sing (a :: *) where
> SNat :: Sing Nat
> SBool :: Sing Bool
> SMaybe :: SingRep a => Sing a -> Sing (Maybe a)
The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,
@Bool@, and @Maybe@, not just promoted data constructors.
Please note that support for * is *very* experimental. Use at your own risk.
