Existential witnesses, singletons, and classes for operations on GHC TypeLits https://github.com/mstksg/typelits-witnesses
|Version on this page:||0.3.0.2|
|LTS Haskell 14.27:||0.4.0.0|
|Stackage Nightly 2019-09-21:||0.4.0.0|
|Latest on Hackage:||0.4.0.0|
Provides witnesses for
KnownSymbol instances for various
operations on GHC TypeLits — in particular, the arithmetic operations
GHC.TypeLits, and also for type-level lists of
This is useful for situations where you have
KnownNat n, and you want to
prove to GHC
KnownNat (n + 3), or
KnownNat (2*n + 4).
It’s also useful for when you want to work with type level lists of
KnownSymbol instances and singletons for traversing them, and be
able to apply analogies of
symbolVal to lists with analogies for
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
Provides tools for refining upper and lower bounds on
KnownNats and proving
inequalities involving GHC.TypeLits’s comparison API. (Both with
If a library function requires
1 <= n constraint, but only
KnownNat n is
foo :: (KnownNat n, 1 <= n) => Proxy n -> Int bar :: KnownNat n => Proxy n -> Int bar n = case Proxy @1 %<=? n of LE Refl -> foo n NLE _ -> 0
foo requires that
1 <= n, but
bar has to handle all cases of
lets you compare the
KnownNats in two
Proxys and returns a
has two constructors,
If you pattern match on the result, in the
LE branch, the constraint
1 <= n will be satisfied according to GHC, so
bar can safely call
foo, and GHC will recognize that
1 <= n.
NLE branch, the constraint that
1 > n is satisfied, so any
functions that require that constraint would be callable.
isNLE are also offered:
bar :: KnownNat n => Proxy n -> Int bar n = case Proxy @1 `isLE` n of Just Refl -> foo n Nothing -> 0
Similarly, if a library function requires something involving
you can use
cmpNat and the
foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int bar :: KnownNat n => Proxy n -> Int bar n = case Proxy @5 `cmpNat` n of CLT Refl -> foo1 n CEQ _ -> 0 CGT Refl -> foo2 n
You can use the
cmpNat gives you with
cmpNatLE to “flip” the inequality or turn it into something compatible
<=? (useful for when you have to work with libraries that mix the
two methods) or
eqCmpNat to get to/from witnesses for
equality of the two
SOFT DEPRECATED: Use singletons library instead! However, this module is still here in case people want the functionality of singletons without requiring the entire library.
Provides witnesses for instances arising from the arithmetic operations
In general, if you have
KnownNat n, GHC can’t infer
KnownNat (n + 1);
and if you have
KnownNat m, as well, GHC can’t infer
KnownNat (n + m).
This can be extremely annoying when dealing with libraries and applications
where one regularly adds and subtracts type-level nats and expects
instances to follow. For example, vector concatenation of length-encoded
vector types can be:
concat :: (KnownNat n, KnownNat m) => Vector n a -> Vector m a -> Vector (n + m) a
n + m now does not have a
KnownNat instance, which severely hinders
what you can do with this!
Consider this concrete (but silly) example:
getDoubled :: KnownNat n => Proxy n -> Integer getDoubled p = natVal (Proxy @(n * 2))
Which is supposed to call
n * 2. However, this fails, because
n is a
n * 2 is not necessarily so. This module lets
you re-assure GHC that this is okay.
The most straightforward/high-level usage is with
getDoubled :: forall n. KnownNat n => Proxy n -> Integer getDoubled p = withNatOp (%*) p (Proxy @2) $ natVal (Proxy @(n * 2))
Within the scope of the argument of
withNatOp (%*) (Proxy @n) (Proxy @m),
n * m is an instance
KnownNat, so you can use
natVal on it, and get the expected result:
> getDoubled (Proxy @12) 24
There are four “nat operations” defined here, corresponding to the four
type-level operations on
Nat provided in
(%^), corresponding to addition, subtraction, multiplication, and
(%-) is implemented in a way that allows for the result to be a
There are more advanced operations dealing with low-level machinery, as well, in the module. See module documentation for more detail.
This module is deprecated, and it is recommended you use the functionality from
the singletons package instead. A direct translation using
getDoubled :: forall n. KnownNat n => Proxy n -> Integer getDoubled p = withKnownNat (SNat @n %:* SNat @2) $ natVal (Proxy @(n * 2))
But one using singletons throughout the whole process would be:
getDoubled :: forall n. KnownNat n => Sing n -> Integer getDoubled s = withKnownNat (s %:* SNat @2) $ natVal (Proxy @(n * 2))
**HARD DEPRECATED: Use singletons library instead! This module is extremely unweildy, and using singletons is much, much smoother on many levels, and integrates everything together in a nice way. This module will likely be removed in a future version.
Provides analogies of
natVal, etc., to type-level
KnownNat instances, and also singletons for iterating over
type-level lists of
If you had
KnownNats ns, then you have two things you can do with it; first,
natsVal, which is like
natVal but for type-level lists of
> natsVal (Proxy @[1,2,3]) [1,2,3]
And more importantly,
natsList, which provides singletons that you can
pattern match on to “reify” the structure of the list, getting a
Proxy n for
every item in the list with a
KnownSymbol instance in scope for
you to use:
printNats :: NatList ns -> IO () printNats nl = case nl of ØNL -> return () p :># nl' -> do print $ natVal p printNats nl'
> printNats (natsList :: @[1,2,3]) 1 2 3
Without this, there is no way to “iterate over” and “access” every
Nat in a
KnownNats. You can’t “iterate” over
but you can iterate over them in
This module also lets you “reify” lists of
SymbolLists, so you can access them at the type level for
some dependent types fun.
> reifyNats [1,2,3] $ \nl -> do print nl printNats nl Proxy :<# Proxy :<# Proxy :<# ØNL 1 2 3
Another thing you can do is provide witneses that two
are the same/were instantiated with the same numbers/symbols.
> reifyNats [1,2,3] $ \ns -> do reifyNats [1,2,3] $ \ms -> do case sameNats ns ms of Just Refl -> -- in this branch, ns and ms are the same. Nothing -> -- in this branch, they aren't
The above would match on the
Just Refl branch.
See module documentation for more details and variations.
This module is deprecated, and it is recommended you use the functionality from
the singletons package instead.
sameNats is simply
%~, and you can traverse/reify
singletons of lists too:
printNats :: forall (ns :: [Nat]). Sing ns -> IO () printNats ss = case ss of SNil -> return () s `SCons` ss' -> do print $ fromSing s printNats ss'
March 30, 2018
- Functions taking multiple
p min GHC.TypeLits.Compare now are able to take different “proxy” types (
- Documentation fixes because deprecation warnings were not showing up on haddocks for GHC.TypeLits.List.
- Added extra witnesses inside the constructors of
- Allowed functions to polymorphically expect
p ninstead of
Proxy nwhenever possible.
- Soft deprecation of GHC.TypeLits.Witnesses, in case people want to use the functionality of singletons without the full library.
- Formal deprecation of GHC.TypeLits.List, with migration information, because it’s just so much more unweidly than using singletons.
- Added the
GHC.TypeLits.Comparemodule for refining bounds and proving inequalities on
KnownNats and associated utility functions.
- Removed redundant
- Added “eliminators”, a staple of dependently typed programming, for
Breaking: Changed the name of
someNatsValPos, to break away from the “just add
'” anti-pattern and to make the function name a bit more meaningful.
reifyNats', a “safe” version of
reifyNatsshould be the safe one, but its connection to
reifyNatfrom the reflection package is very strong and worth preserving, I think.
mapSymbolList; they use
SymbolListinstead of Rank-2 types, so they can work better with function composition with
(.)and other things that Rank-2 types would have trouble with.
sameSymbols, modeled after
sameSymbol. They provide witnesses to GHC that
KnownNats passed in are both the same.
- Added strict fields to
SomeSymbols. It really doesn’t make any sense for them to be lazy.
- Added README to the cabal package as an extra source file, for viewing on Hackage.
- Initial version.