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 (June 2, 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.5.20120529 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 Singletons.Lib.

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

The following constructs are fully supported:

• variables
• tuples
• constructors
• 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.

---

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