A framework for generating singleton types.

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. (https://richarde.dev/papers/2012/singletons/paper.pdf) See also the paper published at Haskell Symposium, 2014, which describes how promotion works in greater detail: https://richarde.dev/papers/2014/promotion/promotion.pdf.

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

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.

singletons-th

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

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.