typelits-witnesses-0.2.3.0: Existential witnesses, singletons, and classes for operations on GHC TypeLits
Provides witnesses for KnownNat
and KnownSymbol
instances for various operations on GHC TypeLits - in
particular, the arithmetic operations defined in
GHC.TypeLits, and also for type-level lists of
KnownNat
and KnownSymbol
instances.
This is useful for situations where you have
, and you want to prove to GHC
KnownNat
n
, or KnownNat
(n + 3)
, or when
constraints on the lower or upper limits of KnownNat
(2*n + 4)n
are
needed.
It's also useful for when you want to work with type
level lists of KnownNat
or KnownSymbol
instances and
singletons for traversing them, and be able to apply
analogies of natVal
and symbolVal
to lists with
analogies for SomeNat
and SomeSymbol
.
Note that most of the functionality in this library can be reproduced in a more generic way using the great singletons library. The versions here are provided as a "plumbing included" alternative that makes some commonly found design patterns involving GHC's TypeLits functionality a little smoother, especially when working with external libraries or GHC TypeLit's Nat comparison API.
See README for more information.
Modules
- GHC
- TypeLits
- GHC.TypeLits.Compare Tools and singletons for proving and refining inequalities
and bounds on GHC TypeLits types using
<=
and<=?
- GHC.TypeLits.List Typeclasses, singletons, and reifiers for type-level lists
of
Nat
s andSymbol
s. - GHC.TypeLits.Witnesses Instance witnesses for various arithmetic operations on GHC TypeLits.
- GHC.TypeLits.Compare Tools and singletons for proving and refining inequalities
and bounds on GHC TypeLits types using
- TypeLits