Crypto.Number.Nat

Numbers at type level.

This module provides extensions to GHC.TypeLits and GHC.TypeNats useful to work with cryptographic algorithms parameterized with a variable bit length. Constraints like IsDivisibleBy8 n ensure that the type-level parameter is applicable to the algorithm.

Functions are also provided to test whether constraints are satisfied from values known at runtime. The following example shows how to discharge IsDivisibleBy8 in a computation fn requiring this constraint:

withDivisibleBy8 :: Integer
                 -> (forall proxy n . (KnownNat n, IsDivisibleBy8 n) => proxy n -> a)
                 -> Maybe a
withDivisibleBy8 len fn = do
    SomeNat p <- someNatVal len
    Refl <- isDivisibleBy8 p
    pure (fn p)

Function withDivisibleBy8 above returns Nothing when the argument len is negative or not divisible by 8.