Readme for singletons-0.9.3

singletons 0.9.3

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, eir@cis.upenn.edu. See also Dependently typed programming with singletons, available here.

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.3 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:

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 singletons, 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.

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. 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)

The 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 Thing.

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 singleton Nat back to an ordinary Nat. The toSing method produces an existentially-quantified singleton, wrapped up in a SomeSing. The DemoteRep associated kind-indexed type family maps a proxy of the kind Nat back to the type Nat.

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 SingI). The SingInstance type simply wraps a SingI dictionary, and the singInstance function produces this dictionary from an explicit singleton. The singInstance function runs in constant time, using a little magic.

Equality classes

There are two different notions of equality applicable to singletons: Boolean equality and propositional equality.

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 SEq and 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 Data.Singletons.TH.

Pre-defined singletons

The singletons library defines a number of singleton types and functions by default:

These are all available through Data.Singletons.Prelude. Functions that operate on these singletons are available from modules such as Data.Singletons.Bool and Data.Singletons.Maybe.

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 (you can use Zero when unambiguous)
singleton constructor: SZero

original constructor: :+:
promoted type: ':+:
singleton 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

original constructor: :
singleton constructor: SCons

original datatype: (,)
singleton type: STuple2

original constructor: (,)
singleton constructor: STuple2

All tuples (including the 0-tuple, unit) are treated similarly.

original value: undefined
promoted type: Any
singleton value: undefined

Supported Haskell constructs

The following constructs are fully supported:

The following constructs will be coming soon:

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 *.

  1. The module Data.Singletons.CustomStar allows the programmer to define a subset of types with which to work. See the Haddock documentation for the function singletonStar for more info.

Changes from earlier versions

singletons 0.9 contains a bit of an API change from previous versions. Here is a summary: