Grisette.Utils

Utilities for type-level natural numbers.

Unsafe axiom

unsafeAxiom :: forall a b. a :~: b

Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!

Runtime representation of type-level natural numbers

data NatRepr (n :: Nat)

A runtime representation of type-level natural numbers. This can be used for performing dynamic checks on type-level natural numbers.

natValue :: NatRepr n -> Natural

The underlying runtime natural number value of a type-level natural number.

unsafeMkNatRepr :: Natural -> NatRepr n

Construct a runtime representation of a type-level natural number.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

natRepr :: forall n. KnownNat n => NatRepr n

Construct a runtime representation of a type-level natural number when its runtime value is known.

decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)

Decrement a NatRepr by 1.

predNat :: NatRepr (n + 1) -> NatRepr n

Predecessor of a NatRepr

incNat :: NatRepr n -> NatRepr (n + 1)

Increment a NatRepr by 1.

addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)

Addition of two NatReprs.

subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)

Subtraction of two NatReprs.

divNat :: 1 <= n => NatRepr m -> NatRepr n -> NatRepr (Div m n)

Division of two NatReprs.

halfNat :: NatRepr (n + n) -> NatRepr n

Half of a NatRepr.

Proof of KnownNat

data KnownProof (n :: Nat) where

'KnownProof n' is a type whose values are only inhabited when n has a known runtime value.

Constructors

KnownProof :: KnownNat n => KnownProof n

hasRepr :: forall n. NatRepr n -> KnownProof n

Construct a KnownProof given the runtime representation.

withKnownProof :: KnownProof n -> (KnownNat n => r) -> r

Introduces the KnownNat constraint when it's proven.

unsafeKnownProof :: Natural -> KnownProof n

Construct a KnownProof given the runtime value.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)

Adding two type-level natural numbers with known runtime values gives a type-level natural number with a known runtime value.

Proof of (<=) for type-level natural numbers

data LeqProof (m :: Nat) (n :: Nat) where

'LeqProof m n' is a type whose values are only inhabited when m <= n.

Constructors

LeqProof :: m <= n => LeqProof m n

withLeqProof :: LeqProof m n -> (m <= n => r) -> r

Introduces the m <= n constraint when it's proven.

unsafeLeqProof :: forall m n. LeqProof m n

Construct a LeqProof.

Note: This function is unsafe, as it does not check that the left-hand side is less than or equal to the right-hand side. You should ensure the consistency yourself or the program can crash or generate incorrect results.

testLeq :: NatRepr m -> NatRepr n -> Maybe (LeqProof m n)

Checks if a NatRepr is less than or equal to another NatRepr.

leqRefl :: f n -> LeqProof n n

Apply reflexivity to LeqProof.

leqSucc :: f n -> LeqProof n (n + 1)

A natural number is less than or equal to its successor.

leqTrans :: LeqProof a b -> LeqProof b c -> LeqProof a c

Apply transitivity to LeqProof.

leqZero :: LeqProof 0 n

Zero is less than or equal to any natural number.

leqAdd2 :: LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh)

Add both sides of two inequalities.

leqAdd :: LeqProof m n -> f o -> LeqProof m (n + o)

Produce proof that adding a value to the larger element in an LeqProof is larger.

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)

Adding two positive natural numbers is positive.