GHC.TypeLits.Witnesses

Deprecated: Use the singletons package instead

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.

Singletons

All of the functionality in this module can be subsumed by the singletons package, by utilizing:

• Data.Singletons
• Data.Singletons.TypeLits
• Data.Singletons.Prelude.Num

This module is left in this package as an alternative for those who might, for some reason, not want to add a singletons dependency to their project. However, if you do much at the type level, using the singletons library is much preferred, as it provides a unifed interface for all of the functionality here, generalized to other kinds besides Nat.

For all functions in this module, a singletons equivalent is included for help migrating.

In general:

• The singletons type Sing n (or its equivalent, SNat n) subsumes both Proxy n and Dict (KnownNat n). You can replace both Proxy n and Dict (KnownNat n) with SNat n to move to singletons style.
• dictNatVal and natVal are both just fromSing.
• Replace %+, %-, and %* with their singletons equivalents, %:+, %:-, and %:* from Data.Singletons.Prelude.Num. Note that the current version of singletons does not have an equivalent for %^.
• Use withKnownNat from singletons (or just pattern match on SNat) to get a KnownNat instance from a SNat n, the same way you'd get one from a Dict.
• The high-level combinator withNatOp can simply be replaced with applying your singleton functions (%+ etc.) to SNat values, and pattern matching on the result, or using withKnownNat on the result.

withNatOp :: (KnownNat n, KnownNat m) => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) -> p n -> p 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.)

With singletons, withNatOp f x y is withKnownNat (f x y).

So, instead of

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

You can just use

withKnownNat (SNat n) ('SNat 1) $
    natVal (Proxy :: Proxy (n + 1))

natVal can of course be replaced with fromSing.

Direct witnesses

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

Create a Dict witness for KnownNat n.

Not necessary with singletons, as SNat n stands in for both Proxy n and Dict (KnownNat n).

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

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

With singletons, this is fromSing, which takes an SNat n and returns an Integer.

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.

With singletons, this is %:+ from Data.Singletons.Prelude.Num.

(%-) :: 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.

With singletons, this is %:- from Data.Singletons.Prelude.Num.

(%*) :: 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.

With singletons, this is %:* from Data.Singletons.Prelude.Num.

(%^) :: 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.