开源软件名称（OpenSource Name）：

开源软件地址(OpenSource Url)：

开源编程语言(OpenSource Language)：

开源软件介绍(OpenSource Introduction)：

singletons

This is the README file for the singletons, singletons-th, and singletons-base libraries. This file contains documentation for the definitions and functions in these libraries.

The singletons libraries were written by Richard Eisenberg ([email protected]) and with significant contributions by Jan Stolarek ([email protected]) and Ryan Scott ([email protected]). There are two papers that describe the libraries. 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".

Ryan Scott ([email protected]) is the active maintainer.

Purpose of the libraries

Broadly speaking, the singletons libraries define an ecosystem of singleton types, which allow programmers to use dependently typed techniques to enforce rich constraints among the types in their programs. To that end, the three libraries serve the following roles:

• The singletons library is a small, foundational library that defines basic singleton-related types and definitions.
• The singletons-th library defines Template Haskell functionality that allows promotion of term-level functions to type-level equivalents and singling functions to dependently typed equivalents.
• The singletons-base library uses singletons-th to define promoted and singled functions from the base library, including the Prelude.

Besides the functionality of the libraries themselves, singletons differs from singletons-th and singletons-base by aiming to be compatible with a wider range of GHC versions. See the "Compatibility" section for further details.

Some other introductions to the ideas in these libraries include:

• The singletons paper and promotion papers.
• This blog series, authored by Justin Le, which offers a tutorial for these libraries that assumes no knowledge of dependent types.

Compatibility

singletons, singletons-th, and singletons-base have different support windows for requirements on the compiler version needed to build each library:

• singletons is a minimal library, and as such, it has a relatively wide support window. singletons must be built with one of the following compilers:

  • GHC 8.0 or greater
  • GHCJS

• singletons-th and singletons-base require use of many bleeding-edge GHC language extensions, even more so than singletons itself. As such, it is difficult to maintain support for multiple GHC versions in any given release of either library, so they only support the latest major GHC version (currently GHC 9.2).

Any code that uses the singleton-generation functionality from singletons-th or singletons-base needs to enable a long list of GHC extensions. This list includes, but is not necessarily limited to, the following:

• DataKinds
• DefaultSignatures
• EmptyCase
• ExistentialQuantification
• FlexibleContexts
• FlexibleInstances
• GADTs
• InstanceSigs
• KindSignatures
• NoCUSKs
• NoNamedWildCards
• NoStarIsType
• PolyKinds
• RankNTypes
• ScopedTypeVariables
• StandaloneDeriving
• StandaloneKindSignatures
• TemplateHaskell
• TypeApplications
• TypeFamilies
• TypeOperators
• UndecidableInstances

Some notes on the use of No* extensions:

• NoNamedWildCards is needed since singletons-th will single code like f _x = ... to sF (_sx :: Sing _x) = ..., which crucially relies on the _x in Sing _x being treated as a type variable, not a wildcard.
• NoStarIsType is needed to use the * type family from the PNum class because with StarIsType enabled, GHC thinks * is a synonym for Type.

You may also want to consider toggling various warning flags:

• -Wno-redundant-constraints. The code that singletons generates uses redundant constraints, and there seems to be no way, without a large library redesign, to avoid this.
• -fenable-th-splice-warnings. By default, GHC does not run pattern-match coverage checker warnings on code inside of Template Haskell quotes. This is an extremely common thing to do in singletons-th, so you may consider opting in to these warnings.

Modules for singleton types

