typelitswitnesses
Existential witnesses, singletons, and classes for operations on GHC TypeLits
https://github.com/mstksg/typelitswitnesses
Version on this page:  0.2.3.0 
LTS Haskell 19.33:  0.4.0.0@rev:1 
Stackage Nightly 20220317:  0.4.0.0 
Latest on Hackage:  0.4.0.0@rev:1 
typelitswitnesses0.2.3.0@sha256:666f13234db641c9217d7a0ca0ef9c0ef6c885f886d14a9fccbb76e5f2dbad2d,2901
Module documentation for 0.2.3.0
 GHC
typelitswitnesses
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 typelevel lists of KnownNat
and
KnownSymbol
instances.
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
KnownNat
/KnownSymbol
instances and singletons for traversing them, and be
able to apply analogies of natVal
/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.
GHC.TypeLits.Witnesses
Provides witnesses for instances arising from the arithmetic operations
defined in GHC.TypeLits
.
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 typelevel nats and expects KnownNat
instances to follow. For example, vector concatenation of lengthencoded
vector types can be:
concat :: (KnownNat n, KnownNat m)
=> Vector n a
> Vector m a
> Vector (n + m) a
But, 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 :: Proxy (n * 2))
Which is supposed to call natVal
with n * 2
. However, this fails, because
while n
is a KnownNat
, n * 2
is not necessarily so. This module lets
you reassure GHC that this is okay.
The most straightforward/highlevel usage is with withNatOp
:
getDoubled :: forall n. KnownNat n => Proxy n > Integer
getDoubled p = withNatOp (%*) p (Proxy :: Proxy 2) $
natVal (Proxy :: Proxy (n * 2))
Within the scope of the argument of
withNatOp (%*) (Proxy :: Proxy n) (Proxy :: Proxy m)
, n * m
is an instance
of KnownNat
, so you can use natVal
on it, and get the expected result:
> getDoubled (Proxy :: Proxy 12)
24
There are four “nat operations” defined here, corresponding to the four
typelevel operations on Nat
provided in GHC.TypeLits
: (%+)
, (%)
,
(%*)
, and (%^)
, corresponding to addition, subtraction, multiplication,
and exponentiation, respectively.
Note that (%)
is implemented in a way that allows for the result to be a
negative Nat
.
There are more advanced operations dealing with lowlevel machinery, as well, in the module. See module documentation for more detail.
GHC.TypeLits.Compare
Provides tools for refining upper and lower bounds on KnownNat
s and proving
inequalities involving GHC.TypeLits’s comparison API. (Both with <=?
and
CmpNat
).
If a library function requires 1 <= n
constraint, but only KnownNat n
is
available:
foo :: (KnownNat n, 1 <= n) => Proxy n > Int
bar :: KnownNat n => Proxy n > Int
bar n = case (Proxy :: Proxy 1) %<=? n of
LE Refl > foo n
NLE _ > 0
foo
requires that 1 <= n
, but bar
has to handle all cases of n
. %<=?
lets you compare the KnownNat
s in two Proxy
s and returns a :<=?
, which
has two constructors, LE
and NLE
.
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
.
In the NLE
branch, the constraint that 1 > n
is satisfied, so any
functions that require that constraint would be callable.
For convenience, isLE
and isNLE
are also offered:
bar :: KnownNat n => Proxy n > Int
bar n = case isLE (Proxy :: Proxy 1) n of
Just Refl > foo n
Nothing > 0
Similarly, if a library function requires something involving CmpNat
,
you can use cmpNat
and the SCmpNat
type:
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 cmpNat (Proxy :: Proxy 5) n of
CLT Refl > foo1 n
CEQ Refl > 0
CGT Refl > foo2 n
You can use the Refl
that cmpNat
gives you with flipCmpNat
and
cmpNatLE
to “flip” the inequality or turn it into something compatible
with <=?
(useful for when you have to work with libraries that mix the
two methods) or cmpNatEq
and eqCmpNat
to get to/from witnesses for
equality of the two Nat
s.
GHC.TypeLits.List
Provides analogies of KnownNat
, SomeNat
, natVal
, etc., to typelevel
lists of KnownNat
instances, and also singletons for iterating over
typelevel lists of Nat
s and Symbol
s.
If you had KnownNats ns
, then you have two things you can do with it; first,
natsVal
, which is like natVal
but for typelevel lists of KnownNats
:
> natsVal (Proxy :: 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 KnownNat
/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 :: NatList [1,2,3])
1
2
3
Without this, there is no way to “iterate over” and “access” every Nat
in a
list of KnownNat
s. You can’t “iterate” over [1,2,3]
in Proxy [1,2,3]
,
but you can iterate over them in NatList [1,2,3]
.
This module also lets you “reify” lists of Integer
s or String
s into
NatList
s and SymbolList
s, 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 [Nat]
s or [Symbol]
s
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.
Changes
Version 0.2.3.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.2.3.0
 Added the
GHC.TypeLits.Compare
module for refining bounds and proving inequalities onKnownNat
s and associated utility functions.
Version 0.2.2.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.2.2.0
 Removed redundant
KnownNats
andKnownSymbols
constraints forsameNats
andsameSymbols
.
Version 0.2.1.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.2.1.0
 Added “eliminators”, a staple of dependently typed programming, for
NatList
andSymbolList
.
Version 0.2.0.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.2.0.0

Breaking: Changed the name of
someNatsVal'
tosomeNatsValPos
, to break away from the “just add'
” antipattern and to make the function name a bit more meaningful. 
Added
reifyNats'
, a “safe” version ofreifyNats
. Ideally,reifyNats
should be the safe one, but its connection toreifyNat
from the reflection package is very strong and worth preserving, I think.
Version 0.1.2.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.1.2.0

Added
mapNatList'
andmapSymbolList'
companions tomapNatList
andmapSymbolList
; they useNatList
andSymbolList
instead of Rank2 types, so they can work better with function composition with(.)
and other things that Rank2 types would have trouble with. 
Added
sameNats
andsameSymbols
, modeled aftersameNat
andsameSymbol
. They provide witnesses to GHC thatKnownNat
s passed in are both the same.
Version 0.1.1.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.1.1.0
 Added strict fields to
NatList
,SomeNats
,SymbolList
, andSomeSymbols
. It really doesn’t make any sense for them to be lazy.
Version 0.1.0.1
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.1.0.1
 Added README to the cabal package as an extra source file, for viewing on Hackage.
Version 0.1.0.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.1.0.0
 Initial version.