singletons 2.2

Build Status

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, [email protected], and with significant contributions by Jan Stolarek, [email protected]. There are two papers that describe the library. Original one, Dependently typed programming with singletons, is available here and will be referenced in this documentation as the “singletons paper”. A follow-up paper, Promoting Functions to Type Families in Haskell, is available here and will be referenced in this documentation as the “promotion paper”.

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 singletons paper for a more thorough introduction.

The package also allows promotion of term-level functions to type-level equivalents. Accordingly, it exports a Prelude of promoted and singletonized functions, mirroring functions and datatypes found in Prelude, Data.Bool, Data.Maybe, Data.Either, Data.Tuple and Data.List. See the promotion paper for a more thorough introduction.

Compatibility

The singletons library requires GHC 8.0.1 or greater. Any code that uses the singleton generation primitives needs to enable a long list of GHC extensions. This list includes, but is not necessarily limited to, the following:

  • ScopedTypeVariables
  • TemplateHaskell
  • TypeFamilies
  • GADTs
  • KindSignatures
  • TypeOperators
  • FlexibleContexts
  • RankNTypes
  • UndecidableInstances
  • FlexibleInstances
  • InstanceSigs
  • DefaultSignatures
  • TypeInType

You may also want

  • -Wno-redundant-constraints

as the code that singletons generates uses redundant constraints, and there seems to be no way, without a large library redesign, to avoid this.

Modules for singleton types

Data.Singletons exports all the basic singletons definitions. Import this module if you are not using Template Haskell and wish only to define your own singletons.

Data.Singletons.TH exports all the definitions needed to use the Template Haskell code to generate new singletons.

Data.Singletons.Prelude re-exports Data.Singletons along with singleton definitions for various Prelude types. This module provides a singletonized equivalent of the real Prelude. Note that not all functions from original Prelude could be turned into singletons.

Data.Singletons.Prelude.* modules provide singletonized equivalents of definitions found in the following base library modules: Data.Bool, Data.Maybe, Data.Either, Data.List, Data.Tuple and GHC.Base. We also provide singletonized Eq and Ord typeclasses

Data.Singletons.Decide exports type classes for propositional equality.

Data.Singletons.TypeLits exports definitions for working with GHC.TypeLits.

Data.Singletons.Void exports a Void type, shamelessly copied from Edward Kmett’s void package, but without the great many package dependencies in void.

Modules for function promotion

Modules in Data.Promotion namespace provide functionality required for function promotion. They mostly re-export a subset of definitions from respective Data.Singletons modules.

Data.Promotion.TH exports all the definitions needed to use the Template Haskell code to generate promoted definitions.

Data.Promotion.Prelude and Data.Promotion.Prelude.* modules re-export all promoted definitions from respective Data.Singletons.Prelude modules. Data.Promotion.Prelude.List adds a significant amount of functions that couldn’t be singletonized but can be promoted. Some functions still don’t promote - these are documented in the source code of the module. There is also Data.Promotion.Prelude.Bounded module that provides promoted PBounded typeclass.

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.

Usage example:

