typelits-witnesses
==================
[](https://hackage.haskell.org/package/typelits-witnesses)
[](http://stackage.org/lts/package/typelits-witnesses)
[](http://stackage.org/nightly/package/typelits-witnesses)
[](https://travis-ci.org/mstksg/typelits-witnesses)
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 `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.
[singletons]: https://hackage.haskell.org/package/singletons
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:
~~~haskell
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:
~~~haskell
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:
~~~haskell
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 type-level nats and expects `KnownNat`
instances to follow. For example, vector concatenation of length-encoded
vector types can be:
~~~haskell
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:
~~~haskell
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 re-assure GHC that this is okay.
The most straightforward/high-level usage is with `withNatOp`:
~~~haskell
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:
~~~haskell
> getDoubled (Proxy @12)
24
~~~
There are four "nat operations" defined here, corresponding to the four
type-level 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 low-level 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:
~~~haskell
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:
~~~haskell
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 type-level
lists of `KnownNat` instances, and also singletons for iterating over
type-level 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 type-level lists of `KnownNats`:
~~~haskell
> 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:
~~~haskell
printNats :: NatList ns -> IO ()
printNats nl = case nl of
ØNL ->
return ()
p :># nl' -> do
print $ natVal p
printNats nl'
~~~
~~~haskell
> 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.
~~~haskell
> 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.
~~~haskell
> 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:
~~~haskell
printNats :: forall (ns :: [Nat]). Sing ns -> IO ()
printNats ss = case ss of
SNil ->
return ()
s `SCons` ss' -> do
print $ fromSing s
printNats ss'
~~~