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