Data.Singletons (from 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.Decide (from singletons) exports type classes for propositional equality. See the "Equality classes" section for more information.

Data.Singletons.TH (from singletons-th) exports all the definitions needed to use the Template Haskell code to generate new singletons. Data.Singletons.Base.TH (from singletons-base) re-exports Data.Singletons.TH plus any promoted or singled definitions that are likely to appear in TH-generated code. For instance, singling a deriving Eq clause will make use of SEq, the singled Eq class, so Data.Singletons.TH re-exports SEq.

Prelude.Singletons (from singletons-base) re-exports Data.Singletons along with singleton definitions for various Prelude types. This module provides promoted and singled equivalents of functions from the real Prelude. Note that not all functions from original Prelude could be promoted or singled.

The singletons-base library provides promoted and singled equivalents of definitions found in several commonly used base library modules, including (but not limited to) Data.Bool, Data.Maybe, Data.Either, Data.List, Data.Tuple, and Data.Void. We also provide promoted and singled versions of common type classes, including (but not limited to) Eq, Ord, Show, Enum, and Bounded.

GHC.TypeLits.Singletons (from singletons-base) exports definitions for working with GHC.TypeLits.

Functions to generate singletons

The top-level functions used to generate promoted or singled definitions are documented in the Data.Singletons.TH module in singletons-th. The most common case is just calling the singletons function, which I'll describe here:

singletons :: Q [Dec] -> Q [Dec]

This function 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

This section contains a brief overview of some of the most important types from Data.Singletons (from 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.

type Sing :: k -> Type
type family Sing

The type family of singleton types. A new instance of this type family is generated for every new singleton type.

type SingI :: forall {k}. k -> Constraint
class SingI a where
  sing :: Sing a

A class used to pass singleton values implicitly. The sing method produces an explicit singleton value.

type SomeSing :: Type -> Type
data SomeSing k where
  SomeSing :: Sing (a :: k) -> SomeSing 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 Thing is isomorphic to Thing.

type SingKind :: Type -> Constraint
class SingKind k where
  type Demote k :: *
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing 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 toSing method produces an existentially-quantified singleton, wrapped up in a SomeSing. The Demote associated kind-indexed type family maps the kind Nat back to the type Nat.

type SingInstance :: k -> Type
data SingInstance a 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.

In addition to SingI, there are also higher-order versions named SingI1 and SingI2:

type SingI1 :: forall {k1 k2}. (k1 -> k2) -> Constraint
class (forall x. SingI x => SingI (f x)) => SingI1 f where
  liftSing :: Sing x -> Sing (f x)

type SingI2 :: forall {k1 k2 k3}. (k1 -> k2 -> k3) -> Constraint
class (forall x y. (SingI x, SingI y) => SingI (f x y)) => SingI2 f where
  liftSing2 :: Sing x -> Sing y -> Sing (f x y)

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 (==) (in the PEq class) and the (%==) method (in the SEq class). See the Data.Eq.Singletons module from singletons-base 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 from singletons 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 SEq, SDecide, TestEquality, and TestCoercion 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 (from singletons-th) and Data.Singletons.Base.TH (from singletons-base).

Show classes

Promoted and singled versions of the Show class (PShow and SShow, respectively) are provided in the Text.Show.Singletons module from singletons-base. In addition, there is a ShowSing constraint synonym provided in the Data.Singletons.ShowSing module from singletons:

type ShowSing :: Type -> Constraint
type ShowSing k = (forall z. Show (Sing (z :: k)) -- Approximately

This facilitates the ability to write Show instances for Sing instances.

What distinguishes all of these Shows? Let's use the False constructor as an example. If you used the PShow Bool instance, then the output of calling Show_ on False is "False", much like the value-level Show Bool instance (similarly for the SShow Bool instance). However, the Show (Sing (z :: Bool)) instance (i.e., ShowSing Bool) is intended for printing the value of the singleton constructor SFalse, so calling show SFalse yields "SFalse".

Instance of PShow, SShow, and Show (for the singleton type) are generated when singletons is called on a datatype that has deriving Show. You can also generate these instances directly through functions exported from Data.Singletons.TH (from singletons-th) and Data.Singletons.Base.TH (from singletons-base).

Errors

The singletons-base library provides two different ways to handle errors:

• The Error type family, from GHC.TypeLits.Singletons:

  type Error :: a -> k
  type family Error str where {}

  This is simply an empty, closed type family, which means that it will fail to reduce regardless of its input. The typical use case is giving it a Symbol as an argument, so that something akin to Error "This is an error message" appears in error messages.

• The TypeError type family, from Data.Singletons.Base.TypeError. This is a drop-in replacement for TypeError from GHC.TypeLits which can be used at both the type level and the value level (via the typeError function).

  Unlike Error, TypeError will result in an actual compile-time error message, which may be more desirable depending on the use case.

Pre-defined singletons

The singletons-base library defines a number of singleton types and functions by default. These include (but are not limited to):

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

These are all available through Prelude.Singletons. 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 the "Haskell constructs supported by singletons-th" section of this README for a full list.

Promoted definitions are usually generated by calling the 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 defunctionalization symbols. These are required to represent partial application at the type level. For more information, refer to the "Promotion and partial application" section below.

Users also have access to Prelude.Singletons and related modules (e.g., Data.Bool.Singletons, Data.Either.Singletons, Data.List.Singletons, Data.Maybe.Singletons, Data.Tuple.Singletons, etc.) in singletons-base. 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.

Promotion and partial application

Promoting higher-order functions proves to be surprisingly tricky. Consider this example:

$(promote [d|
  map :: (a -> b) -> [a] -> [b]
  map _ []     = []
  map f (x:xs) = f x : map f xs
  |])

A naïve attempt to promote map would be:

type Map :: (a -> b) -> [a] -> [b]
type family Map f xs where
  Map _ '[]    = '[]
  Map f (x:xs) = f x : Map f xs

While this compiles, it is much less useful than we would like. In particular, common idioms like Map Id xs will not typecheck, since GHC requires that all invocations of type families be fully saturated. That is, the use of Id in Map Id xs is rejected since it is not applied to one argument, which the number of arguments that Id was defined with. For more information on this point, refer to the promotion paper.

Not having the ability to partially apply functions at the type level is rather painful, so we do the next best thing: we defunctionalize all promoted functions so that we can emulate partial application. For example, if one were to promote the id function:

$(promote [d|
  id :: a -> a
  id x = x
  |]

Then in addition to generating the promoted Id type family, two defunctionalization symbols will be generated:

type IdSym0 :: a ~> a
data IdSym0 x

type IdSym1 :: a -> a
type family IdSym1 x where
  IdSym1 x = Id x

In general, a function that accepts N arguments generates N+1 defunctionalization symbols when promoted.

IdSym1 is a fully saturated defunctionalization symbol and is usually only needed when generating code through the Template Haskell machinery. IdSym0 is more interesting: it has the kind a ~> a, which has a special arrow type (~>). Defunctionalization symbols using the (~>) kind are type-level constants that can be "applied" using a special Apply type family:

type Apply :: (a ~> b) -> a -> b
type family Apply f x

Every defunctionalization symbol comes with a corresponding Apply instance (except for fully saturated defunctionalization symbols). For instance, here is the Apply instance for IdSym0:

type instance Apply IdSym0 x = Id x

The (~>) kind is used when promoting higher-order functions so that partially applied arguments can be passed to them. For instance, here is our final attempt at promoting map:

type Map :: (a ~> b) -> [a] -> [b]
type family Map f xs where
  Map _ '[]    = '[]
  Map f (x:xs) = Apply f x : Map f xs

Now map id xs can be promoted to Map IdSym0 xs, which typechecks without issue.

Defunctionalizing existing type families

The most common way to defunctionalize functions is by promoting them with the Template Haskell machinery. One can also defunctionalize existing type families, however, by using genDefunSymbols. For example:

type MyTypeFamily :: Nat -> Bool
type family MyTypeFamily n

$(genDefunSymbols [''MyTypeFamily])

This can be especially useful if MyTypeFamily needs to be implemented by hand. Be aware of the following design limitations of genDefunSymbols:

• genDefunSymbols only works for type-level declarations. Namely, it only works when given the names of type classes, type families, type synonyms, or data types. Attempting to pass the name of a term level function, class method, data constructor, or record selector will throw an error.
• Passing the name of a data type to genDefunSymbols will cause its data constructors to be defunctionalized but not its record selectors.
• Passing the name of a type class to genDefunSymbols will cause the class itself to be defunctionalized, but /not/ its associated type families or methods.

Note that the limitations above reflect the current design of genDefunSymbols. As a result, they are subject to change in the future.

Defunctionalization and visible dependent quantification

Unlike most other parts of singletons-th, which disallow visible dependent quantification (VDQ), genDefunSymbols has limited support for VDQ. Consider this example:

type MyProxy :: forall (k :: Type) -> k -> Type
type family MyProxy k (a :: k) :: Type where
  MyProxy k (a :: k) = Proxy a

$(genDefunSymbols [''MyProxy])

This will generate the following defunctionalization symbols:

type MyProxySym0 ::              Type  ~> k ~> Type
type MyProxySym1 :: forall (k :: Type) -> k ~> Type
type MyProxySym2 :: forall (k :: Type) -> k -> Type

Note that MyProxySym0 is a bit more general than it ought to be, since there is no dependency between the first kind (Type) and the second kind (k). But this would require the ability to write something like this:

type MyProxySym0 :: forall (k :: Type) ~> k ~> Type

This currently isn't possible. So for the time being, the kind of MyProxySym0 will be slightly more general, which means that under rare circumstances, you may have to provide extra type signatures if you write code which exploits the dependency in MyProxy's kind.

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 PEq a => POrd 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 SEq a => SOrd 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 singled 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 Bool where
  type Compare 'False 'False = 'EQ
  type Compare 'False 'True  = 'LT
  type Compare 'True  'False = 'GT
  type Compare 'True  'True  = 'EQ

instance SOrd 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-th 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