$(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 singletons paper 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.

  • Boolean equality is implemented in the type family (:==) (which is actually a synonym for the type family (==) from Data.Type.Equality) and the class SEq. See the Data.Singletons.Prelude.Eq module for more information.

  • Propositional equality is implemented through the constraint (~), the type (:~:), and the class SDecide. See modules Data.Type.Equality and Data.Singletons.Decide for more information.

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:

  • Bool
  • Maybe
  • Either
  • Ordering
  • ()
  • tuples up to length 7
  • lists

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.

Promoting functions

Function promotion allows to generate type-level equivalents of term-level definitions. Almost all Haskell source constructs are supported – see last section of this README for a full list.

Promoted definitions are usually generated by calling promote function:

$(promote [d|
  data Nat = Zero | Succ Nat
  pred :: Nat -> Nat
  pred Zero = Zero
  pred (Succ n) = n
  |])

Every promoted function and data constructor definition comes with a set of so-called “symbols”. These are required to represent partial application at the type level. Each function gets N+1 symbols, where N is the arity. Symbols represent application of between 0 to N arguments. When calling any of the promoted definitions it is important refer to it using their symbol name. Moreover, there is new function application at the type level represented by Apply type family. Symbol representing arity X can have X arguments passed in using normal function application. All other parameters must be passed by calling Apply.

Users also have access to Data.Promotion.Prelude and its submodules (Base, Bool, Either, List, Maybe and Tuple). These provide promoted versions of function found in GHC’s base library.

Note that GHC resolves variable names in Template Haskell quotes. You cannot then use an undefined identifier in a quote, making idioms like this not work:

type family Foo a where ...
$(promote [d| ... foo x ... |])

In this example, foo would be out of scope.

Refer to the promotion paper for more details on function promotion.

Classes and instances

This is best understood by example. Let’s look at a stripped down Ord:

class Eq a => Ord a where
  compare :: a -> a -> Ordering
  (<)     :: a -> a -> Bool
  x < y = case x `compare` y of
            LT -> True
	    EQ -> False
	    GT -> False

This class gets promoted to a “kind class” thus:

class (kproxy ~ 'KProxy, PEq kproxy) => POrd (kproxy :: KProxy a) where
  type Compare (x :: a) (y :: a) :: Ordering
  type (:<)    (x :: a) (y :: a) :: Bool
  type x :< y = ... -- promoting `case` is yucky.

Note that default method definitions become default associated type family instances. This works out quite nicely.

We also get this singleton class:

class (kproxy ~ 'KProxy, SEq kproxy) => SOrd (kproxy :: KProxy a) where
  sCompare :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Compare x y)
  (%:<)    :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x :< y)

  default (%:<) :: forall (x :: a) (y :: a).
                   ((x :< y) ~ {- RHS from (:<) above -})
		=> Sing x -> Sing y -> Sing (x :< y)
  x %:< y = ...  -- this is a bit yucky too

Note that a singletonized class needs to use default signatures, because type-checking the default body requires that the default associated type family instance was used in the promoted class. The extra equality constraint on the default signature asserts this fact to the type-checker.

Instances work roughly similarly.

instance Ord Bool where
  compare False False = EQ
  compare False True  = LT
  compare True  False = GT
  compare True  True  = EQ

instance POrd ('KProxy :: KProxy Bool) where
  type Compare 'False 'False = 'EQ
  type Compare 'False 'True  = 'LT
  type Compare 'True  'False = 'GT
  type Compare 'True  'True  = 'EQ

instance SOrd ('KProxy :: KProxy Bool) where
  sCompare :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Compare x y)
  sCompare SFalse SFalse = SEQ
  sCompare SFalse STrue  = SLT
  sCompare STrue  SFalse = SGT
  sCompare STrue  STrue  = SEQ

The only interesting bit here is the instance signature. It’s not necessary in such a simple scenario, but more complicated functions need to refer to scoped type variables, which the instance signature can bring into scope. The defaults all just work.

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:

  1. original datatype: Nat

    promoted kind: Nat

    singleton type: SNat (which is really a synonym for Sing)

  2. original datatype: :/\:

    promoted kind: :/\:

    singleton type: :%/\:

  3. original constructor: Succ

    promoted type: 'Succ (you can use Succ when unambiguous)

    singleton constructor: SSucc

    symbols: SuccSym0, SuccSym1

  4. original constructor: :+:

    promoted type: ':+:

    singleton constructor: :%+:

    symbols: :+:$, :+:$$, :+:$$$

  5. original value: pred

    promoted type: Pred

    singleton value: sPred

    symbols: PredSym0, PredSym1

  6. original value: +

    promoted type: :+

    singleton value: %:+

    symbols: :+$, :+$$, :+$$$

  7. original class: Num

    promoted class: PNum

    singleton class: SNum

  8. original class: ~>

    promoted class: #~>

    singleton class: :%~>

Special names

There are some special cases:

  1. original datatype: []

    singleton type: SList

  2. original constructor: []

    promoted type: '[]

    singleton constructor: SNil

    symbols: NilSym0

  3. original constructor: :

    promoted type: ':

    singleton constructr: SCons

    symbols: ConsSym0, ConsSym1

  4. original datatype: (,)

    singleton type: STuple2

  5. original constructor: (,)

    promoted type: '(,)

    singleton constructor: STuple2

    symbols: Tuple2Sym0, Tuple2Sym1, Tuple2Sym2

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

  6. original value: undefined

    promoted type: Any

    singleton value: undefined

Supported Haskell constructs

The following constructs are fully supported:

  • variables
  • tuples
  • constructors
  • if statements
  • infix expressions
  • _ patterns
  • aliased patterns
  • lists
  • sections
  • undefined
  • error
  • deriving Eq, Ord, Bounded, and Enum
  • class constraints (though these sometimes fail with let, lambda, and case)
  • literals (for Nat and Symbol), including overloaded number literals
  • unboxed tuples (which are treated as normal tuples)
  • records
  • pattern guards
  • case
  • let
  • lambda expressions
  • ! and ~ patterns (silently but successfully ignored during promotion)
  • class and instance declarations
  • functional dependencies (with limitations – see below)

The following constructs are supported for promotion but not singleton generation:

  • scoped type variables
  • overlapping patterns. Note that overlapping patterns are sometimes not obvious. For example, the filter function does not singletonize due to overlapping patterns:
filter :: (a -> Bool) -> [a] -> [a]
filter _pred []    = []
filter pred (x:xs)
  | pred x         = x : filter pred xs
  | otherwise      = filter pred xs

Overlap is caused by otherwise catch-all guard, that is always true and this overlaps with pred x guard.

The following constructs are not supported:

  • list comprehensions
  • do
  • arithmetic sequences
  • datatypes that store arrows, Nat, or Symbol
  • literals (limited support)

Why are these out of reach? First two depend on monads, which mention a higher-kinded type variable. GHC does not support higher-sorted kind variables, which would be necessary to promote/singletonize monads. There are other tricks possible, too, but none are likely to work. See the bug report here for more info. Arithmetic sequences are defined using Enum typeclass, which uses infinite lists.

As described in the promotion paper, promotion of datatypes that store arrows is currently impossible. So if you have a declaration such as

data Foo = Bar (Bool -> Maybe Bool)

you will quickly run into errors.

Literals are problematic because we rely on GHC’s built-in support, which currently is limited. Functions that operate on strings will not work because type level strings are no longer considered lists of characters. Function working on integer literals can be promoted by rewriting them to use Nat. Since Nat does not exist at the term level it will only be possible to use the promoted definition, but not the original, term-level one.

This is the same line of reasoning that forbids the use of Nat or Symbol in datatype definitions. But, see this bug report for a workaround.

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.

Known bugs

  • Record updates don’t singletonize
  • In obscure scenarios, GHC “forgets” constraints on functions. This should happen only with certain uses where the constraint is needed inside of a case or lambda-expression. Having type inference on result types nearby makes this more likely to bite.
  • Inference dependent on functional dependencies is unpredictably bad. The problem is that a use of an associated type family tied to a class with fundeps doesn’t provoke the fundep to kick in. This is GHC’s problem, in the end.

Changes

Changelog for singletons project

2.2

  • With TypeInType, we no longer kind KProxy. @int-index has very helpfully removed the use of KProxy from singletons.

  • Drop support for GHC 7.x.

  • Remove bugInGHC. That function was intended to work around GHC’s difficulty in detecting exhaustiveness of GADT pattern matches. GHC 8 comes with a much better exhaustiveness checker, and so this function is no longer necessary.

2.1

  • Require th-desugar >= 1.6

  • Work with GHC 8. GHC 8 gives the opportunity to simplify some pieces of singletons, but these opportunities are not yet fully realized. For example, injective type families means that we no longer need Sing to be a data family; it could be a type family. This might drastically simplify the way functions are singletonized. But not yet!

  • singletons now outputs a few more type/kind annotations to help GHC do type inference. There may be a few more programs accepted than before. (This is the fix for #136.)

2.0.1

  • Lots more functions in Data.Singletons.Prelude.List: filter, find, elemIndex, elemIndices, findIndex, findIndices, intersect, intersectBy, takeWhile, dropWhile, dropWhileEnd, span, break, take, drop, splitAt, group, maximum, minimum, insert, sort, groupBy, lookup, partition, sum, product, length, replicate, transpose, (!!), nub, nubBy, unionBy, union, genericLength

2.0.0.2

  • Fix fixity of *.

2.0.0.1

  • Make haddock work.

2.0

  • Instance promotion now works properly – it was quite buggy in 1.0.

  • Classes and instances can now be singletonized.

  • Limited support for functional dependencies.

  • We now have promoted and singletonized versions of Enum, as well as Bounded.

  • Deriving Enum is also now supported.

  • Ditto for Num, which includes an instance for Nat, naturally.

  • Promoting a literal number now uses overloaded literals at the type level, using a type-level FromInteger in the type-level Num class.

  • Better support for dealing with constraints. Some previously-unsingletonizable functions that have constrained parameters now work.

  • No more orphan Quasi instances!

  • Support for functions of arity 8 (instead of the old limit, 7).

  • Full support for fixity declarations.

  • A raft of bugfixes.

  • Drop support for GHC 7.8. You must have GHC 7.10.2.

1.1.2.1

Fix bug #116, thus allowing locally-declared symbols to be used in GHC 7.10.

1.1.2

  • No more GHC 7.8.2 support – you must have GHC 7.8.3.

1.1.1

Update testsuite to work with th-desugar-1.5.2. No functional changes.

1.1

This is a maintenance release to support building (but not testing, due to GHC bug #10058) with 7.10. This release also targets th-desugar-1.5. Some types changed (using th-desugar’s new DsMonad instead of Quasi), but clients generally won’t need to make any changes, unless they, too, generalize over Quasi.

1.0

This is a complete rewrite of the package.

  • A much wider array of surface syntax is now accepted for promotion and singletonization, including let, case, partially-applied functions, and anonymous functions, where, sections, among others.

  • Classes and instances can be promoted (but not singletonized).

  • Derivation of promoted instances for Ord and Bounded.

This release can be seen as a “technology preview”. More features are coming soon.

This version drops GHC 7.6 support.

0.10.0

Template Haskell names are now more hygienic. In other words, singletons won’t try to gobble up something happened to be named Sing in your project. (Note that the Template Haskell names are not completely hygienic; names generated during singleton generation can still cause conflicts.)

If a function to be promoted or singletonized is missing a type signature, that is now an error, not a warning.

Added a new external module Data.Singletons.TypeLits, which contain the singletons for GHC.TypeLits. Some convenience functions are also provided.

The extension EmptyCase is no longer needed. This caused pain when trying to support both GHC 7.6.3 and 7.8.

0.9.3

Fix export list of Data.Singletons.TH, again again.

Add SEq instances for Nat and Symbol.

0.9.2

Fix export list of Data.Singletons.TH, again.

0.9.1

Fix export list of Data.Singletons.TH.

0.9.0

Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.

Change module structure significantly. If you want to derive your own singletons, you should import Data.Singletons.TH. The module Data.Singletons now exports functions only for the use of singletons.

New modules Data.Singletons.Bool, ...Maybe, ...Either, and ...List are just like their equivalents from Data., except for List, which is quite lacking in features.

For singleton equality, use Data.Singletons.Eq.

For propositional singleton equality, use Data.Singletons.Decide.

New module Data.Singletons.Prelude is meant to mirror the Haskell Prelude, but with singleton definitions.

Streamline representation of singletons, resulting in exponential speedup at execution. (This has not been rigorously measured, but the data structures are now exponentially smaller.)

Add internal support for TypeLits, because the TypeLits module no longer exports singleton definitions.

Add support for existential singletons, through the toSing method of SingKind.

Remove the SingE class, bundling its functionality into SingKind. Thus, the SingRep synonym has also been removed.

Name change: KindIs becomes KProxy.

Add support for singletonizing calls to error.

Add support for singletonizing empty data definitions.

0.8.6

Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.

0.8.5

Bug fix to make singletons compatible with GHC 7.6.1.

Added git info to cabal file.

0.8.4

Update to work with latest version of GHC (7.7.20130114).

Now use branched type family instances to allow for promotion of functions with overlapping patterns.

Permit promotion of functions with constraints by omitting constraints.

0.8.3

Update to work with latest version of GHC (7.7.20121031).

Removed use of Any to simulate kind classes; now using KindOf and OfKind from GHC.TypeLits.

Made compatible with GHC.TypeLits.

0.8.2

Added this changelog

Update to work with latest version of GHC (7.6.1). (There was a change to Template Haskell).

Moved library into Data.Singletons.

0.8.1

Update to work with latest version of GHC. (There was a change to Template Haskell).

Updated dependencies in cabal to include the newer version of TH.

0.8

Initial public release