singletons-th

A framework for generating singleton types

http://www.github.com/goldfirere/singletons

Version on this page:3.2
LTS Haskell 22.39:3.2
Stackage Nightly 2024-10-31:3.3
Latest on Hackage:3.4

See all snapshots singletons-th appears in

BSD-3-Clause licensed by Richard Eisenberg, Jan Stolarek
Maintained by Ryan Scott
This version can be pinned in stack with:singletons-th-3.2@sha256:07b39a6c93a338cebb0437ffa071ac4b64a71f9a4951e5c511a89741d1147ee7,4700

singletons-th

Hackage

singletons-th defines Template Haskell functionality that allows promotion of term-level functions to type-level equivalents and singling functions to dependently typed equivalents. This library was originally presented in Dependently Typed Programming with Singletons, published at the Haskell Symposium, 2012. See also the paper published at Haskell Symposium, 2014, which describes how promotion works in greater detail.

singletons-th generates code that relies on bleeding-edge GHC language extensions. As such, singletons-th only supports the latest major version of GHC (currently GHC 9.6). For more information, consult the singletons README.

You may also be interested in the following related libraries:

  • The singletons library is a small, foundational library that defines basic singleton-related types and definitions.
  • The singletons-base library uses singletons-th to define promoted and singled functions from the base library, including the Prelude.

Changes

Changelog for the singletons-th project

3.2 [2023.03.12]

  • Require building with GHC 9.6.
  • Derived POrd and SOrd instances (arising from a use of deriving Ord) now use (<>) @Ordering in their implementations instead of the custom thenCmp :: Ordering -> Ordering -> Ordering function. While most code will likely continue to work after this change, this may break code that attempts to prove properties about the implementation of a derived POrd/SOrd instance.
  • Fix a bug in which the singDecideInstances and showSingInstances, as well as deriving Show declarations, would not respect custom promotedDataTypeOrConName options.
  • Allow building with mtl-2.3.*.

3.1.1 [2022.08.23]

  • Require building with GHC 9.4.
  • Improve error messages when attempting to promote a partial application of a function arrow (->), which is not currently supported.

3.1 [2021.10.30]

  • Require building with GHC 9.2.
  • Allow promoting and singling type applications in data constructor patterns.
  • Make the Template Haskell machinery generate SingI1 and SingI2 instances when possible.
  • Make genDefunSymbols and related functions less likely to trigger GHC#19743.

3.0 [2021.03.12]

  • The singletons library has been split into three libraries:

    • The new singletons library is now a minimal library that only provides Data.Singletons, Data.Singletons.Decide, Data.Singletons.Sigma, and Data.Singletons.ShowSing (if compiled with GHC 8.6 or later). singletons now supports building GHCs back to GHC 8.0, as well as GHCJS.
    • The singletons-th library defines Template Haskell functionality for promoting and singling term-level definitions, but but nothing else. This library continues to require the latest stable release of GHC.
    • The singletons-base library defines promoted and singled versions of definitions from the base library, including the Prelude. This library continues to require the latest stable release of GHC.

    Consult the changelogs for singletons and singletons-base for changes specific to those libraries. For more information on this split, see the relevant GitHub discussion.

  • Require building with GHC 9.0.

  • Data.Singletons.CustomStar and Data.Singletons.SuppressUnusedWarnings have been renamed to Data.Singletons.TH.CustomStar and Data.Singletons.SuppressUnusedWarnings, respectively, to give every module in singletons-th a consistent module prefix.

  • Due to the singletons package split, the singletons-th modules Data.Singletons.TH and Data.Singletons.TH.CustomStar (formerly known as Data.Singletons.CustomStar) no longer re-export any definitions from the singletons-base module Prelude.Singletons (formerly known as Data.Singletons.Prelude). The singletons-base library now provides versions of these modules—Data.Singletons.Base.CustomStar and Data.Singletons.Base.TH, respectively—that do re-export definitions from Prelude.Singletons.

  • “Fully saturated” defunctionalization symbols (e.g., IdSym1) are now defined as type families instead of type synonyms. This has two notable benefits:

    • Fully saturated defunctionalization symbols can now be given standalone kind signatures, which ensures that the order of kind variables is the same as the user originally declared them.
    • This fixes a minor regression in singletons-2.7 in which the quality of :kind! output in GHCi would become worse when using promoted type families generated by Template Haskell.

    Under certain circumstances, this can be a breaking change:

    • Since more TH-generated promoted functions now have type families on their right-hand sides, some programs will now require UndecidableInstances where they didn’t before.

    • Certain definitions that made use of overlapping patterns, such as natMinus below, will no longer typecheck:

      $(singletons [d|
        data Nat = Z | S Nat
      
        natMinus :: Nat -> Nat -> Nat
        natMinus Z     _     = Z
        natMinus (S a) (S b) = natMinus a b
        natMinus a     Z     = a
        |])
      

      This can be worked around by avoiding the use of overlapping patterns. In the case of natMinus, this amounts to changing the third equation to match on its first argument:

      $(singletons [d|
        natMinus :: Nat -> Nat -> Nat
        natMinus Z       _     = Z
        natMinus (S a)   (S b) = natMinus a b
        natMinus a@(S _) Z     = a
        |])
      
  • The specification for how singletons deals with record selectors has been simplified. Previously, singletons would try to avoid promoting so-called “naughty” selectors (those whose types mention existential type variables that do not appear in the constructor’s return type) to top-level functions. Determing if a selector is naughty is quite challenging in practice, as determining if a type variable is existential or not in the context of Template Haskell is difficult in the general case. As a result, singletons now adopts the dumb-but-predictable approach of always promoting record selectors to top-level functions, naughty or not.

    This means that attempting to promote code with a naughty record selector, like in the example below, will no longer work:

    $(promote [d|
      data Some :: (Type -> Type) -> Type where
        MkSome :: { getSome :: f a } -> Some f
        -- getSome is naughty due to mentioning the type variable `a`
      |])
    

    Please open an issue if you find this restriction burdensome in practice.

  • The singEqInstanceOnly and singEqInstancesOnly functions, which generate SEq (but not PEq) instances, have been removed. There is not much point in keeping these functions around now that PEq now longer has a special default implementation. Use singEqInstance{s} instead.

  • The Template Haskell machinery will no longer promote TypeRep to Type, as this special case never worked properly in the first place.

  • The Template Haskell machinery will now preserve strict fields in data types when generating their singled counterparts.

  • Introduce a new promotedDataTypeOrConName option to Data.Singletons.TH.Options. Overriding this option can be useful in situations where one wishes to promote types such as Nat, Symbol, or data types built on top of them. See the “Arrows, Nat, Symbol, and literals” section of the README for more information.

  • Define a Quote instance for OptionsM. A notable benefit of this instance is that it avoids the need to explicitly lift TH quotes into OptionsM. Before, you would have to do this:

    import Control.Monad.Trans.Class (lift)
    
    withOptions defaultOptions
      $ singletons
      $ lift [d| data T = MkT |]
    

    But now, it suffices to simply do this:

    withOptions defaultOptions
      $ singletons [d| data T = MkT |]