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.

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 type-level nats and expects KnownNat 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

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 re-assure GHC that this is okay.

The most straightforward/high-level 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 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.

GHC.TypeLits.Compare

Provides tools for refining upper and lower bounds on KnownNats 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 KnownNats in two Proxys 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 Nats.

GHC.TypeLits.List

Provides analogies of KnownNat, SomeNat, natVal, etc., to type-level lists of KnownNat instances, and also singletons for iterating over type-level lists of Nats and Symbols.

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:

> 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 KnownNats. 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 Integers or Strings into NatLists and 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 [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.