The singletons package

[Tags: bsd3, library]

This library generates singleton types, promoted functions, and singleton functions using Template Haskell. It is useful for programmers who wish to use dependently typed programming techniques. The library was originally presented in Dependently Typed Programming with Singletons, published at the Haskell Symposium, 2012. (http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf) As of this release date, Haddock was not able to properly process the code and produce documentation. Hence, all of the documentation is in the README file distributed with the package. This README is also accessible from the project home page.


[Skip to ReadMe]

Properties

Versions0.8, 0.8.1, 0.8.2, 0.8.3, 0.8.4, 0.8.5, 0.8.6, 0.9.0, 0.9.1, 0.9.2, 0.9.3, 0.10.0, 1.0, 1.1, 1.1.1, 1.1.2, 1.1.2.1
Change logCHANGES
Dependenciesbase (==4.*), containers (>=0.5), mtl (>=2.1.1), syb (>=0.3), template-haskell (>=2.8) [details]
LicenseBSD3
AuthorRichard Eisenberg <eir@cis.upenn.edu>
MaintainerRichard Eisenberg <eir@cis.upenn.edu>
Stabilityexperimental
CategoryDependent Types
Home pagehttp://www.cis.upenn.edu/~eir/packages/singletons
UploadedWed Sep 12 20:58:19 UTC 2012 by RichardEisenberg
DistributionsLTSHaskell:1.1.2.1, Stackage:1.1.2.1
Downloads5749 total (431 in last 30 days)
Votes
0 []
StatusDocs not available [build log]
Successful builds reported [all 2 reports]

Modules

Downloads

Maintainers' corner

For package maintainers and hackage trustees

Readme for singletons-0.8.2

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 (September 12, 2012), 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, eir@cis.upenn.edu.
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-dpeth explanation of these
definitions.


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 SingE (a :: k) where
  type Demote a :: *
  fromSing :: Sing a -> Demote (Any :: k)

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 'Demote' associated
kind-indexed type family maps, for example, types of the kind @Nat@
back to the type @Nat@.


class (SingI a, SingE a) => SingRep a
instance (SingI a, SingE a) => SingRep a

'SingRep' is a synonym for @('SingI' a, 'SingE' 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 (b ~ Any) => SingKind (b :: 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 (Any :: k)@ is defined.


class (t ~ Any) => SEq (t :: 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.


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

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 eir@cis.upenn.edu) 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.