GHC.TypeLits.Witnesses

This module provides witnesses for instances that result from the various arithmetic operations on GHC TypeLits Nat types. 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, now n + m does not have a KnownNat instance...which makes operations like this extremely less useful!

At the highest level, this module can be used with withNatOp:

getDoubled :: forall n. KnownNat n => Proxy n -> Integer
getDoubled p = withNatOp (%*) p (Proxy :: Proxy 2) $
    natVal (Proxy :: Proxy (n * 2))

With the final argument of withNatOp, you can provide a result computed in an environment where n * 2 is indeed an instance of KnownNat.

For more complex usage, you can directly manipulate witnesses and then use them via pattern matching:

let pn = natDict (Proxy :: Proxy n)
    p1 = natDict (Proxy :: Proxy 1)
    p2 = natDict (Proxy :: Proxy 2)
in  case pn %* p2 %+ p1 of
      Dict -> natVal (Proxy :: Proxy (n * 2 + 1))

In the branch of the case statement, n * 2 + 1 indeed has a KnownNat instance.

Note that the operators have appropriate fixities to mimic value-level arithmetic operations.

WARNING: %- and entailSub are is implemented in a way such that negative KnownNats are produced without any errors. The production of witnesses and entailments will hold, but be aware that any functions that rely on KnownNat instances to be non-negative can potentially break.

High level wrapper

withNatOp :: (KnownNat n, KnownNat m) => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) -> Proxy n -> Proxy m -> (KnownNat q => r) -> r

A high-level the interface of this module. Give it one of the witness-generating operators on KnownNats in this module (%+, %-, %*, or %^), two Proxys containing the KnownNats to be modified, and receive an environment where the result of the operation (applied to the KnownNats) has a KnownNat instance.

For example, with

withNatOp (%+) (Proxy :: Proxy n) (Proxy :: Proxy 1) r

in r, n + 1 has a KnownNat instance:

withNatOp (%+) (Proxy :: Proxy n) (Proxy :: Proxy 1) $
    natVal (Proxy :: Proxy (n + 1))
-- => will return the Integer correpsonding to n + 1

Normally, if n is a KnownNat instance, it is not in general inferrable that n + 1 also has a KnownNat instance. This combinator makes it so.

For multiple operations on values, this can be chained:

withNatOp (%*) (Proxy :: Proxy n) (Proxy :: Proxy 2) $
  withNatOp (%+) (Proxy :: Proxy (n*2)) (Proxy :: Proxy 1) $
    natVal (Proxy :: Proxy (n * 2 + 1))

But, at this point, it's easier and simpler to just directly use the operators and pattern match:

let pn = natDict (Proxy :: Proxy n)
    p1 = natDict (Proxy :: Proxy 1)
    p2 = natDict (Proxy :: Proxy 2)
in  case pn %* p2 %+ p1 of
      Dict -> natVal (Proxy :: Proxy (n * 2 + 1))

(Note that associativity and fixity for the witness-generating operators are set to match that of normal addition and multiplication, etc.)

Direct witnesses

natDict :: KnownNat n => Proxy n -> Dict (KnownNat n)

Create a Dict witness for KnownNat n.

dictNatVal :: forall n. Dict (KnownNat n) -> Integer

Get the Integer from the KnownNat instance witnessed by the Dict.

Witness generators

(%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) infixl 6

Given witnesses for KnownNat n and KnownNat m, generates a witness for KnownNat (n + m).

Follows proper association and fixity for usage with other similar operators.

(%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m)) infixl 6

Given witnesses for KnownNat n and KnownNat m, generates a witness for KnownNat (n - m).

Note that this is implemented in a way such that negative KnownNats are produced without any errors.

Follows proper association and fixity for usage with other similar operators.

(%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) infixl 7

Given witnesses for KnownNat n and KnownNat m, generates a witness for KnownNat (n * m).

Follows proper association and fixity for usage with other similar operators.

(%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m)) infixr 8

Given witnesses for KnownNat n and KnownNat m, generates a witness for KnownNat (n ^ m).

Follows proper association and fixity for usage with other similar operators.

Entailments

entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)

An entailment for addition of KnownNat instances.

entailSub :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n - m)

An entailment for subtraction of KnownNat instances.

Note that this is implemented in a way such that negative KnownNats are produced without any errors.

entailMul :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)

An entailment for multiplication of KnownNat instances.

entailExp :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)

An entailment for exponentiation of KnownNat instances.