typelitswitnesses
Existential witnesses, singletons, and classes for operations on GHC TypeLits https://github.com/mstksg/typelitswitnesses
Version on this page:  0.3.0.3 
LTS Haskell 13.3:  0.3.0.3 
Stackage Nightly 20190116:  0.3.0.3 
Latest on Hackage:  0.3.0.3 
Module documentation for 0.3.0.3
 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.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 @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 Proxy @1 `isLE` 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 Proxy @5 `cmpNat` n of
CLT Refl > foo1 n
CEQ _ > 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.Witnesses
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
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 @(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 @2) $
natVal (Proxy @(n * 2))
Within the scope of the argument of
withNatOp (%*) (Proxy @n) (Proxy @m)
, n * m
is an instance
of 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
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.
Singletons replacement
This module is deprecated, and it is recommended you use the functionality from
the singletons package instead. A direct translation using Proxy
would
be:
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))
GHC.TypeLits.List
**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 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 @[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 :: @[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.
Singletons replacement
This module is deprecated, and it is recommended you use the functionality from
the singletons package instead. natsVal
is fromSing
, reifyNats
is
toSing
/withSomeSing
, 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'
Changes
Version 0.3.0.3
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.3.0.3
October 1, 2018
 Fix build for GHC 8.6 and
TypeIsStar
changes.  Break compatibility with GHC < 8.0
Version 0.3.0.2
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.3.0.2
March 30, 2018
 Functions taking multiple
p m
in GHC.TypeLits.Compare now are able to take different “proxy” types (p
andq
).
Version 0.3.0.1
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.3.0.1
 Documentation fixes because deprecation warnings were not showing up on haddocks for GHC.TypeLits.List.
Version 0.3.0.0
https://github.com/mstksg/typelitswitnesses/releases/tag/v0.3.0.0
 Added extra witnesses inside the constructors of
(:<=?)
.  Allowed functions to polymorphically expect
p n
instead ofProxy n
whenever 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.
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.